Publication details

Saarland University Computer Science

Denotational Semantics for Abadi and Leino's Logic of Objects

Bernhard Reus, Jan Schwinghammer

The European Symposium on Programming (ESOP'05), Vol. 3444 of LNCS, pp. 264--279, Springer, April 2005

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.

Superseded by MSCS journal version.

Download PDF        Show BibTeX               


Login to edit


Legal notice, Privacy policy