In the new 0.2.2 release of the typestate checker (an extension to the JSR308 checkers framework), you can now specify a state, to which an object transits, if a method returns true or false using the afterTrue and afterFalse elements in state annotations.

A good use-case and example is an Iterator. As you probably know, before calling next(), it’s good to check if an element is available using hasNext(). So we can distinguish two “states” of an iterator: CheckHasNext – which means that it is unknown if an element is available or not and ReadNext, in which it is safe to call next().

After calling hasNext(), the iterator should transit to the ReadNext state, but only if the method returns true. Also, after calling next(), the iterator should always transit to the CheckHasNext state. Using typestate annotations, we can write that specification on a stub of the Iterator interface:

public interface Iterator<E> {
  public abstract boolean hasNext() 
    @CheckHasNext(afterTrue=ReadNext.class) 
    @ReadNext;
  public abstract E next() @ReadNext(after=CheckHasNext.class);
  public abstract void remove();
}

Here I am using annotations on the receiver of the method, a new place where you can put annotations introduced with JSR308.

You can download the definitions of the stubs and the states in an easy-to-run example here. All you need to do is edit the example.sh file to specify the path to the JSR308 distribution, which you can download from its homepage. There are several example source code files which you can typestate-check. It is also quite easy to typestate check your own files – just change the SOURCES parameter of javac.

For example, this snippet of code checks without errors:

Iterator iter = collection.iterator();
  while (iter.hasNext()) {
    iter.next();
  }

While this throws an error on line 5:

Iterator iter = collection.iterator();
  while (iter.hasNext()) {
    iter.next();
  }
  iter.next(); // error: iter is in a wrong state

You can find the newest release available for download on the checker’s homepage, as well as in a maven2 repository. The source code is available on github.

Have fun!
Adam