Typestate Inference for Mungo : Algorithm and Implementation

Abstract

We present a usage inference algorithm for the Mungo language. Mungo is an object-orientedprogramming language with usage annotations describing the permitted sequence of method callson objects. A typestate in Mungo is a class name and a usage, and describes the type of anobject. The type system for Mungo ensures that well typed programs follows the specified usagesof all classes, and that null-dereferencing cannot occur at runtime. We show that the inferencealgorithm correctly infers the principal usage, the largest usage that does not result in runtimeerrors. Furthermore we show that a class is well-typed with an inferred usage. We present animplementation of both the type system and the inference algorithm, and provide an analysis ontime and space complexity of both the algorithm and the inferred usage.