JaTyC

The Java Typestate Checker (JaTyC) is a tool that verifies Java source code with respect to typestates. A typestate is associated with a Java class with the @Typestate annotation and defines: the object's states, the methods that can be safely called in each state, and the states resulting from the calls. The tool statically verifies that when a Java program runs: sequences of method calls obey the object's protocols; objects' protocols are completed (if the program terminates); null-pointer exceptions are not raised; and subclasses' instances respect the protocol of their superclasses.

JaTyC is a plugin for the Checker Framework. It is a purely transparent checker, i.e., it does not modify the baseline Java compilation. This tool was inspired by the Mungo toolset. It is a new implementation that includes new features and improvements over the current version of Mungo.

The core features are:

• checking that methods are called in the correct order specified by the protocol;
• checking that protocols of objects are completed (if the program terminates);
• checking the absence of null pointer errors;
• support for subtyping;
• support for protocols to be associated with classes from the standard Java library or from third-party libraries;
• support for "droppable" states, which allow one to specify states in which an object may be "dropped" (i.e., stop being used) without having to reach the final state;
• support for transitions of state to depend on boolean values or enumeration values returned by methods.
• invalid sequences of method calls are ignored when analyzing the use of objects stored inside other objects by taking into account that the methods of the outer object will only be called in the order specified by the corresponding protocol, thus avoiding false positives.

What inputs are supported?

Java, Typestate specifications

For which programming languages has it support?

Java

What properties can be verified?

JaTyC statically verifies that when a Java program runs: sequences of method calls obey the object's protocols; objects' protocols are completed (if the program terminates); null-pointer exceptions are not raised; and subclasses' instances respect the protocol of their superclasses.

What are the tool’s main techniques for the supported (input, property) pairs?

JaTyC performs syntax-directed type-checking relying on minimal annotations and typestate specifications associated with classes.

What external tools are used? (e.g., compilers, SMT solvers)

JaTyC relies on the Checker Framework.

What is the tool’s URL?

https://github.com/jdmota/java-typestate-checker provides source code, documentation, installation instructions, built JAR files, examples, publications, and other resources.

Example(s)

Examples are available in the examples folder of the repository: https://github.com/jdmota/java-typestate-checker/tree/master/examples

References

Available at https://github.com/jdmota/java-typestate-checker#publications