Modular Typestate Verification of Aliased Objects
Abstract
A number of type systems have used typestates to specify and statically verify protocol compliance. Aliasing is a major challenge for these systems. This paper proposes a modular type system for a core object-oriented language that leverages linear logic for verifying compliance to more expressive protocol specifications than previously supported. The system improves reasoning about aliased objects by associating references with access permissions that systematically capture what aliases know about and can do to objects. Permissions grant full, shared, or read-only access to a certain part of object state and allow aliasing both on the stack and in the heap. The system supports dynamic state tests, arbitrary callbacks, and open recursion. The system's expressiveness is illustrated with examples from the Java I/O library.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 01, 2007
- Accession Number
- ADA465507
Entities
People
- Jonathan Erik Aldrich
- Kevin Bierhoff
Organizations
- Carnegie Mellon University