I’ve uploaded a new version (0.2) of the typestate checker (for an introduction, see this blog post), which contains bug fixes and much improved exception handling. The binaries, source code and installation instructions are on the web page; the source code is also on github, and the binaries in the maven repository. You can use the typestate checker with the jsr308-maven plugin.

A new state-annotation element: onException is supported, which specifies the state, to which an object transits, in case of an exception being thrown (from the place where the object is used: a method or constructor). For example, the specification of some of InputStreams methods could look like this:

class InputStream implements Closeable {
   int read() /*@Open(onException=InputStreamError.class)*/ 
    throws java.io.IOException;
   close() /*@Any(after=Closed.class)*/
}

This specification says that the read method can only be invoked when the object is in the “open” state, and in case of an error, the object transits to the “inputStreamError” state; that means that the read method cannot be invoked anymore. The close method transits the object from any state (so it can be invoked both when the stream is open, or in an error), to a closed state; again, read cannot be invoked anymore.

The annotations are in comments to make the code Java5-compatible; the checkers framework will recognize them.

Thanks to such specification, and the typestate checker, we can verify at compile-time that no read operations are invoked when the stream is closed. For example, the code below won’t compile (type-check), if compiled with the typestate checker, because of the invalid use of the last read method:

int test(@Open InputStream stream) throws IOException {
  int ret = 0;
  try {
    int input;
    while ((input = stream.read()) != -1) {
      ret += input;
    }
  } finally {
    stream.close();
  }

  // An error will be reported here; the stream is closed
  ret += stream.read();

  return ret;
}

More examples can be found in the examples directory of the source distribution (and ran with the example.sh script; on github: example 1, example 2)

The flow algorithm was improved to properly handle various try-catch-finally combinations, inferring the states of the objects properly when the catches are “alive” or “dead” (if they return/throw an exception or not).

Any opinions, comments, suggestions are welcome! :)

Adam