# Mungo

A research topic for typechecking protocols in object oriented languages

# What is Mungo?

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.

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18  typestate FileProtocol { Init = { Status open(): } Open = { BooleanEnum hasNext(): , void close(): end } Read = { void read(): Open } Close = { void close(): end } }

# Tools

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.

# Mungo related publications

Quickly discover relevant content by filtering publications.

### Papaya: Global Typestate Analysis of Aliased Objects Extended Version

Typestates are state machines used in object-oriented programming to specify and verify correct order of method calls on an object. To …

### Coping with the reality: adding crucial features to a typestate-oriented language

Detecting programming errors and vulnerabilities in software is increasingly important, and building tools that help with this task is …

### Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language

We present a type-based analysis ensuring memory safety and object protocol completion in the Java-like language Mungo. Objects are …

# Tutorial

#### Scala-Mungo

Tutorial session and exercises for the Scala Mungo implementation

#### Mungo with Behavioural Separation

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.

#### Bookstore

We illustrate the toolchain by means of a bookstore (two-buyer) example, which models two buyers coordinationg to buy a book from a seller.

#### Travel Agency

We illustrate the toolchain by means of a travel agency example, which models the process of booking a flight through a university travel agent.

#### DisCoTec Tutorial

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.

# Contact

• School of Computing Science, University of Glasgow, Sir Alwyn Williams Building, 18 Lilybank Gardens, Glasgow, Strathclyde, G12 8RZ