Institute for Software Research
School of Computer Science, Carnegie Mellon University
A Theory of Typestate-Oriented Programming
Darpan Saini, Joshua Sunshine, Jonathan Aldrich
In this paper we present Plaidcore,a core calculus that embodies typestate-oriented programming by integrating typestate directly into the programming language and its type system. Plaidcore's typestate change operator allows the representation of objects to change at run time, and uses a type system based on access permissions to statically guarantee that clients use object protocols correctly. We introduce the features of the calculus with examples, formally dene its static and dynamic semantics, and prove type soundness. Based on this firm typing foundation, typestate-oriented programming has the potential to help engineers more easily specify and enforce protocol constraints, leading to more reliable software.