Institute for Software Research
School of Computer Science, Carnegie Mellon University
Ronald Garcia, Roger Wolff,
Éric Tanter*, Jonathan Aldrich
Keywords: Access permissions, state guarantees
Typestate oriented programming integrates notions of typestate directly
into the semantics of an object-oriented programming language. This
document presents the formalization of Featherweight
Typestate, a typestate oriented language modeled after Featherweight Java.
This language supports a classes-as-states model of typestates, and
utilizes a flow-sensitive type system for checking access permissions and
state guarantees, thereby enabling safe and modular typestate checking.
The syntax and both static and dynamic semantics of Featherweight
Typestate are presented, as well as a proof of type safety.
*PLEIAD Laboratory, Computer Science Department, University of Chile