Transitive, Abstract, and Class Polymorphic Immutability

State mutations can often lead to silent program errors, including broken invariants and security vulnerabilities. Object-oriented languages offer basic mechanisms to prevent mutation; however, enforcing desired guarantees remains challenging. Two such guarantees are transitive immutability, which disallows mutation of all objects reachable from a reference, and abstract immutability, which permits controlled mutation of otherwise immutable objects. Furthermore, introducing readonly references to support subtype polymorphism often complicates the soundness of the type system. The integration of immutability into a class hierarchy introduces challenges, primarily manifesting as duplicated code between mutable and immutable variants.

We present Precise Immutability for Classes and Objects (PICO), a type system that enforces transitive abstract immutability with readonly references. PICO introduces novel viewpoint adaptation rules to achieve transitivity. These rules prevent unsoundness caused by mutable and immutable cross-type aliasing, a long-standing issue for systems combining immutability and assignability. Additionally, PICO formally defines the abstract state, which allows developers to permit mutation for selected parts of the object graph. PICO provides four state-preservation guarantees within a single system by selecting corresponding viewpoint adaptation rules: abstract-, concrete-, readonly-, and transitive-state preservation. Finally, the system supports safe class mutability polymorphism: one class can express both mutable and immutable uses, avoiding duplicate mutable/immutable class variants while also enabling backward-compatible retrofitting of existing hierarchies.

We formalize PICO and prove its type soundness and four state-preservation guarantees in the Rocq proof assistant. We also implement a type checker for Java using the Checker Framework. We evaluate this implementation on the Java Collections Framework in OpenJDK 17 and other benchmarks, covering approximately 26,000 non-comment lines of code. The results demonstrate that PICO effectively enforces immutability guarantees and can successfully retrofit existing libraries without duplicating code.