Typestate checker

Introduction

For an introduction on state annotations and the typestate checker, see this blog entry (this one and this one for information on the new features)

Installation

Java 6 (or higher) is required. To run the typestate checker, you must download the checkers framework. Unpack the jsr308-checkers.zip file, and download typestate-checker.jar. You can then run the checker using this command:

$JSR308/checkers/binary/javac -proc:only -processor checkers.typestate.TypestateChecker -cp $TYPESTATE/typestate-checker.jar MyClass.java

where $JSR308 is the directory to which you unpacked the checkers framework, and $TYPESTATE is the directory to which you downloaded the typestate checker. Thanks to the "-proc:only" option, no files are compiled, only the additional type-checking is done. You may also include a "-sourcepath $SOURCEPATH" option, to include for example some typestate-annotated class stubs.

Downloads

The source code is available on github: http://github.com/adamw/jsr308-typestate-checker/tree/master.

And the binaries in the maven repository: http://repository.mamut.net.pl/content/repositories/releases/mamut/net/pl/typestate-checker/0.2.2/.

Also, you can take a look at the javadocs.

Examples

You can find some examples, using an annotated InputStream in the examples directory of the source code. They are also available via the web interface of github. The examples show how to verify at compile-time that the read operation is not invoked on a closed input stream.

Some simple example java files on which you can test. Note that all of these will compile even on Java 5.

import checkers.typestate.State;
import checkers.typestate.NoChange;

public class VariableReceiverState {
    @State public static @interface State1 { Class after() default NoChange.class; }
    @State public static @interface State2 { Class after() default NoChange.class; }

    public static class Helper {
        // We use receiver annotations to specify the state, in which the object that invokes the method must be.
        public void onlyInState1() /*@State1*/ { }
        public void fromState1ToState2() /*@State1(after=State2.class)*/ { }
        public void onlyInState2() /*@State2*/ { }
    }

    // By annotating a parameter with a state annotation, we specify that the parameter must be in the given
    // state. This state is also the initial state of the variable in the method body.
    public void testOk(@State1 Helper h) {
        h.onlyInState1();
        h.fromState1ToState2();
        h.onlyInState2();
    }

    public void testError1(@State1 Helper h) {
        h.onlyInState1();
        h.fromState1ToState2();
        h.onlyInState1(); // error
    }

    public void testError2(@State1 Helper h) {
        h.onlyInState1();
        h.fromState1ToState2();
        h.fromState1ToState2(); // error
    }
}
import checkers.typestate.State;
import checkers.typestate.NoChange;

public class SimpleVariableTransitionState {
    @State public static @interface State1 { Class after() default NoChange.class; }
    @State public static @interface State2 { Class after() default NoChange.class; }

    public static class Helper {
        // The initial state of an object can be specified in the receiver annotation of the constructor.
        public Helper() /*@State1*/ { }
    }

    public void acceptHelperInState1(@State1 Helper h) { }
    public void acceptHelperInState2(@State2 Helper h) { }
    public void transit(@State1(after=State2.class) Helper h) { }

    public void testOk() {
        Helper h = new Helper();
        acceptHelperInState1(h);
        transit(h);
        acceptHelperInState2(h);
    }

    public void testError() {
        Helper h = new Helper();
        acceptHelperInState1(h);
        transit(h);
        acceptHelperInState1(h); // error
    }
}

More info

In case of any questions, suggestions, remarks, etc., write me at adam (at) warski (dot) org.