A technical report with proof of soundness is available here: http://ecs.victoria.ac.nz/twiki/pub/Main/TechnicalReportSeries/

To use OIGJ compiler you must first download the Checkers Framework (look for checkers/oigj): http://code.google.com/p/checker-framework/

The Java language has no support for the important notions of ownership (an object owns its representation to prevent unwanted aliasing or modifications) and immutability (the division into mutable, immutable, and readonly). Inexperienced programmers are likely to make design mistakes such as representation exposure or violation of immutability contracts. This paper presents Ownership Immutability Generic Java (OIGJ), a backward-compatible purely-static language extension supporting ownership and immutability without changing Java's syntax.

OIGJ combines the two main flavors of ownership: owner-as-dominator and owner-as-modifier, that restricts aliasing and modifications, respectively. Thus, the programmer has the flexibility to choose whether the representation of an object cannot leak (the object dominates it) or whether it may be freely shared as readonly (only the object can modify it).

OIGJ is easy for the programmer to grasp and easy to implement (flow insensitive, using only 12 rules). Yet, OIGJ is more expressive than previous ownership languages, e.g., it can express the factory and visitor patterns. OIGJ is also more flexible than previous work, because it can type-check more good code. Specifically, OIGJ can type-check Sun's java.util collections (excluding the clone method) with only a small number of annotations. Previous work had to do major refactoring of existing code in order to fit their ownership restrictions. Forcing refactoring of well-designed code is undesirable because it costs programmer effort, results in worse design, and hinders adoption in the mainstream community.

OIGJ is based on previous work on ownership (OGJ) and immutability (IGJ). This paper also presents an extension of OGJ, called OGJ+, that supports scoped-confinement and existential owners with no additional syntax changes. OIGJ adds owner-as-modifier to OGJ+, as well as other enhancements to IGJ due to the delicate intricacies between ownership and immutability. We formally define the OIGJ typing rules and prove them sound.