Typestate checker – introduction

3 Flares 3 Flares ×

When dealing with mutable objects in Java, we quite often see that “states” of the class considered emerge. The (abstract) “state” depends of course on the content of the fields of the object. When methods are invoked, which mutate the fields, the state of the object may change. Also, it may be illegal to call some methods in one state, but legal in another.

So far, specifying the state space of an object, which methods can be called in which states, and how methods change the state, is done mainly in comments (javadocs). With the new possibilities brought by JSR 308 – type annotations, it’s now possible to do it in a much more structured way.

The basic idea is simple. Each state of our object is one annotation. We can define those annotations for example as inner classes. There are 2 immediate gains:

  • we enumerate all the states of our object, so the state space is well defined;
  • each state can be commented, so we have a very good place to describe when an object is in the given state and what does it mean.

As an example, let’s assume that we have a class for reading a remote resource, for example RemoteResourceReader. Objects of this class can be in one of the three states:

  • configuration – connection to the resource is being configured
  • open – connection to the resource is open, data can be read
  • closed – the connection is closed, data cannot be read

The inital state is configuration, in which we set the connection properties, like the URL, username, password, etc. Then, we can change the state to open, read some data, and close the connection, changing the state to closed. After that, we may re-open the connection to read more data, etc.

So how would the source of our class look like? First, we define the states:

1
2
3
4
5
6
7
8
9
10
public class RemoteResourceReader {
/** Connection to the resource is being configured */
public static @interface Configuration { }
/** Connection to the resource is open, data can be read */
public static @interface Open { }
/** Connection to the resource is closed, data cannot be read */
public static @interface Closed { }
 
(...)
}

Now, we have to specify what is the initial state and how methods change the state. Thanks to JSR 308, that is easy. Type annotations extend the number of places, where annotations are allowed; you may place them on any type. See its web page for more information.

One of the new places, where annotations are allowed, is the “method receiver”. This lets you specify meta-data (annotations) that apply to the object, on which the method is called. For example, we want to specify that the read method can be invoked on an object only when it is in the open state; similarly, the setURL method can be invoked only when the object is in the configuration state. Using JSR308, we can write it like this:

1
2
3
4
(...)
public String read() @Open { ... }
public void setURL(String newURL) @Configuration { ... }
(...)

However, to keep the code compatible with Java 5/6, we may place the annotations in comments. They will still be recognized by the JSR308 checker framework (why this is important – read on :) ).

Finally, what about state changes? Here, we also use the method receiver annotations. We may add an element to our state annotations, which will specify the state of the object after the method invocation. For example:

1
2
3
4
5
(...)
public void open() @Configuration(after=Open.class)
@Closed(after=Open.class) { ... }
public void close() @Open(after=Closed.class) { ... }
(...)

We have specified that:

  • we can invoke the open method, if the object was in the configuration or closed states. After invoking this method, the object will be in the open state
  • we can invoke the close method, only if the object was in the open state. After invoking this method, the object will be in the closed state

What are the benefits of using state annotations so far? Improved documentation: users immediately see in what states objects of the class can be, when it is legal to call a method and how the states change. However, there is more: you can check if your objects are in the correct state by using the typestate checker!

The typestate checker is built on top of the checkers framework, which out-of-the box provides other very useful checkers, for nullness and immutability. Be sure to try them out :).

To use the typestate checker, go here for downloads and installation instructions. The only additional requirement is that you must annotate your state annotations with @State. The checker will verify, using flow analysis, if you invoke methods on objects in the correct state, pass parameters in the correct state etc. This version of the checker should be treated more like a proof-of-concept, than as a final version. It is in a very early development stage, so your comments and experiences are very welcome! :)

To complete the RemoteResourceReader example, here is a full version of the class, ready to be used with the typestate checker:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
public class RemoteResourceReader {
/** Connection to the resource is being configured */
@State public static @interface Configuration {
Class<?> after default Object.class }
/** Connection to the resource is open, data can be read */
@State public static @interface Open {
Class<?> after default Object.class }
/** Connection to the resource is closed, data cannot be read */
@State public static @interface Closed {
Class<?> after default Object.class }
 
// Initial state of the object - specified in the
// constructor's receiver annotation
public RemoteResourceReader() /*@Configuration*/ { ... }
 
public void setURL(String newURL) /*@Configuration*/ { ... }
 
public void open() /*@Configuration(after=Open.class)*/
/*@Closed(after=Open.class)*/ { ... }
 
public String read() /*@Open*/ { ... }
 
public void close() /*@Open(after=Closed.class)*/ { ... }
}

Finally, here is some example code which demonstrates what errors are caught by the typestate checker:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
void readMore(@Open RemoteResourceReader rrr) { ... }
 
void test() {
// initially in the 'configuration' state
RemoteResourceReader rrr = new RemoteResourceReader();
 
// ok: correct state
rrr.setUrl("http://something");
 
// error: not in the 'open' state
rrr.close();
 
// changing state from 'configuration' to 'open'
rrr.open();
 
// ok
String read = rrr.read();
 
// error: not in the 'configuration' state
rrr.setUrl("http://different");
 
// ok: parameter in the 'open' state
readMore(rrr);
 
// ok
rrr.close();
 
// error: parameter not in the correct state
readMore(rrr);
}

If you’d like to make experiments with the typestate checker on your own, go ahead and download it. The setup is really easy. And remember, that your feedback is very valuable and important!

I’d like to thank Michael Ernst and the rest of the JSR308 team for helping me with some questions that I had during development. The specification and framework is really good and worth taking a look at :)

Adam

  • Corneil du Plessis

    Another way to describe the states would be an Enum.
    Then use:
    public enum States {
    Configuration,
    Open,
    Closed
    };
    @State(state=States.Configuration, endState=States.Open)
    public void open();
    Or
    @State(required=States.Open, endState=States.Closed)
    public void close();

    A proxy could be generated to do the state checking…

  • http://www.warski.org Adam Warski

    Hello,
    yes, that would be possibly nicer, however the @State annotation would then have to be redefined for each state-defining enum, as an annotation element cannot be “an” enum, but a concrete enum.

    Adam

  • Pingback: Blog of Adam Warski » Blog Archive » New features in Typestate Checker

3 Flares Twitter 2 Facebook 1 Google+ 0 LinkedIn 0 Email -- 3 Flares ×