CMU-ISR-10-115
Institute for Software Research
School of Computer Science, Carnegie Mellon University



CMU-ISR-10-115R2

Featherweight Typestate

Ronald Garcia, Roger Wolff,
Éric Tanter*, Jonathan Aldrich

July 2010
Updated May 2012

Supercedes CMU-ISR-10-115

CMU-ISR-10-115R2.pdf


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.

32 pages


*PLEIAD Laboratory, Computer Science Department, University of Chile


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu