Substructural typestates

Finding simple, yet expressive, verification techniques to reason about both aliasing and mutable state has been a major challenge for static program verification. One such approach, of practical relevance, is centered around a lightweight typing discipline where types denote abstract object states, known as typestates. In this paper, we show how key typestate concepts can be precisely captured by a substructural type-and-effect system, exploiting ideas from linear and separation logic. Building on this foundation, we show how a small set of primitive concepts can be composed to express high-level idioms such as objects with multiple independent state dimensions, dynamic state tests, and behaviororiented usage protocols that enforce strong information hiding. By exploring the relationship between two mainstream modularity concepts, state abstraction and hiding, we also provide new insights on how they naturally fit together and complement one another. Technically, our results are based on a typed lambda calculus with mutable references, location-dependent types, and secondorder polymorphism. The soundness of our type system is shown through progress and preservation theorems. We also describe a prototype implementation of a type checker for our system, which is available on the web and can be used to experiment with the examples in the paper. Categories and Subject Descriptors D.3.3 [Programming Languages]: Abstract Data Types; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs.