A theory of typestate-oriented programming
Darpan Saini, Joshua Sunshine, Jonathan Aldrich · 2010
Engineers in many disciplines use state machines to reason about system changes, and many object-oriented libraries require their clients to follow state machine protocols. No existing language, however, has native support for state machines, and programmers often lose productivity and introduce errors when trying to understand and follow interaction protocols. The Plaid language extends the object paradigm with explicit states and state transitions, in order to better model object state transitions. In this paper, we present P laidcore, a core calculus for Plaid, which uses states and permissions to statically guarantee that clients use object protocols correctly.