Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/23185| Title: | UJ : type soundness for universe types |
| Other Titles: | Formal methods for components and objects |
| Authors: | Cunningham, Dave Francalanza, Adrian Drossopoulou, Sophia Dietl, Werner Muller, Peter |
| Keywords: | Object-oriented methods (Computer science) Real-time data processing Autonomous distributed systems Formal methods (Computer science) |
| Issue Date: | 2008 |
| Publisher: | Springer-Verlag |
| Citation: | Cunningham, D., Dietl, W., Drossopoulou, S., Francalanza, A., & Müller, P. (2008). UJ: type soundness for universe types. In F. S. de Boer, M. M. Bonsangue, S. Graf, & W.-P. de Roever (Eds.), Formal Methods for Components and Objects (pp. 1-31). Berlin: Springer-Verlag. |
| Abstract: | Universe types characterise aliasing in object oriented programming languages and are used to reason modularly about programs. In this report we formalise prior work by M ̈uller and Poetzsch-Heffter, who designed the Universe Type System for a core subset of Java. We present our work in two steps. We first give a Topological Universe Type System and show subject reduction to a small-step dynamic semantics for our language. Motivated by concerns of Modular verification, we then give an Encapsulation Universe Type System (based on the owner-as-modifier principle), prove subject reduction with respect to the former small-step semantics, and show how the type system can be used for modular verification. |
| URI: | https://www.um.edu.mt/library/oar//handle/123456789/23185 |
| Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| UJ_Type_Soundness_for_Universe_Types (1).pdf | 315.37 kB | Adobe PDF | View/Open |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.