Computing Publications

Publications Home » Universe Types for Topology and E...

Universe Types for Topology and Encapsulation

David Cunningham, Werner Dietl, Sophia Drossopoulou, Adrian Francalanza, Peter , Alexander Summers

Journal Special Issue Article
Formal Methods for Components (FMCO) 2007
Lecture Notes in Computer Science
Volume 5382
Springer Verlag
ISBN 978-3-540-92187-5
DOI 10.1007/978-3-540-92188-2_4

The Universe Type System is an ownership type system for object-oriented programming languages that hierarchically structures the object store; it is used to reason modularly about programs. We formalise Universe Types for a core subset of Java in two steps: We first define a Topological Type System that structures the object store hierarchically into an ownership tree, and demonstrate soundness of the Topological Type System by proving subject reduction. Motivated by concerns of modular verification, we then present an Encapsulation Type System that enforces the owner-as-modifier discipline; that is, that object updates are initiated by the owner of the object. The contributions of this paper are, firstly, an extensive type-theoretic account of the Universe Type System, with explanations and complete proofs, and secondly, the clean separation of the topological from the encapsulation concerns.

Program Verification
PDF of full publication (348 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.