Object and reference immutability using Java generics

A compiler-checked immutability guarantee provides useful doc-umentation, facilitates reasoning, and enables optimizations. This paper presents Immutability Generic Java (IGJ), a novel language extension that expresses immutability without changing Java’s syn-tax by building upon Java’s generics and annotation mechanisms. In IGJ, each class has one additional generic parameter that is Immutable, Mutable, or ReadOnly. IGJ guarantees both refer-ence immutability (only mutable references can mutate an object) and object immutability (an immutable reference points to an im-mutable object). IGJ is the first proposal for enforcing object im-mutability, and its reference immutability is more expressive than previous work. IGJ also permits covariant changes of generic ar-guments in a type-safe manner, e.g., a readonly list of integers is a subtype of a readonly list of numbers. IGJ extends Java’s type system with a few simple rules. We formalize this type system and prove it sound. Our IGJ compiler works by type-erasure and gen-erates byte-code that can be executed on any JVM without runtime penalty. 1