Abstract:

A compiler-checked immutability guarantee provides useful documentation, 
facilitates reasoning, and enables optimizations. This talk will present 
Immutability Generic Java (IGJ), a novel language extension that 
expresses immutability without changing Java's syntax by building upon 
Java's generics and annotation mechanisms. In IGJ, each class has one 
additional type parameter that is Immutable, Mutable, or ReadOnly. IGJ 
guarantees both reference immutability (only mutable references can 
mutate an object) and object immutability (an immutable reference points 
to an immutable object). IGJ is the first proposal for enforcing object 
immutability within Java's syntax and type system, and its reference 
immutability is more expressive than previous work. IGJ also permits 
covariant changes of type parameters 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 generates byte-code that can be executed on any JVM 
without runtime penalty.