Please use this identifier to cite or link to this item:
Title: Universe types for topology and encapsulation
Other Titles: Formal methods for components and objects. FMCO 2007. Lecture notes in computer science
Authors: Cunningham, Dave
Dietl, Werner
Drossopoulou, Sophia
Francalanza, Adrian
Muller, Peter
Summers, Alexander J.
Keywords: Object-oriented methods (Computer science)
Real-time data processing
Computer algorithms
Autonomous distributed systems
Issue Date: 2008
Publisher: Springer, Berlin, Heidelberg
Citation: Cunningham, D., Dietl, W., Drossopoulou, S., Francalanza, A., Müller, P., & Summers, A. J. (2008) Universe types for topology and encapsulation. In F.S. de Boer, M.M. Bonsangue, S. Graf, WP. de Roever (Eds.) Formal Methods for Components and Objects. FMCO 2007. Lecture Notes in Computer Science, vol 5382. Springer, Berlin, Heidelberg.
Abstract: 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.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
Universe_Types_for_Topology_and_Encapsulation.pdf330.62 kBAdobe PDFView/Open

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.