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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Reus, B., & Schwinghammer, J. (2005). Denotational semantics for Abadi and Leino’s Logic of objects. In Lecture Notes in Computer Science (Vol. 3444, pp. 263–278). Springer Verlag. https://doi.org/10.1007/978-3-540-31987-0_19
Mendeley helps you to discover research relevant for your work.