Gradual Featherweight Typestate (CMU-ISR-10-116R)

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 classesas-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.