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 Javari checker plugin is distributed as part of the JSR 308 checkers framework.

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 inherited 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.

To run the test suite for the Javari checker, use ant javari-tests.

Examples from the test suite

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, or specify just one of the test files. (You might need to specify the classpath location of checkers.jar; add the option -cp checkers.jar if needed)


  javac -typeprocessor checkers.javari.JavariChecker tests/javari/*.java 

The compiler should issue the errors and warnings specified in the .out files with same name.


Back to the JSR 308 checkers framework.