Publication details

Saarland University Computer Science

Denotational Semantics for a Program Logic of Objects

Bernhard Reus, Jan Schwinghammer

Mathematical Structures in Computer Science 16(2):313-358, April 2006

The object-calculus is an imperative and object-based programming language where every object comes equipped with its own method suite. Consequently, methods need to reside in the store (``higher-order store'') which complicates the semantics. Abadi and Leino defined a program logic for this language enriching object types by method specifications. We present a new soundness proof for their logic using Denotational Semantics. It turns out that denotations of store specifications are predicates defined by mixed-variant recursion. A benefit of our approach is that derivability and validity can be kept distinct. Moreover, it is revealed which of the limitations of Abadi and Leino's logic are incidental design decisions and which follow inherently from the use of higher-order store. We discuss the implications for the development of other, more expressive, program logics.

revised and expanded version of ESOP'05 paper, "Denotational Semantics for Abadi and Leino's Logic of Objects"

Download PDF        Show BibTeX               

Login to edit

Webmaster, Wed Sep 16 10:47:00 2009