Javari: Java with reference immutability

Javari is a backward-compatible extension of the Java language. Javari permits a programmer to specify that a particular reference is read-only — that is, the reference cannot be used to change the transitive state of its referent. The Javari compile-time checker verifies this property, giving a programmer (or other tools) confidence that no side effects are performed through the reference. The Javari toolset helps programmers to detect and prevent subtle, hard-to-debug errors in their programs.

Javari implementation

The Javari implementation is distributed as part of the Checker framework. Follow the installation instructions, or read the Javari section of the manual.

Javarifier implementation

Javarifier infers reference immutability. In other words, given a Java program, Javarifier inserts Javari keywords into it. Javarifier is available for download.

Publications (technical papers)

For more information about Javari, see the papers

Javarifier infers Javari's reference immutability keywords. It is described in the following papers.

Javari enforces reference immutability. An alternative language design that enforces both object and reference immutability is is IGJ (Immutability Generic Java):