Ownership Types for Controlling Aliasing
A summary to introduce ownership types from reference 1 (link below): “Ownership types impose structural restrictions on object graphs based on statically definable and checkable notions of owner and representation. The owner of an object is another object and its representation is the objects owned by it. Ultimately, ownership types enforce a statically-checkable notion of encapsulation: every object can have its own private collection of representation objects which are not accessible outside the object which owns them.”
Why private fields are not sufficient (explanation in reference 2): In Java, if a field is declared to be private to a class, it cannot be accessed outside the class using that field name. However, Java allows the contents of a private field to be returned by a method. Using ownership types, this is not allowed, so we have object protection, which stronger that the name protection offered by normal programming languages.
Typical kind of a property enforced: the indicated edge is an articulation edge in a graph: if a node is reachable from a root, it must be reachable through a given edge.
Identify owners statically by some references that are immutable in a given scope
- 'this' always points to same thing within a method
- final references of 'this' and final local variables
Along with standard types, also track owner of objects, e.g.
- allow references from owner to its owned objects
- allow references between objects with same owner
- disallow other references
This diagram and the code that goes along with it are more fully explained in reference 1.
References