Convention Ctr - Ballroom 6D

The papers in this session present mathematical foundations for reasoning about object-oriented software. Each paper gives a type-based analysis that can prove key properties of a program. The first paper concerns proving that two statements have disjoint effects and that two expressions cannot lead to aliases. The second paper presents an extension of Java in which one can specify and check information about owners and ownership of objects. The third paper shows an approach to modeling components and enforcing COM conformance. Each paper contains key correctness theorems, including type soundness.

Ownership types provide a statically enforceable notion of object-level encapsulation in object-oriented programs. We extend ownership types with computational effects, so as to support reasoning about object-oriented programs. The ensuing system itself provides both access control and effects reporting. Based on this type system, we codify two formal systems for reasoning about aliasing and the disjointness of computational effects. The first can be used to prove that evaluation of two expressions will never lead to aliases, while the latter can be used to show the noninterference of two expressions.

Building and evolving a large software system is challenging in part because it is difficult to understand the system architecture: how the system breaks down into parts, and how those parts interact. One of the primary challenges in understanding the software architecture of an object-oriented program is dealing with aliasing between objects. Unexpected aliasing can lead to broken invariants, mistaken assumptions, security holes, and surprising side effects, all of which may lead to software defects and complicate software evolution. This paper presents AliasJava, an alias annotation system for Java that makes alias patterns explicit in the source code, enabling developers to reason more effectively about the interactions in a complex system. We describe our implementation, prove the soundness of the annotation system, and give an algorithm for automatically inferring alias annotations. Our experience suggests that the annotation system is practical, that annotation inference yields appropriate annotations, and that the annotations can express important invariants of data structures and of software architectures.

We introduce in this paper a typed calculus intended to capture the execution model of COM. The innovation of this calculus is to model very low-level aspects of the COM framework, specifically the notion of interface pointers. This is handled by specifying an allocation semantics for the calculus, thereby modeling heap allocation of interfaces explicitly. Having an explicit way of talking about interface pointers allows us to model in a reasonable way the notions of interface sharing and object identity. We introduce a type system that can be used to disambiguate between specification and implementation of interfaces. The type system moreover can capture a notion of COM conformance, that is, the legality of COM components. We discuss extensions of the calculus to handle subtyping of interfaces, dynamic interface negotiation and aggregation.