Javarifier

Javarifier infers the immutability (according to the definition of the Javari language) of every reference in a Java program. In other words, it converts Java programs and libraries to Javari. It annotates source or .class format with backward-compatible comments or attributes. Annotating programs aids developers in reasoning about the code and modifying it without introducing subtle Mutation errors. Annotating libraries is important because Javari programs use libraries without Javari annotations often do not typecheck. Manually determining the mutability for each (public) parameter and return type is tedious and error-prone. Javarifier automatically performs this Analysis. Javarifier reads a set of Java classes to analyze (in .class format) and infers the (im)mutability of every reference. It outputs the inferred mutabilities in an annotation file, a textual file format for describing annotations of Java programs; the input class files are not modified. These annotations can be used directly, or inserted into either the .class files or the corresponding .java files using the annotation file utilities. If Javari annotations are inserted into the source code, they can be checked by the Javari type checker. In earlier versions of Javari, methods must be invariant in the mutability of their parameters and return types. The newer definition of Javari used by both Javarifier and the Javari type checker permits covariant subtyping on parameters and contra-variant subtyping on return types. Javarifier respects all existing Javari annotations in the program classes it analyzes. If any type is already annotated as @ReadOnly, Javarifier uses this annotation to determine the mutability of other types and does not change the existing @ReadOnly annotation. This mechanism is how Javarifier infers annotations on a program that uses libraries that have already been annotated using stub classes (also known as skeleton classes).