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