Mungo is a research topic for adding usage-protocols to Java-like languages, and verifying that they are adhered to i.e. that methods are called in the correct order. 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. A number of tools has been developed within this topic. One such tool is a Java frontend tool that at statically verifies that the protocol is followed at runtime.
Consider the typestate below, that models the protocol of a file. Initially only the open method can be called. Afterwards we can check if data is available in the file, and there is, read it. Otherwise the file can only be closed.
|
|
The research project has resulted in a number of tools.
The following video shows how the StMungo and Mungo toolchain work together to statically typecheck the Simple Mail Transfer Protocol (SMTP), and communicate with the gmail server.
Tutorial session and exercises for the Scala Mungo implementation
We illustrate the Mungo prototype with support for behavioural separation, and shows how behavioural separation helps writing more concise protocols
We illustrate the toolchain by means of an adder protocol example, which models a client requesting two numbers to be added by a server.
We illustrate the toolchain by means of a bookstore (two-buyer) example, which models two buyers coordinationg to buy a book from a seller.
We illustrate the toolchain by means of a travel agency example, which models the process of booking a flight through a university travel agent.
This tutorial gives a more in depth overview of the [St]Mungo toolchain through several examples. It has been first presented as part of the DisCoTec 2020 tutorial series.