Semantics and logic of object calculi

The main contribution of this paper is a formal characterization of recursive object specifications based on a denotational untyped semantics of the object calculus and the discussion of existence of those (recursive) specifications. The semantics is then applied to prove soundness of a programming logic for the object calculus and to suggest possible extensions. For the purposes of this discussion we use an informal logic of predomains in order to avoid any commitment to a particular syntax of specification logic.