File(s) not publicly available
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.
History
Publication status
- Published
ISSN
0302-9743Publisher
SpringerVolume
3444Pages
16.0Presentation Type
- paper
Event name
14th European Symposium on Programming (ESOP), LNCSEvent location
EdinburghEvent type
conferenceISBN
3-540-25435-8Department affiliated with
- Informatics Publications
Notes
Originality: presents a new way to obtain the soundness result of a given calculus for objects; this also allows the analysis of the strengths and weaknesses of the logic. Rigour: full mathematical model and proof Impact: cited (with its journal version) as only serious attempt to understand logic for higher-order store denotationally Significance: potential blueprint for correctness proofs of similar logics Outlet/citations: ESOP is a respected conference and had 24.6% acceptance rate that year.Full text available
- No
Peer reviewed?
- Yes
Editors
M SagivLegacy Posted Date
2012-02-06Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC