Typestate: A programming language concept for enhancing software reliability

TLDR

Typestate refines the type system by specifying which operations are allowed in a given context, thereby enabling detection of errors such as using uninitialized variables or dereferencing freed pointers. The authors introduce typestate as a new programming language concept, define it, provide application examples, and demonstrate how typestate checking can be integrated into a compiler. Typestate tracking is a compile‑time program analysis that identifies syntactically legal but semantically undefined execution sequences, and the authors illustrate its implementation within a compiler. The authors report that typestate checking enhances software reliability and influences software structure, and they share their experience using a high‑level language that incorporates typestate checking.

Abstract

The authors introduce a new programming language concept, called typestate, which is a refinement of the concept of type. Whereas the type of a data object determines the set of operations over permitted on the object, typestate determines the subset of these operations which is permitted in a particular context. Typestate tracking is a program analysis technique which enhances program reliability by detecting at compile-time syntactically legal but semantically undefined execution sequences. These include reading a variable before it has been initialized and dereferencing a pointer after the dynamic object has been deallocated. The authors define typestate, give examples of its application, and show how typestate checking may be embedded into a compiler. They discuss the consequences of typestate checking for software reliability and software structure, and summarize their experience in using a high-level language incorporating typestate checking.