Reus, Bernhard and Schwinghammer, Jan (2005) Denotational semantics for Abadi and Leino's logic of objects. In: Sagiv, Mooly (ed.) Programming Languages and Systems: Proceedings of the 14th European Symposium on Programming, ESOP 2005, Edinburgh, UK. Lecture Notes in Computer Science, 3444 . Springer, pp. 263-278. ISBN 9783540254355

PDF Restricted to SRO admin only Download (243kB)

Abstract

Abadi-Leino Logic is a Hoare-calculus style logic for a simple imperative and object-based language where every object comes with its own method suite. Consequently, methods need to reside in the store (rdquohigher-order storerdquo). We present a new soundness proof for this logic using a denotational semantics where object specifications are recursive predicates on the domain of objects. Our semantics reveals which of the limitations of Abadi and Leinorsquos logic are deliberate design decisions and which follow from the use of higher-order store. We discuss the implications for the development of other, more expressive, program logics.

Item Type:	Book Section
Schools and Departments:	School of Engineering and Informatics > Informatics
Subjects:	Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User:	Chris Keene
Date Deposited:	03 Mar 2008
Last Modified:	24 Sep 2019 12:39
URI:	http://sro.sussex.ac.uk/id/eprint/1429
Google Scholar:	8 Citations

View download statistics for this item

📧 Request an update