University of Sussex
Browse

File(s) under permanent embargo

Denotational semantics for Abadi and Leino's logic of objects

chapter
posted on 2023-06-07, 14:13 authored by Bernhard ReusBernhard Reus, Jan Schwinghammer
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 (rdquohigher-order storerdquo). 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 Leinorsquos 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.

History

Publication status

  • Published

Journal

The European Symposium on Programming

Publisher

Springer

Volume

3444

Page range

263-278

Pages

439.0

Book title

Programming Languages and Systems: Proceedings of the 14th European Symposium on Programming, ESOP 2005, Edinburgh, UK

ISBN

9783540254355

Series

Lecture Notes in Computer Science

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Editors

Mooly Sagiv

Legacy Posted Date

2008-03-03

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC