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 along all reachable objects from a reference, and abstract immutability, which permits safe internal 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.

In this paper, 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 exclude parts of the object graph from the immutability guarantee. PICO provides three immutability properties: abstract immutability, safe readonly, and concrete immutability within a single system, by selecting corresponding viewpoint adaptation rules. 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 class hierarchies.

We formalize PICO and prove its type soundness, along with its three immutability properties, 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.