Sciweavers

Share
ESOP
2005
Springer

Denotational Semantics for Abadi and Leino's Logic of Objects

10 years 7 months ago
Denotational Semantics for Abadi and Leino's Logic of Objects
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.
Bernhard Reus, Jan Schwinghammer
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where ESOP
Authors Bernhard Reus, Jan Schwinghammer
Comments (0)
books