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