===== 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

{{:ownership-types.jpg|Illustration from 'Ownership, Encapsulation and the Disjointness of Types and Effects'}}

This diagram and the code that goes along with it are more fully explained in reference 1. 

References

  - [[http://slurp.doc.ic.ac.uk/pubs/ownershipdisjointness-oopsla02.ps|Ownership, Encapsulation and the Disjointness of Types and Effects]]
  - [[http://doi.acm.org/10.1145/286936.286947|Ownership types for flexible alias protection]]
  - [[http://www.eecs.umich.edu/~bchandra/publications/phd.pdf|SafeJava: A Unified Type System for Safe Programming]]
  - [[http://www.jot.fm/issues/issue_2004_06/article2/index_html|Verification of object-oriented programs with invariants]]