Many object-oriented libraries require their clients to follow state machine protocols, and typestate analyses have been developed to check conformance to these protocols. Prior work on typestate specication and analysis, however, has been divorced from the static and dynamic semantics of the language. This results in duplicated mechanisms in the type system and typestate checker, complicates reasoning, and prevents programmers from directly expressing their state-based designs in the language.

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.

43 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu