Javari type annotations and checker

This document summarizes the Javari type annotations, and a checker for them.

The Javari type annotations and checker constitute an annotation-based implementation of the Javari immutability checker. For more details, see the Javari language page.

The supported annotations are @ReadOnly, @Mutable, @Assignable, @QReadOnly and @RoMaybe, that correspond to the Javari keywords readonly, mutable, assignable, ? readonly and romaybe, respectively.

The @ReadOnly type annotation indicates that a reference provides only read-only access. The plugin issues an error whenever mutation happens through a readonly reference, when fields of a readonly reference which are not explicitly marked with @Assignable are reassigned, or when a readonly expression is assigned to a mutable variable. The plugin also emits a warning when casts increase the mutability access of a reference.

The @Mutable annotation ensures that a reference is mutable, no matter the inheritted mutability.

The @QReadOnly annotation is a mutability wildcard that can be applied to types (for example, List<@QReadOnly Date>). As such, it allows only the operations which are allowed for both readonly and mutable types.

The @RoMaybe annotation simulates mutability overloading. It can be applied to methods and parameters. Read the @RoMaybe javadoc for more details.

The plugin itself is built on the checkers framework and is implemented in the checkers.javari package.

Tiny example

To try the Javari checker plugin on a source file that uses the Javari qualifier, use the following command, where javac is the JSR 308 compiler. (You might need to specify the classpath location of checkers.jar; add the option -cp checkers.jar if needed)


  javac -typeprocessor checkers.javari.JavariChecker examples/JavariExample.java 

The compiler should issue 24 errors and 1 warning. The inline comments detail why an operation is illegal, as well as the checker messages.