Infering Ownership Types for Encapsulated Object-Oriented Program Components

Modular analyses of object-oriented programs need clear encapsulation boundaries between program components. The reference semantics of object-oriented languages complicates encapsulation. Ownership type systems are a way to guarantee encapsulation. However, they introduce a substantial and nontrivial annotation overhead for the programmer. This is in particular true for type systems with an access policy that is more flexible than owners-as-dominators. As we want to use ownership disciplines as basis for modular analyses, we need the flexibility. However, to keep it practical, the annotation overhead should be kept minimal.

In this paper, we present such a flexible ownership type system together with an inference technique to reduce the annotation overhead. Runtime components in our approach can be accessed via the interface of the owner as well as via other boundary objects with explicitly declared interface types. The resulting type system is quite complex, however, the programmer only has to annotate the interface types of a component. The ownership type information for the classes implementing the components is automatically inferred by a constraint-based algorithm. We proved the soundness of our approach for a Java-like core language.