logo [St]Mungo

What is Mungo?

Mungo is a Java front-end tool that statically checks the order of method calls. It is based on the notion of typestate describing non-uniform objects, where the availability of methods to be called depends on the state of the object. Hence, the typestate defines an object protocol. The Mungo tool checks that the object conforms to its specified typestate, namely object protocol.

What is StMungo?

StMungo (Scribble to Mungo) is a transpiler from Scribble protocol specifications (similar to session types) into typestate specifications. After the traslation, the Mungo tool can be used to statically check the order of methods calls, namely the object protocol.

The following video shows how the StMungo and Mungo toolchain work together to statically typecheck the Simple Mail Transfer Protocol (SMTP), and communciate with the gmail server.

Use case

The FileProtocol typestate describes a protocol on a file object. It imposes an order in which the methods of a file object should be called.

The first method available to be called on a file is open().

Depending on the return state of this method call, there is a transition either to a state where the file is open or to the end state, denoting the terminatation of the protocol.

Once the file is open, being in the Open state, there are two methods available for a call, hasNext() and close(). The latter terminates the protocol.

Depending on the return state of the hasNext() call, there is a transition either to a state where method read() or method close() can be called.

If read() is called this returns to the Open state. If close() is called the protocol terminates with the end state.

typestate FileProtocol {

    Init =  {
        Status open(): <OK: Open, ERROR:end>
    }

    Open =  {
        Boolean hasNext(): <TRUE: Read, FALSE: Close>,
        void close(): end
    }

    Read =  {
        void read(): Open
    }

    Close = {
        void close(): end
    }
}