Reus, Bernhard and Schwinghammer, Jan (2005) Denotational semantics for Abadi and Leino's logic of objects. In: 14th European Symposium on Programming (ESOP), LNCS, Edinburgh.

Full text not available from this repository.

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 ("higher-order store"). 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 Leino's 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:	Conference or Workshop Item (Paper)
Additional Information:	Originality: presents a new way to obtain the soundness result of a given calculus for objects; this also allows the analysis of the strengths and weaknesses of the logic. Rigour: full mathematical model and proof Impact: cited (with its journal version) as only serious attempt to understand logic for higher-order store denotationally Significance: potential blueprint for correctness proofs of similar logics Outlet/citations: ESOP is a respected conference and had 24.6% acceptance rate that year.
Schools and Departments:	School of Engineering and Informatics > Informatics
Depositing User:	Bernhard Reus
Date Deposited:	06 Feb 2012 20:18
Last Modified:	24 Sep 2019 12:37
URI:	http://sro.sussex.ac.uk/id/eprint/25293

📧 Request an update