Institute for Software Research
School of Computer Science, Carnegie Mellon University
Gradual Featherweight Typestate
Roger Wolff, Ronald Garcia, Éric Tanter*, Jonathan Aldrich
Supercedes Institute for Software Research Technical Reports
Typestate oriented programming integrates notions of typestate directly into the semantics of an objectoriented programming language. This document presents the formalization of Gradual 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.