Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/23235
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Cunningham, Dave | - |
dc.contributor.author | Dietl, Werner | - |
dc.contributor.author | Drossopoulou, Sophia | - |
dc.contributor.author | Francalanza, Adrian | - |
dc.contributor.author | Muller, Peter | - |
dc.contributor.author | Summers, Alexander J. | - |
dc.date.accessioned | 2017-10-31T13:59:24Z | - |
dc.date.available | 2017-10-31T13:59:24Z | - |
dc.date.issued | 2008 | - |
dc.identifier.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. | en_GB |
dc.identifier.uri | https://www.um.edu.mt/library/oar//handle/123456789/23235 | - |
dc.description.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. | en_GB |
dc.language.iso | en | en_GB |
dc.publisher | Springer, Berlin, Heidelberg | en_GB |
dc.rights | info:eu-repo/semantics/openAccess | en_GB |
dc.subject | Object-oriented methods (Computer science) | en_GB |
dc.subject | Real-time data processing | en_GB |
dc.subject | Computer algorithms | en_GB |
dc.subject | Autonomous distributed systems | en_GB |
dc.title | Universe types for topology and encapsulation | en_GB |
dc.title.alternative | Formal methods for components and objects. FMCO 2007. Lecture notes in computer science | en_GB |
dc.type | bookPart | en_GB |
dc.rights.holder | The copyright of this work belongs to the author(s)/publisher. The rights of this work are as defined by the appropriate Copyright Legislation or as modified by any successive legislation. Users may access this work and can make use of the information contained in accordance with the Copyright Legislation provided that the author must be properly acknowledged. Further distribution or reproduction in any format is prohibited without the prior permission of the copyright holder | en_GB |
dc.description.reviewed | peer-reviewed | en_GB |
dc.identifier.doi | 10.1007/978-3-540-92188-2_4 | - |
Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
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.