Tools

StMungo Source on Bitbucket

StMungo (Scribble-to-Mungo) is a Java-based tool used to translate Scribble local protocol specifications into typestate specifications. It is implemented using the ANTLR v4.5 framework. After the translation, we use Mungo to statically typecheck the protocol implementation.

We start from a distributed multiparty protocol defined as Scribble global protocol and then use the Scribble tools to validate and project into a local protocol describing the interactions from the point of view of one participant. For every participant, there is a local projection.

For every Scribble local protocol, StMungo produces Mungo files containing:

  • a typestate specification describing the local protocol as a sequence of method calls,
  • a Java API for the participant implementing the methods in the typestate, and
  • a main() method skeleton calling the methods in the typestate.

Mungo Source on Bitbucket

Mungo is a Java front-end tool used to statically check the order of method calls. It is implemented using the JastAdd framework. A protocol definition is described as a sequence of method calls, the order of which determines the validity of the protocol.

A typestate file is defined and associated to a class. The Mungo tool checks that the object instantiating the class performs method calls by following its declared typestate. If the object respects the typestate, the code can be compiled and run as standard Java code. If the typestate is violated, Mungo reports the errors.

Java Typestate Checker Source on Github

The Java Typestate Checker is a plugin for the Checker Framework. This plugin allows one to statically ensure that method calls are called in the correct order. The sequences of method calls allowed are specified in a protocol file which is associated with a Java class by adding a @Typestate annotation to the class.

This tool in inspired in the Mungo tool. It is a new implementation which includes new features and improvements over the current version of Mungo. A comparison table between Mungo and this tool is available here.

Mungoi and Mungob Source on Github

Mungoi and Mungob are two prototype implementations of a fully formalized core object oriented language, with typestate annotations. Mungoi supports typestate inference, where the most permissible typestate is inferred from a class definition. Mungob supports behavioural separation to lessen the linearity constraint present in other versions of Mungo. Through a parallel construct, a parallel typestate can be split into two constituents, which each can be used separately and later be joined back together.

Papaya Source on Github

Papaya is an implementation for Scala of global typestate analysis allowing unrestricted aliasing. It is implemented as a compiler library for Scala, allowing it to be embedded into real-life programs, verifying at compile time that protocols are being adhered to by all instances. The protocols are expressed as singleton classes and thus are written in Scala itself. Using the @Typestate annotation a protocol is linked to a class, and the tool will generate errors or warning if instances of this class does not respect the protocol, or if a protocol is potentially left unfinished.