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

• Javari: Adding reference immutability to Java (OOPSLA 2005)
  An extended version (a Masters thesis, 2006) contains expanded explanations and also some additional material, as explained in its Chapter 7.
• Practical pluggable types for Java (ISSTA 2008)
  This paper (along with an OOPSLA 2007 demo) discusses the Checker Framework, on which the Javari implementation is built.
• A practical type system and language for reference immutability (OOPSLA 2004)
  This paper describes an earlier version of the language, which we call “Javari 2004”.

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

• Inference of reference immutability (ECOOP 2008)
  An extended version appeared as Jaime Quinonez's Master's thesis, 2008

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

• Object and reference immutability using Java generics (ESEC/FSE 2007)