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|
Summers, Alexander J.
|Keywords:||Object-oriented methods (Computer science)|
Real-time data processing
Autonomous distributed systems
|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:
|Universe_Types_for_Topology_and_Encapsulation.pdf||330.62 kB||Adobe PDF||View/Open|
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.