This document summarizes the IGJ type annotations, and a checker for them.
The IGJ type annotations and checker constitute an annotation-based dialect of the IGJ immutability checker. For more details about the original proposal of IGJ, see the IGJ language page.
The plugin itself is built on the checkers
framework and is implemented in the checkers.igj
package.
The supported annotations are @ReadOnly
,
@Mutable
, @Immutable
,
@Assignable
, @AssignsFields
,
as specified in IGJ Document.
@W(int) annotation is added to mimic the template behavior of Generics.
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 @Immutable
annotation ensures that a reference is immutable
to an immutable object.
The @W
annotation simulates mutability overloading. It can be
applied to classes, methods and parameters. Please read the section below
for further explanation.
@W
@W
.W
could be declared with any IGJ
Immutability annotation. The actual immutability that @W
is
resolved dectates the immutability type for all the non-static
appearances of @W
with the same value as the class
declaration.@W(0) public class FileDiscriptor { private @Immutable Date creationData; private @W(0) Date lastModData; public @W(0) getLastModDate() @ReadOnly { } } ... void useFileDiscriptor() { @Mutable FileDiscriptor file = new @Mutable FileDiscriptor(...); ... @Mutable Data date = file.getLastModDate(); }In the last example,
@W(0)
was resolved to @Mutable
for
the instance file./* (1) */ static @W(0) Point getMidPoint(@W(0) Point p1, @W(0) Point p2) { ... } /* (2) */ staticMethod (1) would return a@W(0) Collection findUnion(@W(0) Collection col1, @W(1) Collection col1) { ... }
Point
object that returns a Point with
the same immutability type as the passed parameters if p1 and p2 match in
immutability, otherwise @W(0)
is resolved to @ReadOnly
.@W
annotation value is used to distinguish
between @W
declarations. So, method (2) would return a collection
of the same immutability type as the first collection parameter.The original paper introduced the novel IGJ language building upon Java's generics and annotation mechanisms, as introduced in Java 5. This checker supports a dialect of IGJ that is based on JSR308 annotations. This dialect differs from the original proposal in semantics and syntax.
Semantic Changes:
Vector<Mutable, Integer> <: Vector<ReadOnly, Integer> <: Vector<ReadOnly, Number> <: Vector<ReadOnly, Object>The current dialect forbids that, due to a limitation in the annotation processor framework. Java compiler determines the subtyping rules during the Attribution phase (a.k.a. resolution phase), before the type processor round.
Syntax Changes:
@Immutable Date, @Immutable String
.@ReadOnly List<@Immutable Data>
, refers to a read only
List
of immutable Date
s.@ReadOnly Date[@Mutable][@Immutable]
is a read only array
that is composed of a mutable array containing immutable
Date
s. The array semantical meaning is similar to
@ReadOnly List<@Mutable List<@Immutable Date>>
.
public void setDate(@ReadOnly Date d) @AssignsFields { ... }
public @ReadOnly getDate() @ReadOnly { ... }
public boolean add(E e) @Mutable { ... }
@W(value)
is
used to template of immutability.To try the IGJ checker plugin on a source file that uses
the IGJ 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.igj.IGJChecker examples/IGJExample.java