logo 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 a 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, then .java files are produced, for every .mungo file in the program. Finally, the Java tools can be used to compile and run the standard Java code. If the typestate is violated, Mungo reports the errors.

The following video shows Mungo at work on SMTP.

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
    }
}