Gradual Featherweight Typestate

Typestate oriented programming integrates notions of typestate directly into the semantics of an object-oriented programming language. This document presents the formalization of Feather-weight 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 check-ing access permissions and state guarantees, thereby enabling safe and modular typestate check-ing. The syntax and both static and dynamic semantics of Featherweight Typestate are presented, as well as a proof of type safety.