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 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.
described by its introduction rule w.r.t. object formation.
Therefore, the existence of the specification is equivalent to
the validity of its introduction rule. The resulting implicit
definition of a specification neither guarantees
existence nor uniqueness unless \Phi is of a certain form 1 . It is
Domain Theory that provides sufficient machinery to guarantee
existence and uniqueness. Therefore, working with
a denotational (domain theoretic) semantics puts us into a
position to precisely account for this problem.
As far as the authors are aware, such a systematic denotational
analysis of object logics has not been carried
First author partially supported by the EPSRC under grant
GR/R65190/01 and the Nuffield Foundation under grant NAL/00244/A.
Usually, if \Phi is monotonic then S is recursively defined. But monotonicity
is too strong a condition for object specifications.
through yet although there is a successful role model, the
LCF (Logic of Computable Functions) logic, for the functional
paradigm.
The outline of this paper is as follows. Firstly, a denotational
semantics of the functional and imperative untyped
object calculus of [1] is given. On top of that a notion of
specification inspired by the Abadi & Leino logic [2] is defined
on the resulting object domains. We prove existence
of these specifications under mild assumptions employing
Andy Pitts' machinery for relational properties of domains
[10].
The existence theorem is not only interesting in its own
right, it will be also applied to
ffl prove soundness of the object formation rule in [2] (in
an untyped way but types can be encoded as specifications

ffl exemplify via counterexamples that certain specification
can not exist
suggest extensions of an existing programming logic
[2, 8] introducing method invariants and logic of
higher order store.
Moreover, the proposed technique is expected to be applicable
to various other object-oriented languages and programming
logics.
Some basic ideas date back to a draft [13] an abstract of
which has been published in [14].
Denotational model of the object calculus
In this section we describe a most simple denotational semantics
for functional and imperative object calculi within
the category PreDom of predomains and partial continuous
functions. Let * denote the partial continuous function
space between predomains. By f(a)" we denote that
function f applied to a is undefined whereas f(a)# denotes
definedness.
2.1 Preliminaries
When specifying the recursive types needed for the interpretation
of object calculi we often have to employ record
type formation in the following sense. Let L be a (count-
able) set of labels and A a predomain then the type of
records with entries from A and labels from L is defined
as follows:
where A L is the set of all total functions from L to A. It
is easily seen that RecL is a locally continuous functor on
PreDom. A record with labels l i and corresponding entries
jg. Notice
that RecL (A) is always non-empty as it contains the
element h;; ;i.
Definition 2.1 The update (and extension) operation for
records is defined as in Table 1 (page 3). Selection of a
label a 2 L in a record r 2 RecL (A), short r:a, is defined
yielding f(a) 2 A.
2.2. Functional object calculus
Let us first recall the syntax of the functional object calculus
of [1]. For the sake of simplicity, in the functional
case we do not distinguish between field and method up-date
so and F are sets of method
names and field names, respectively.
object creation
method call
method update
Again, for simplicity, methods do not have additional argu-
ments. This is not a real restriction as arguments can be
encoded by fields. Let BVal denote the flat predomain of
basic values like numbers or booleans. The functional object
calculus most naturally finds its interpretation within
the recursively specified predomain
which is nonempty as record types are always non-empty.
If we choose BVal to be empty then we get the recursive
type of [2]:
and if we consider a variant of object calculus without fields
then we get the most simple recursive type
which strongly reminds one of call-by-value lambda calculus
as given by the type equation L*L. The difference
essentially is that an object is not just a partial continuous
function from objects to objects but a whole record of such.
For an "object" o2O and a "message" the result of
"sending message m to object o" is given by o:m(o) which
is understood as divergent if m does not occur as a label in
the record o. It makes sense to conceive methods as partial
continuous functions from O to O, i.e. as strict functions,
because if o:m is defined then the argument o has to be defined
as well.
For the sake of simplicity, in this paper we will use
the last domain equation to interpret the functional object-
calculus which fits with the convention that in the calculus
we do not distinguish between method and field update. 2
We write [[a]]ae for the interpretation of object expression
a in the environment ae 2 O Var . This interpretation
is defined by structural recursion on object expressions via
the following clauses:
2.3. Imperative object calculus
Recall that the syntax of the imperative untyped object
calculus of [1] is as follows if we distinguish between fields
and methods:
object creation
field selection
field update
method call
method update
clone(a) shallow copy
j letx=a in b local def.
The imperative calculus finds its interpretation within the
following slightly more complicated system of recursive
types:
where Loc is some countable set of locations (considered as
a predomain). Some notation will come in handy in later
sections. We write St Val for Rec Loc (Rec F (Val)). There is
an obvious projection -Val : St!StVal with -Val (oe):' '
projects on the first component.
2 Note that we will distinguish, however, in the object logic.
different
from all m i

Table

1. Definition of record update (extension)
Notice that the definition of St as Rec Loc (Ob) faithfully
reflects the idea of a state as an assignment of objects to
a finite set of locations. We think that this modelling of
states as records should also be employed when modelling
e.g. simple imperative languages where only basic values
can be stored to locations. Besides conceptual adequacy a
technical advantage of such a modelling is that Rec Loc (N)
is a countable flat predomain whereas the traditional choice
Loc!N? is uncountable and highly non-flat.
Definition 2.2 Given an environment ae 2
and an object expression a its interpretation
St*Loc\ThetaSt is defined in Table 2.2 (page 4). Note that
for an O we write o:f and o:m instead of - 1 (o):f and
resp. to reduce syntactic clutter.
If one does not distinguish between methods and fields
and ignores basic values, as Abadi & Cardelli do in [1], the
above system of mutual recursive type definitions simplifies
as follows
The fact that fields and methods are not distinguished implies
that method overriding is allowed.
Notice that equivalently Ob can be defined by the single
recursive equation
which, obviously, is obtained from O = RecM (O*O) by
simply replacing O by Loc\ThetaRec Loc (Ob) on the right hand
side.
2.3.1 Variation -
a la Abadi & Cardelli
Notice that the denotational semantics presented above is
not quite in accordance with the operational semantics for
the imperative object calculus given in the book [1] of Abadi
and Cardelli (pp. 136-137) which implies the following domain
equations
where method closures are saved in the store and meanings
of object expressions a in an environment ae 2
Val Var are functions of type St*Val\ThetaSt and not of type
St*Loc\ThetaSt. We leave it as an exercise for the inclined
reader to give the semantic equations for the object calculus
according to the domain equations above such that the
interpretation is adequate w.r.t. operational semantics in [1].
3 Object specifications
Having identified the meaning of the (functional and imperative
resp.) object calculus (within the recursively defined
predomain O and Loc \Theta St) we are in the position to
use any logic of predomains for reasoning about objects. In
the end one might find it useful to identify a special purpose
calculus for reasoning about objects which finds its meaning
by translation into some logic of predomains. 3 However,
before embarking on such a project we rather discuss what
is the shape of predicates expressing interesting properties
of objects.
3.1 A first notion of specification
We consider the functional case first in order to understand
what a specification of an object should be. A possible
definition could be the following.
Definition 3.1 Let A 2 P(O)!P(O) monotonic, ~
O\ThetaO) m2M . Then these data induce a monotonic operator
which is defined as
P(O). The Bm stand for result specifications and
the Tm represent transition specifications for each method
m. Finally, A specifies the remaining properties of the ob-
ject, i.e. the fields. We write Inv(A; ~
T ) for the greatest
fixpoint of \Phi A; ~
T .
3 as e.g. Hoare logic which provides sort of a useful "macro-language"
for reasoning about partial functions on states
where ' is a fresh location not in the domain of oe
where ' 0 is a fresh location not in the domain of oe 0
[[let x=a in b]]ae

