IGJ type annotations and checker

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:

IGJ and Mutability

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.

Supported Annotations

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.

Annotation IGJ Dialect

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:

Syntax Changes:

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

Usage on classes

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.

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

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 

Back to the JSR 308 checkers framework.