This document describes the IGJ type annotations, and a checker (a compiler plugin) for them.
If the plugin issues no warnings for a given program, then that program will never change objects that should not be changed. This guarantee enables a programmer to detect and prevent mutation-related errors.
The IGJ checker plugin is distributed as part of the JSR 308 checkers framework.
Contents:
@I
IGJ is a Java language extension that helps programmers to avoid mutation errors that result from unintended side effects. In particular, IGJ permits a programmer to express that a particular object should never be modified via any reference (object immutability), or that a reference should never be used to modify its referent (reference immutability). Once a programmer has expressed these facts, an automatic checker analyzes the code to either locate mutability bugs or to guarantee that the code contains no such bugs.
To learn the details of the IGJ language and type system, please see the ESEC/FSE 2007 paper “Object and reference immutability using Java generics”. This IGJ checker supports Annotation IGJ, which is slightly different dialect of IGJ than that described in the ESEC/FSE paper.
The supported annotations are @ReadOnly
,
@Mutable
, @Immutable
,
@Assignable
, @AssignsFields
,
as specified in IGJ Document.
The @I(String)
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 inherited mutability.
The @Immutable
annotation ensures that a reference is immutable
to an immutable object.
The @I
annotation simulates mutability overloading. It can be
applied to classes, methods and parameters. Please read the section below
for further explanation.
This checker supports the Annotation IGJ dialect of IGJ. The syntax of Annotation IGJ is based on JSR 308 annotations.
The original version of IGJ was introduced in the ESEC/FSE 2007 paper “Object and reference immutability using Java generics”. The syntax of the original IGJ dialect was based on Java 5's generics and annotation mechanisms. The original IGJ dialect was not backward-compatible with Java (either syntactically or semantically). The dialect of IGJ checked by this plug-in corrects these problems.
The differences between the Annotation IGJ dialect and the original IGJ dialect are as follows.
Semantic Changes:
Vector<Mutable, Integer> <: Vector<ReadOnly, Integer> <: Vector<ReadOnly, Number> <: Vector<ReadOnly, Object>Annotation IGJ forbids such covariant changes, for backward compatibility with Java.
Syntax Changes:
@Immutable Date
.@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 { ... }
@I(id)
is
used to template over immutability.@I
Template annotation over IGJ Immutability annotations. It acts
somewhat similar to Type Variables in Generics. The annotation
value is used to distinguish between multiple instances of
@I
.
A class annotated with I
could be declared with any IGJ
Immutability annotation. The actual immutability that @I
is
resolved dictates the immutability type for all the non-static
appearances of @I
with the same value as the class
declaration.
Example:
@I public class FileDescriptor { private @Immutable Date creationData; private @I Date lastModData; public @I Date getLastModDate() @ReadOnly { } } ... void useFileDescriptor() { @Mutable FileDescriptor file = new @Mutable FileDescriptor(...); ... @Mutable Data date = file.getLastModDate(); }
In the last example, @I
was resolved to @Mutable
for
the instance file.
For example, it could be used for method parameters, return values, and the actual IGJ immutability value would be resolved based on the method invocation.
Example:
/* (1) */ static @I Point getMidpoint(@I Point p1, @I Point p2) { ... } /* (2) */ static <E> @I("T") Collection<E> findUnion(@I("T") Collection<E> col1, @I("G") Collection<E> col1) { ... }
Method (1) would return a Point
object that returns a Point with
the same immutability type as the passed parameters if p1 and p2 match in
immutability, otherwise @I
is resolved to @ReadOnly
.
Please note, that the @I
annotation value is used to distinguish
between @I
declarations. So, method (2) would return a collection
of the same immutability type as the first collection parameter.
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
Back to the JSR 308 checkers framework.