Paper Info
Title
Typestates for Objects
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.
Year
DOI
Venue
2004
10.1007/978-3-540-24851-4_21
Lecture Notes in Computer Science
Keywords
Field
DocType
object oriented,object oriented programming,programming model
Programming language,Programming paradigm,Aspect-oriented programming,Object-oriented programming,Computer science,Typestate analysis,Type theory,Theoretical computer science,Compiler,Virtual function,Software development
Conference
Volume
ISSN
Citations 
3086
0302-9743
87
PageRank 
References 
Authors
4.62
15
2
Name
Order
Citations
PageRank
Robert DeLine12957210.35
Manuel Fähndrich21559116.28