Blogs (9) >>
SPLASH 2016
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands

Immutability is a valuable feature for programmers in object-oriented languages: making objects immutable often simplifies reasoning about the correctness of code, particularly when concurrency is present. Java allows programmers to express and enforce immutability by declaring all fields of an object "final", but this comes at the cost of decreased expressiveness and intuitiveness of initialization. In this work, we propose a minimalistic type-based mechanism that both enforces immutability and relaxes these constraints on initialization. Furthermore, we propose and formalize two different type systems based on this mechanism that form a meaningful trade-off with respect to complexity, expressiveness, and strength of static guarantees. System One is simple, more expressive, and provides object-level immutability; System Two has more complicated annotation, is less expressive, and ensures that immutable objects are fully initialized in addition to enforcing immutability.