The main contribution of this paper is a formal characterization of
recursive object specifications based on a denotational untyped
semantics of Abadi & Cardelli's object calculus and the discussion
of existence of those (recursive) specifications.
The existence theorem uses domain theoretical machinery known from the
work of Freyd and Pitts.
The semantics is then applied to prove soundness of a programming
logic for the object calculus (by Abadi & Leino) 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 special syntax of
specification logic
