×

Simple ownership types for object containment. (English) Zbl 0982.68763

Lindskov Knudsen, Jørgen (ed.), ECOOP 2001 - Object-oriented programming. 15th European conference, Budapest, Hungary, June 18-22, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2072, 53-76 (2001).
Summary: Containment of objects is a natural concept that has been poorly supported in object-oriented programming languages. For a predefined set of ownership contexts, this paper presents a type system that enforces certain containment relationships for run-time objects. A fixed ordering relationship is presumed between the owners.
The formalisation of ownership types has developed from our work with flexible alias protection together with an investigation of structural properties of object graphs based on dominator trees. Our general ownership type system permits fresh ownership contexts to be created at run-time. Here we present a simplified system in which the ownership contexts are predefined. This is powerful enough to express and enforce constraints about a system’s high-level structure.
Our formal system is presented in an imperative variant of the object calculus. We present type preservation and soundness results. Furthermore we highlight how these type theoretic results establish a containment invariant for objects, in which access to contained objects is only permitted via their owners. In effect, the predefined ownership ordering restricts the permissible inter-object reference structure.
For the entire collection see [Zbl 0968.68558].

MSC:

68U99 Computing methodologies and applications
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N15 Theory of programming languages

Software:

Eiffel; Virginity
PDF BibTeX XML Cite
Full Text: Link