Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Typestates for objects

Robert DeLine and Manuel Fähndrich

Abstract

Today's mainstream object-oriented compilers and tools do not support declaring and statically checking simple pre- and postconditions on methods and invariants on object representations. The main technical problem preventing static verification is reasoning about the sharing relationships among objects as well as where object invariants should hold. We have developed a programming model of typestates for objects with a sound modular checking algorithm. The programming model handles typical aspects of object-oriented programs such as downcasting, virtual dispatch, direct calls, and subclassing. The model also permits subclasses to extend the interpretation of typestates and to introduce additional typestates. We handle aliasing by adapting our previous work on practical linear types developed in the context of the Vault system. We have implemented these ideas in a tool called Fugue for specifying and checking typestates on Microsoft .NET-based programs.

Details

Publication typeInproceedings
Published inECOOP 2004 — Object-Oriented Programming, 18th European Conference
Pages465-490
Volume3086
SeriesLecture Notes in Computer Science
PublisherSpringer Verlag
> Publications > Typestates for objects