Table

2. Denotational semantics for the imperative object calculus
If I is a post-fixpoint of \Phi A; ~
then every o2I satisfies the predicate A and whenever
o:m(o) is defined then it satisfies Bm (I) and is
related to o via Tm . In particular, this holds for
the greatest fixpoint Inv(A; ~
T ) of \Phi A; ~
T as given
by
the union of all post-
fixpoints of \Phi A; ~
T . Thus, in order to prove that
one 'simply' has to exhibit a predicate P with
Such a notion of "invariant" specification seems to be
quite in accordance with the "coalgebraic view" of the
object-oriented world and, therefore, is probably quite use-
ful. However, it seems to have its limitations as exemplified
by the following example.
Example 3.1 Consider the object expression a j
[m=&(x)x:m()]. Operational intuition tells us that a:m()
diverges and, therefore, it would be most desirable to prove
this employing an appropriate notion of invariant. What
comes to ones mind immediately is the invariant I =
False and
S. Then for I we have
Coinduction does not help in proving that I for an
object a since one has to find a predicate P such that
But the only canonical choice for
P is I again so nothing is achieved.
In [2] Abadi and Leino introduced a sort of Hoare logic
for a variant of the imperative object calculus which allows
one to prove divergence of a:m() quite easily. For sake of
simplicity we first discuss the following adaption of their
account to the purely functional case.
3.2 Functional object specifications
A notion of specification for functional objects is sug-
gested. The existence of such specifications is discussed in
Section 4.
Definition 3.2 For every A 2 P(O) ! P(O), ~
P(O))m2M and for every ~
T ) be the predicate S'O
with
provided S is unique with this property. We call
T ) the specification induced by A, ~
B and ~
T .
This is different from Inv(A; ~
T ) since one requires
for methods m2M the condition 8o 0 2S: o:m(o 0 )# )
to hold and not just
S is implicitly ("recursively") specified even if the ~
B and A
do not depend on S.
Example 3.2 To illustrate the power of this new notion we
will employ the specification
satisfying
(i.e. 8o 0 2S: o:m(o 0 )") for showing that [[a:m()]]". Of
course, from o2S it follows that o:m(o)". Thus, it remains
to show that which, however, is easily seen to be
the case as for
diverges by the previous consideration.
3.3 Imperative object specifications
For the imperative setting the corresponding notion of
specification is obtained analogously to the functional case
yet accounting for the underlying store (the different "im-
plementation" of O). Again, existence of such specifications
is discussed in Section 4.
Definition 3.3 For any predicates or families of predicates,
resp.,
~
P(Val \Theta St)) m2M
~
St \Theta Val \Theta St)) m2M
let
T ) be the predicate S ' Loc \Theta St with
provided S is unique with the above property.
If ~
T ) be the predicate S ' Loc \Theta St with
provided S is unique with this property.
In Section 4 it will become clear why it is useful to restrict
attention to transition specifications that just refer to
the "flat" part of the store and not to the "higher-order part"
of the store, i.e. the method closures.
Example 3.3 Assume that object specification S is supposed
to express the following invariant. Field f is always a
positive natural number. Define S accordingly:
However, despite their indisputable usefulness the problem
with specifications is that there is no obvious reason
why they should exist as the right hand side of the equivalence
characterising
contains both positive
and negative occurrences of Spec(A; ~
Though in [2]
specifications are used intrinsically their existence is not
verified. Instead the validity of assertions for programs is
defined w.r.t. derivability of correctness assertions which
renders the value of the Soundness Theorem of [2] as somewhat
mysterious (if not dubious).
4 Existence of object specifications
In this section we will identify some mild assumptions
which guarantee the existence and uniqueness of specifications
introduced in the previous section.
4.1 Functional object specifications
In contrast to functional 4 or imperative kernel languages
the object calculus implicitly presupposes recursive types
like O. Thus, it appears necessary to employ induction principles
for the recursive type involved in order to verify pro-
grams. After recalling in fairly concrete terms the induction
principle for O we will use it for establishing the existence
of specifications under fairly mild conditions.
From well-known work of Freyd and Pitts in the early
nineties we know that the bifree solutions of the domain
equation can be characterised by the requirement
that id A is the least fixpoint of
In case of F (X; Y
which is defined explicitly as the endo-function on [O*O]
as given by
or, equivalently, in a more readable form by
for e: O*O, a2O and m2M.
From
F
immediately
that P (id) holds for an admissible predicate P'[O*O] if
8evid: P (e))P (ffi(e)). This Fixpoint Induction principle
can be used directly for verifying properties of objects.
Example 4.1 Let a = [m=&(x)x:m()], then using Fixpoint
Induction one can prove that [[a:m()]]".
consider the admissible predicate
on [O*O]. Obviously, [[a:m()]]" is equivalent to P (id).
Thus, by Fixpoint Induction it suffices to show that
Suppose that evid with P (e),
i.e. e(o):m(e(o))=?. Then P (ffi(e)) as
where the last equality is the induction hypothesis P (e).
The Fixpoint Induction principle will be employed once
more below for proving unique existence of specifications
under rather mild assumptions.
4 For example PCF is based on the finite type hierarchy over the base
type N? and simple imperative languages for which Hoare calculus was
first introduced are based on Rec Loc (Val)*Rec Loc (Val).
Definition 4.1 For a flat predomain I let L I (A) be
the complete lattice of Scott-closed (ie. admissible and
downward-closed) subsets of I \ThetaA ordered by '.
Let I be a flat predomain. For any X;Y 2 L I (A), and
as in [10].
For (A) the set
is obviously a nonempty Scott-closed subset of the domain
[A*A].
The following theorem uses the same line of arguments
as loc.cit.
Theorem 4.2 Given a locally continuous bifunctor on pre-
domains F and a predomain A such that F (A;
A, a predomain I , and a monotonic \Phi : L I (A) op \Theta
I (A)!L I (A), such that
for all X;Y;
for a unique S 2 L I (A).
Proof. Let I (A)!L I (A) be monotonic
and satisfy the condition (y). Then the mapping
I (A)!L I (A) op \Theta L I (A)
is a monotonic endomap on the complete lattice L I (A) op \Theta
I (A). Thus, by Knaster-Tarski b
\Phi has a fixpoint
For establishing we show by fixpoint induction
that for the admissible predicate
we have P (-e:F (e; e)) and, therefore, P (id A ) as id
-e:F (e; e) from which it follows that
viously, we have P (?). For the induction step assume
that P (e). Then F
by (y) that F
gously, it follows from e by (y) that F
. Thus, we have
Thus, we conclude that there exists at least one S 2
showing uniqueness suppose
I (A). For the admissible
predicate
it follows P (-e:F (e; e)) again by fixpoint induction. Obvi-
ously, we have P (?). Assume that P (e). Then F
by (y) that
as the induction hypothesis P
(id) from which
it follows immediately that id
Theorem 4.3 (Existence Theorem)
Let L denote L 1 (O) and F (Y;
Moreover, let A 2 L!L, ~
~
O))m2M be families such that for all
id O and X;Y 2 L
and X;Y 2 L
Scott-closed for
all
Then there exists a unique S 2 L satisfying for all
Proof. For consider the predicate
which is Scott-closed due to the fact that Bm and Tm are
Scott-closed (see also condition (3)) and the fact that the
precondition of the implication is Scott-open. Clearly, the
\Theta L!L is monotonic.
Obviously, the requirement is equivalent to
O. Thus, we have to show that there exists
a unique S 2 L with which is guaranteed by
Theorem 4.2 provided we can show that our \Phi satisfies the
condition (y) of Theorem 4.2 which we verify next.
Suppose e v id O with
For showing F
show that F (e; e)(o) 2 \Phi(Y
First we show that F (e; e)(o)2A(X 0 ). But F (e; e)(o) v
and, therefore, also F (e; e)(o)2A(X 0 ) due to assumption
(1).
Next, let m2M and
therefore, as by induction
hypothesis
But then we have
by (2) and the assumption Moreover, we
obtain
by assumption (3) as e(o:m(e(o 0 ))) v o:m(e(o 0 )) and
since (3) implies that x 0 v x - y v y 0 implies
as F (e; e)(o):m(o 0
4.2 Imperative object specifications
Recall from Section 2 that the imperative object calculus
of [2] finds its denotational interpretation within the recursively
defined predomain St = F St (St; St) if the latter is
defined to be
Rec Loc (Rec F (Val)\ThetaRec M (Loc\ThetaSt*Val\ThetaSt))
Next we prove a variant of Theorem 4.3 for the imperative
object calculus.
Theorem 4.4 For any predicates and families of predi-
cates, resp.,
~
~
St \Theta Val \Theta St)) m2M
such that
(ii) for all m 2
(iii) for all the predicate Tm is Scott-closed in its
last argument and monotonic in its second argument.
Then for
there exists a unique S 2 L Loc (St) with
Proof. Instantiating Theorem 4.2 by F St for F , Loc for I ,
and St for A guarantees the existence of a unique fixpoint
for \Phi provided we can verify that \Phi satisfies the condition
(y) of Theorem 4.2. Note that \Phi(Y; X) is Scott-closed if
are, due to condition (iii) and the fact that
the precondition of the implication is Scott-open. Also, the

For subsequent use it is helpful to recall that
F St (e; e)(oe)# for all oe 2 St, and that
(a) F St (e;
(b) F St (e;
Now we show that \Phi satisfies condition (y). Suppose
e v id St with
for some X;X
We have to show that F St
For that purpose we suppose that
and show that h'; F St (e; e)(oe)i 2 \Phi(Y
From (3) we get A(X)('; oe). Thus by (i) we get that
i.e the first part of the conjunction
For the second part suppose that
From (b) and F St (e; e)(oe):':m(' 0 ; oe 0 )# we know that
for some value v2Val and some store oe 00 2St. We have
to show that F St (e; e)(o):':m('
From (6) it follows
that e(oe 0 )#. Thus, from (4) we get by (2) that
Thus, by (3) it follows that Bm (X)(oe:':m('
i.e. Bm (X)hv; oe 00 i by (6). By (ii) it follows now that
therefore, by (5) that
It follows by the second part of the conjunction h'; oei 2
\Phi(Y; X) as ensured by (3) that
as by (7) and oe:':m(' 0 ; e(oe 0 ))# by (6). From
(5) it follows that e(oe 00 )# and from (6) that e(oe 0 )#. There-
fore, by assumption (iii) it follows that
i.e.
This proves that under certain conditions the specification
really exist. But condition (iii) of
Theorem 4.4 is awkward to prove and can be simplified if
the method specifications only refer to the flat part of the
store.
Corollary 4.5 Given any predicates and families of predi-
cates, resp.,
~
~
such that
(ii) for all m 2
Then for
there exists a unique S 2 L Loc (St) with
Proof. Applying Corollary 4.4 it only remains to show
that condition (iii) of loc.cit. holds. This follows simply
from the fact that St Val is a flat predomain.
5 Soundness of the Abadi & Leino logic de-
notationally
Theorem 5.1 The object creation rule of the Abadi & Leino
logic is correct w.r.t. our semantics.
Proof. An object specification S in [2] reads as follows
where, again, the A i are field specifications, B j are the result
specifications for method m j and T j is the transitions
specification for m j . If we interpret all these predicates denotationally
it follows from Theorem 4.4 that they give rise
to a unique predicate that is as in Definition 3.3 and serves
as the denotational interpretation of S.
It is important that in the Abadi & Leino logic the transition
specifications T j can only refer to the flat part of the
store otherwise existence of S could not be guaranteed.
The object formation rule of loc.cit. says about the newly
created object
specifies the actual memory allocation and
the absence of side effects. Ignoring the side effect
issue T - of the creation the correctness of the rule above
in our semantics follows simply from the Definition 3.3 of
specification (Spec).
It should be relatively straightforward how to devise
a denotational semantics for the whole logic of Abadi &
Leino and to prove correctness of their calculus w.r.t. such a
denotational semantics. Such a proof should be easier than
the one presented in [2].
6 Possible extensions of the Abadi & Leino
logic
Dealing with object specifications denotationally does
not only yield a concise explanation of the Abadi & Leino
logic but also suggests extensions.
6.1 Invariants
By contrast to Abadi & Leino the predicates A and Bm
may contain recursive occurrences of the specification it-
self. If a field is required to fulfill the same specification
as the ambient object then one needs recursion in A. If a
result of method m is required to contain (or be itself) an
object fulfilling the same specification as the ambient ob-
ject, one needs recursion in Bm . In [8] Leino gives a variant
of the logic [2] that allows for recursive object descriptions
but requires that methods are declared in advance.
The presented approach even allows for more. In a definition
of a specification S('; may allow the
Bm to refer to the self reference ' to express that the whole
specification S is an invariant. By setting
it is required that a method invocation of m does preserve
the specification S of the self object. This means that the
specifications Spec can not only describe denotationally
properties of objects at a certain point in a program (like
in Abadi& Leino) but a kind of invariant that can be seen as
a definition of a "class specification" in the object calculus.
6.2 Method update
In its generality the presented approach allows one to
deal with method update in a limited way. Consider the
following example:
Example 6.1 A sensible requirement in presence of method
update is that a method is not altered by another method,
i.e. a method n can at most become less or equally defined
by execution of m (less since we are dealing with partial
correctness). More formally, this translates to the following
transition predicate:
This definition satisfies condition (iii) of Theorem 4.4 since
if e v id and e(oe):':n w oe 0 :':n then by transitivity from
oe:':n w e(oe):':n w oe 0 :':n w e(oe 0 ):':n it follows that
To which forms of transition specifications our existence
theorem applies remains to be clarified. That specifications
of general form need not exist is demonstrated by a counterexample
in the next section.
7 Non existing specifications
Before showing that particular object specifications do
not exist we prove the following auxiliary lemma that deals
with transition specifications that may also refer to the non
flat part of the store, i.e. to some method closures.
Lemma 7.1 Let A ' Loc\ThetaSt\Theta[Loc\ThetaSt*Val\ThetaSt] and
If ' is a location and oe a state satisfying
then
Proof. From (0) it follows that
and, therefore, by (1) that
i.e. that ('; oe) 2 S. Thus, by (y) we have A('; oe; oe:':m).
To give an example of a non-existing object specifica-
tion, we will exhibit a transition specification Tm , a location
and a store oe such that there does not exist S ' Loc\ThetaSt
satisfying
For such a specification the restrictive assumption of Theorem
4.5 - that Tm must only refer to the flat part of the store,
i.e. no specifications of past or future behaviour of methods
can be made - must necessarily be violated, but also condition
(iii) from Theorem 4.4 cannot hold.
Example 7.2 Consider the following object specification
where
Note that T is not admissible. Let A('; oe; h) denote the
property
then the specification S above can be reformulated as
i.e. condition (0) of Lemma 7.1 holds for A. Now for ('; oe)
with
one easily verifies that (1) holds but (2) is false, contradicting
Lemma 7.1(2).
More natural counterexamples are expected by semantic
modelling of logics for object calculi using Hoare triples
like the tentative one suggested in [4].
Conclusions
We have shown that a denotational approach to programming
logics for object calculi leads to a better understanding
of the implicit recursion of object specifications and their
reasoning principles. Since the notion of specification encodes
the object introduction rule of the logic, the soundness
of this rule is equivalent to the existence of the speci-
fication. To guarantee existence one has to be careful with
reasoning on the non-flat method part of the store.
It should be possible to deal with other, similar, object
calculi and logics in the same denotational way. The analysis
of further languages should be fruitful in the quest for
more (natural) counterexamples. A comparison with class-based
languages has been attempted in [15].
Recursive methods can be programmed in the object calculus
without explicit recursion due to the recursive higher-order
definition of the underlying store. This is a particular
instance of "recursion through the store" a more general
variant of which allows unrestricted execution of code
stored in memory. Such a rather liberal usage of higher-order
store needs to be modelled by different domain equations
and thus needs different treatment altogether. Results
analogous to those in this paper are expected to be hard to
establish.
In this paper we used classical logic as a meta logic
but did not commit ourselves to any particular object logic.
Spatial or separation logic [9, 5] is a prospective candidate
for such an object logic as it simplifies handling of aliases.
It remains to be seen whether predicates in such a logic pose
any problems to the presented approach.
Other issues to be tackled include a soundness proof for
the Abadi & Leino logic possibly extended by invariants
and reasoning principles on higher-order store and the development
of a logic over a typed semantics of the object
calculus (with subtyping including method parameters).

Acknowledgment

Thanks to Cristiano Calcagno and Peter
O'Hearn for discussions on ``recursion through the store''
and other related matters.



--R

A Theory of Objects.
A logic of object-oriented pro- grams
A proof theory for a sequential version of POOL.
A logic for objects.
On garbage and program logic.

Modular specification and verification of object-oriented programs
Recursive object types in a logic of object-oriented programs
Local reasoning about programs that alter data structures.
Relational properties of domains.
Logical foundations for typed object-oriented languages
Objects and classes in Algol-like lan- guages
A logic of recursive objects.
A logic of recursive objects (abstract).
Class based vs. object based: A denotational com- parison
A Hoare-Calculus for Verifying Java Realizations of OCL-Constrained Design Models
--TR
Inheritance in smalltalk-80: a denotational definition
Two semantic models of object-oriented languages
Reasoning about Java classes
Objects and classes in Algol-like languages
Component Software
A Theory of Objects
Modular Specification and Verification of Object-Oriented Programs
Recursive object types in a logic of object-oriented programs
A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models
Semantics and Logic of Object Calculi
Class-Based versus Object-Based
A Logic of Object-Oriented Programs
A WP-calculus for OO
On Garbage and Program Logic
A Logic of Recursive Objects
Logical foundations for typed object-oriented languages
Local Reasoning about Programs that Alter Data Structures
An Introduction to Specification Logic
A Denotational Semantics of Inheritance

--CTR
Bernhard Reus , Jan Schwinghammer, Denotational semantics for a program logic of objects, Mathematical Structures in Computer Science, v.16 n.2, p.313-358, April 2006
domain theory;program verification;programming logic;object logic;denotational semantics