Modular Typestate Verification of Aliased Objects

摘要

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.