Foundations of Typestate-Oriented Programming
Abstract
Typestate reflects how the legal operations on imperative objects can change at runtime as their internal statechanges. A typestate checker can statically ensure, for instance, that an object method is only called when the object is in a state for which the operation is well-defined. Prior work has shown how modular typestate checking can be achieved thanks to access permissions and state guarantees. However, typestate was not treated as a primitive language concept: typestate checkers are an additional verification layer on top of an existing language. In contrast, a typestate-oriented programming language directly supports expressing typestates. For example, in the Plaid programming language, the typestate of an object directly corresponds to its class, and that class can changedynamically. Plaid objects have not just typestate-dependent interfaces, but also typestate-dependent behaviors andruntime representations.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 2014
- Accession Number
- AD1019547
Entities
People
- Jonathan Erik Aldrich
- Roger Wolff
- Ronald Garcia
- Éric Tanter
Organizations
- Carnegie Mellon University