IGJ type annotations and checker

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.

Supported Annotations

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.

Templating Over Immutability: @W

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 @W.
Usage On classes
A class annotated with 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.
Example:
    @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.
Usage On Methods
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 @W(0) Point getMidPoint(@W(0) Point p1, @W(0) Point p2) 
                 { ... }

/* (2) */    static  @W(0) Collection findUnion(@W(0) Collection col1,
                                                @W(1) Collection 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 @W(0) is resolved to @ReadOnly.
Please note, that the @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.



IGJ Annotation Dialect

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:

Syntax Changes:

Tiny example

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