Semantics and Logic of Object Calculi

On top of a denotational semantics for Abadi & Cardelli's untyped object calculi we discuss the concept of object specification. Along the lines of Pitts' results on relational properties of domains we prove existence of object specifications under certain assumptions. The proof technique applies to the functional and the imperative object calculus. Correctness of the Abadi & Leino object logic can be seen as a corollary of the existence theorem. Variations of this theorem could simplify soundness checks on other object-oriented verification systems. For the purposes of the discussion we use an informal logic of predomains in order to avoid any commitment to a particular syntax or style.