Semantics and logic of object calculi

The main contribution of this paper is a formal characterization of recursive object specifications and their existence based on a denotational untyped semantics of the object calculus. Existence is not guaranteed but can be shown employing Pitts’ results on relational properties of domains. The sem...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2004-05, Vol.316 (1), p.191-213
Main Authors: Reus, Bernhard, Streicher, Thomas
Format: Article
Language:English
Subjects:
Denotational semantics
Domain theory
Object logic
Program verification
Programming logic
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The main contribution of this paper is a formal characterization of recursive object specifications and their existence based on a denotational untyped semantics of the object calculus. Existence is not guaranteed but can be shown employing Pitts’ results on relational properties of domains. The semantics can be used to analyse and verify Abadi and Leino's object logic but it also suggests extensions. For example, specifications of methods may not only refer to fields but also to methods of objects in the store. This can be achieved without compromising the existence theorem. An informal logic of predomains is in use intentionally in order to avoid any commitment to a particular syntax of specification logic.
ISSN:0304-3975
1879-2294
DOI:10.1016/j.tcs.2004.01.030