arXiv:cs/0212003v1 [] 4 Dec 2002

Ownership Confinement Ensures Representation
Independence for Object-Oriented Programs
ANINDYA BANERJEE
Department of Computing and Information Sciences
Kansas State University
Manhattan KS 66506 USA
and
DAVID A. NAUMANN
Department of Computer Science
Stevens Institute of Technology
Hoboken NJ 07030 USA
Dedicated to the memory of Edsger W. Dijkstra.
Representation independence or relational parametricity formally characterizes the encapsulation
provided by language constructs for data abstraction and justifies reasoning by simulation. Representation independence has been shown for a variety of languages and constructs but not for shared
references to mutable state; indeed it fails in general for such languages. This paper formulates
representation independence for classes, in an imperative, object-oriented language with pointers,
subclassing and dynamic dispatch, class oriented visibility control, recursive types and methods,
and a simple form of module. An instance of a class is considered to implement an abstraction
using private fields and so-called representation objects. Encapsulation of representation objects is
expressed by a restriction, called confinement, on aliasing. Representation independence is proved
for programs satisfying the confinement condition. A static analysis is given for confinement that
accepts common designs such as the observer and factory patterns. The formalization takes into
account not only the usual interface between a client and a class that provides an abstraction but
also the interface (often called “protected”) between the class and its subclasses.
Categories and Subject Descriptors: D.3.3 [Software]: Programming Languages—Language Constructs and Features; F.3.1 [Theory of Computation]: Logics and Meanings of Programs—
Specifying and Verifying and Reasoning about Programs
General Terms: Languages, Verification
Additional Key Words and Phrases: Alias control, confinement, relational parametricity, simulation
This is an expanded and revised version of a paper originally appearing in ACM Symposium on
Principles of Programming Languages, 2002.
Banerjee was supported by NSF grants EIA-9806835, CCR-0209205 and NSF Career award CCR0093080/CCR-0296182.
Naumann was supported by NSF grants INT-9813854 and CCR-0208984 and a grant from the
New Jersey Commission on Science and Technology.
Banerjee and Naumann were also supported by EPSRC grant GR/S03539, “Abstraction, Confinement and Heap Storage”.
Permission to make digital/hard copy of all or part of this material without fee for personal
or classroom use provided that the copies are not made or distributed for profit or commercial
advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and
notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish,
to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.
c 20YY ACM 0000-0000/20YY/0000-0001 $5.00
ACM Journal Name, Vol. V, No. N, Month 20YY, Pages 1–88.

2

·

A. Banerjee and D. Naumann

Contents
1 Introduction

3

2 Representation independence
6
2.1 A first example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2.2 Representation exposure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.3 Overview of results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
3 Ownership confinement
3.1 Callbacks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.2 The observer pattern . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.3 Confinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

13
14
15
17

4 Syntax

19

5 Semantics
24
5.1 Semantic domains . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
5.2 Semantics of expressions, commands, constructors and methods . . . . . . . 28
6 Confinement ramified
33
6.1 Confinement of states . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6.2 Confinement of commands and methods . . . . . . . . . . . . . . . . . . . . 35
6.3 Properties of confinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
7 First abstraction theorem
7.1 Comparing class tables . . . . . . . .
7.2 Coupling relations and simulation . .
7.3 Restricting reps in owner subclasses
7.4 Identity extension . . . . . . . . . .
7.5 Abstraction theorem . . . . . . . . .

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

41
41
42
46
47
48

8 Applications and further examples
52
8.1 Program equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
8.2 Further variations on observer . . . . . . . . . . . . . . . . . . . . . . . . . . 56
9 Owner subclassing: the protected interface
9.1 Owner subclassing and module scope . . . . . . . . . . . . . . . . . . . . . .
9.2 On behavioral subclassing . . . . . . . . . . . . . . . . . . . . . . . . . . . .
9.3 Formalization of module-scoped methods . . . . . . . . . . . . . . . . . . . .

57
58
61
61

10 Second abstraction theorem

63

11 Static analysis

68

12 Discussion and related work
74
12.1 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
12.2 Future challenges . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
A Additional proofs
ACM Journal Name, Vol. V, No. N, Month 20YY.

79

March 26, 2018

·

3

1. INTRODUCTION
You have implemented a class [Dahl and Nygaard 1966; Arnold and Gosling 1998],
FIFO, whose instances are FIFO queues with public methods enqueue and dequeue
as well as method size that reports the number of elements in the queue. The class,
implemented in some Java-like object-oriented language, is part of a library and
is used by many programs, most unknown to you. The queue is represented using
a singly linked chain of nodes that point to elements of the queue. There is also
a sentinel node [Cormen et al. 1990]. Each instance of FIFO has a field num with
the number of nodes and a field snt that references the sentinel. You realize that a
simpler, more efficient implementation can be provided without the sentinel, using
two fields, head and tail, pointing to the end nodes in the chain. You revise method
size to return num instead of num−1 and revise the other methods suitably. You are
guided to the necessary revisions by thinking about the correspondence, sometimes
called a simulation relation, between the representations for the two versions.
Can the revisions affect the behavior of clients, that is, programs that use class
FIFO in some way or other? The answer would be yes, if some client determined
the number of nodes by reading field num directly. A client that refers to field
name snt would no longer compile. But you have taken care to encapsulate the
queue’s representation: the fields are declared to be private. By using programming
language constructs like private fields you aim to ensure that client programs depend
only on the abstraction provided by the class, not on its representation. If client
behavior is independent from the representation of FIFO, it is enough for you to
ensure equivalent visible behavior of the revised methods.
For scalable systems, scalable system-building tools, and scalable development
methods, abstraction is essential. For reasoning about a single component, e.g.,
a class, module, or local block, abstraction makes it possible to consider other
components in terms of their behavioral interface rather than their internal representation.1 Abstraction is needed for the automated reasoning embodied in static
analysis tools [Cousot and Cousot 1977] and it is needed for formal and informal
reasoning about functional correctness during development and evolution [Milner
1971; Hoare 1972]. Modular reasoning has always been a central issue in software
engineering and in static analysis. With the ascendancy of mobile code it has become absolutely essential. For example, it is possible for clients of FIFO to be linked
to it only at runtime, so it is impossible to check all uses to determine whether the
revisions affect them.
The need for flexible but robust encapsulation mechanisms to support data abstraction has been one of the driving forces in the evolution of programming language design, from type safety and scoped local variables to module and abstract
data type constructs [Liskov and Guttag 1986]. There is a rich theoretical literature on the subject (e.g., [Plotkin 1973; Reynolds 1974; Donahue 1979; Haynes
1984; Reynolds 1984; He et al. 1986; Mitchell 1996; Lynch and Vaandrager 1995;
de Roever and Engelhardt 1998]). Many different language constructs have been
studied. There is considerable variation in the details of these theories, partly
because the intended applications vary from justifying general tools for program
1 Even

a primitive type like int is an abstraction from the machine representation.
ACM Journal Name, Vol. V, No. N, Month 20YY.

4

·

A. Banerjee and D. Naumann

Fig. 1. A FIFO object with its encapFIFO
PSfrag
replacements
sulated representation: private
fields
and
nodes of a list (within the dashed rectangle). One element of the queue is shown
as well as a user of the queue, but other
objects and references are omitted. The
dotted reference is an example of representation exposure.

num 4
tail
head

User

Element

analysis and transformation to justifying proof rules to be applied to specific programs as in the FIFO example. The common thread is that two implementations of
a component are linked by a simulation relation between the two representations.
Unfortunately, these theories are inadequate for object-oriented programs. They
deal well with the encapsulation of data structures that correspond directly to some
language construct, such as modules, local variables, or private fields. But the FIFO
example also involves encapsulation of a data structure composed of heap cells and
pointers, including aliasing with the tail field as depicted in Fig. 1.
The problem is that encapsulation provided by language constructs often runs
afoul of aliasing. For variables and parameters, aliasing can be prevented through
syntactic restrictions that are tolerable in practice (and often assumed in formal
logics and theories). Aliasing via pointers is an unavoidable problem in object
oriented programming where shared mutable objects are pervasive. Yet unintended
aliasing can be catastrophic. A version of the Java access control system was
rendered insecure because a leaked reference to an internal data structure made it
possible to forge crytographic authentication [Vitek and Bokowski 2001]. In simply
typed languages, types offer limited help: variables x, y are not aliased if they have
different types. Even this help is undercut by subclass polymorphism: in Java, a
variable x of type Object can alias y of any type.
The ubiquity and practical significance of the issue is articulated well in the manifesto of Hogg et al. [1992]. A number of subsequent papers in the object-oriented
programming literature propose disciplines to control aliasing. Of particular relevance are disciplines that impose some form of ownership confinement that restricts
access to designated “representation objects” except via their “owners”, to prevent
representation exposure [Leino and Nelson 2002]. A good survey on confinement,
especially ownership, can be found in the dissertation of Clarke [2001]; see also Lea
[2000],Vitek and Bokowski [2001], Clarke et al. [2001], Müller and Poetzsch-Heffter
[2000], Boyland [2001], Aldrich et al. [2002], and the related work section of this
paper.
In Figure 1, an instance of class FIFO (the owner) uses private fields to point
to objects intended to be part of its encapsulated representation, as indicated by
the dashed rectangle. The contribution of this paper is a theory of representation
independence for encapsulation of data in the heap, using ownership confinement.
We follow Reynolds [1984] in calling our main result an abstraction theorem. Some
readers may prefer the term relational parametricity.
The literature on confinement is largely concerned with static or dynamic checks
to ensure invariance of various confinement properties. One of our contributions is
to show how established semantic techniques can be used to evaluate confinement
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

5

disciplines. To prove our abstraction theorem, we use a semantic formulation of
confinement. Separately, we give a modular, syntax-directed static analysis for confinement and show that it accepts some interesting example programs that embody
important object-oriented design patterns.
There are a number of ways in which abstractions can be expressed using constructs of contemporary object-oriented languages, including modules, classes, local
variables, object instances, not to mention heap structures such as object groups.
We treat the most common situation: an instance of some class is viewed as representing an abstraction, possibly using some other objects as part of its representation.
We are aware of no previous results on representation independence that address
encapsulation of objects in the heap. Thus it is tempting to present the ideas
in the setting of a simple idealized language, say a simple imperative language
with pointers to mutable heap cells. But this would leave open some challenging
issues, such as how class-based scoping rules fit with instance-based abstraction.
We have chosen to consider a rich imperative object-oriented language with classbased visibility, inheritance and dynamic binding, type casts and tests, recursive
types, and other features sufficient for programs that fit common design patterns
such as observer and factory [Gamma et al. 1995].
Previous work on representation independence has been concerned with relating
two versions of a component with respect to programs that use the component.
But the designer of a class needs to consider not only users (the client interface)
but also subclasses (the protected interface). This is a source of complication in our
treatment of confinement and, to a lesser extent, in our treatment of representation
independence. Our results consider replacement of one version of a class by another
with the same public interface, in the context of arbitrary classes that use it or are
subclasses of it.
Overview and readmap. Sect. 2 introduces the language for which our results are
proved and describes a simple example with which we review the formalization of
representation independence using simulation relations. The example is extended
to one showing how representation independence can be invalidated by leaked references to representation objects. The section concludes with an informal statement
of our abstraction theorem.
Sect. 3 discusses more elaborate examples that typify object-oriented programs.
A version of a Meyer-Sieber [Meyer and Sieber 1988] example shows how higher
order programs can be expressed. Versions of the observer pattern [Gamma et al.
1995] illustrate challenges in formulating robust but practical notions of confinement. The section concludes with an informal description of our notion of ownership
confinement.
Sect. 4 formalizes the syntax and typing rules. Sect. 5 gives a surprisingly simple
denotational semantics in the manner of Strachey [2000]. Confinement, the semantic notion, is defined formally in Sect. 6. Sect. 7 gives the first main result, an
abstraction theorem for confined programs. Sect. 8 shows in detail how the theorem applies to the examples in Sect. 3 and to further variations on the observer
pattern. Sect. 9 considers examples of the interface between an owner class and its
subclasses. To achieve a sufficiently flexible form of confinement for subclasses of
ACM Journal Name, Vol. V, No. N, Month 20YY.

6

·

A. Banerjee and D. Naumann

the owner class, we add a simple module construct to the language. Sect. 10 proves
a second abstraction theorem, for this extended language and for a generalized notion of simulation needed for owner subclasses. Sect. 11 wraps up the technical
development by defining a static analysis for confinement that accepts the examples of Sections 2, 3, 8, and 9; soundness with respect to (semantic) confinement is
shown. Sect. 12 discusses related work and open challenges.
Detailed proofs are given, as the complexity of similar languages has led to errors
in published proofs, e.g., of type soundness. Appendices [to be put on line but not
in print] give some additional proofs and executable Java code for all the examples.
The organization of the paper is intended to make it possible for the casual
reader to skip some technical material and still get the gist of the results. Readers
who wish to study the details may still prefer to skip, on a first reading, material
concerning object constructors and proofs that involve fixpoints and inheritance.
Differences from the preliminary version. Outgoing references, from representation objects to client objects, were disallowed in the preliminary version of this
paper [Banerjee and Naumann 2002a]. We conjectured that they could be allowed
if restricted to read-only access as in [Müller and Poetzsch-Heffter 2000; Leino and
Nelson 2002]. Here we allow them without restriction, as is needed to handle examples such as the observer pattern where observers may well change state in response
to events. We have also added constructors to the language, at the cost of some
complexity in proofs due to the interdependence of semantics for commands and
for constructors. The benefit is succinct formulation of an abstraction theorem
sufficient for transparent application to realistic examples. The other major additions are as follows: module-scoped methods, the generalized abstraction theorem,
substantial worked examples, and the static analysis for confinement.
In [Banerjee and Naumann 2002a] we discuss simulation proofs of the equivalence
of “security passing style” [Wallach et al. 2000] with the lazy “stack inspection”
implementation of Java’s privilege-based access control mechanism [Gong 1999],
and then extend our language to include access control. We give an abstraction
theorem for this extended language. It was this study that led us to the main
results but in retrospect it seems tangential and is omitted.
2. REPRESENTATION INDEPENDENCE
We begin this expository section with a very simple example of representation independence, contrived mainly to introduce the Java-like language that we will use.
Building on this example we show how pointer aliasing can invalidate representationindependence. We conclude with an informal statement of the main results. Sect. 3
deals with more challenging examples including the observer pattern [Gamma et al.
1995] and gives a more precise description of ownership confinement.
2.1 A first example
The concrete syntax for classes is based on that of Java [Arnold and Gosling 1998]
but using more conventional notation for simple imperative constructs. Keywords
are typeset in bold font and comments are preceded by double slash. A program
consists of a collection of class declarations like the following one.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

class Bool extends Object {
bool f;
con{ skip }
unit set(bool x){ self.f := x }
bool get(){ result := self.f }
}

//
//
//
//

·

7

private field
public constructor
public method
public method

There are two associated methods: set takes a boolean parameter and returns nothing; get takes no parameter and returns a boolean value. Methods are considered
to be public, that is, visible to methods in all classes. (Module-scoped methods are
added in Sect. 10.) Every method has a return type; the primitive type unit, with
only a single value (it), corresponds to Java’s “void” and is used for methods like
set that are called only for their effect on state.
Instances of class Bool have a field f of (primitive) type bool. A field f is accessed
in an expression of the form e.f, and in particular self.f is used for fields of the
current object; a bare identifier like x is either a parameter or a local variable.
The distinguished variable result provides the return value; it is initialized with the
default for its type (false for bool and nil for class types). Fields are considered
to be private, that is, visible only to the methods declared in the class. Visibility
is class-based, as in many mainstream object-oriented languages: an object can
directly access the private fields of another object of the same class.
When a new object is constructed, each field is initialized with the default value
for its type. Then the constructor commands are executed: the constructors declared in superclasses are executed before the declared one which is designated
by keyword con. We refrain from considering constructors with parameters. In
subsequent examples we omit the constructor if it is skip.
The observable behavior of a Bool object can be achieved using an alternate
implementation in which the complement is stored in a field:
class Bool extends Object {
bool f;
con{ self.f := true }
unit set(bool x){ self.f := ¬x }
bool get(){ result := ¬(self.f) } }
We do not formalize class types (“interfaces” in Java) separately from class declarations. Class names are used as types and we use the term class loosely to mean the
name of a declared class. But we are concerned with relating comparable versions
of a class: as in the example above, a comparable version has the same name and
methods with the same names and signatures.
We claim that no client program using Bool can distinguish one implementation
from the other; thus we are free to replace one by the other. Of course this is not
the case if we consider aspects of client behavior such as real time or the size of
object code —but these are not at the level of abstraction of source code. Moreover,
input and output for end users is of some limited type like int or String. If a Bool
could be output directly, say displayed in binary on the screen, then an end user
could distinguish between the implementations. So we consider only clients that
use Bool objects in temporary data structures and not as input or output data.
ACM Journal Name, Vol. V, No. N, Month 20YY.

8

·

A. Banerjee and D. Naumann

An example of such a client is method main in the following class. It declares
a local variable b of type Bool, with scope beginning at the keyword in. In the
absence of explicit braces, the scope of a local variable extends to the end of the
method body.
class Main extends Object {
String inout;
unit main(){ Bool b := new Bool in
if . . . self.inout. . . then b.set(true) else b.set(false) fi;
self.inout := convertToString(b.get()) } }
We may consider method main as a main program for which the observable state
consists of field inout. Its final value depends on some condition “. . . self.inout. . . ”
on its initial value. No object of type Bool is reachable in the state of a Main object
after invocation of main, so there is no observable difference between its behavior
using one implementation of Bool and its behavior using the other.
The claim is that we need not consider specific clients; there is no use of Bool
that can distinguish between the two implementations. The standard reasoning
goes as follows.
(1) Suppose o is an object of type Bool for the first implementation and o′ an object
for the second. The correspondence between their states is described by the
basic coupling relation
o.f = ¬(o′ .f) .
(2) This relation has the simulation property:
—it holds initially (once the constructor has been executed), and
—if the two versions of set (respectively, get) are executed from related states
then the outcomes are related. (As we consider sequential programs, the
outcome is the updated heap and the return value if any.)
In short, the relation is established by the constructor and preserved by the
methods of Bool.
(3) To consider client programs we must consider program states consisting of
local variables (and parameters) along with the heap, which may contain many
instances of Bool as well as other objects. For states, we define the induced
coupling relation. Primitive values and locations are related by equality.2 A
pair of heaps are related if there is a one-to-one correspondence between Bool
objects such that they are pairwise related by the basic coupling of (1), and
everything else is related by equality.
The induced coupling relation is preserved by all commands in methods of all
classes. This is the abstraction theorem.
(4) For a pair of states related by the (induced) coupling, if no Bool objects are
reachable then the states are equal. This fact, known as the identity extension
lemma, holds by definition of the induced coupling.
It is a consequence of (3) and (4) that the two implementations cannot be distinguished by a client that does not input or output Bool objects. Any initial state
2 Later

we refine this point.

ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

9

for such a client is related to itself, by (4). We can consider an execution of the
client using either of the two implementations of Bool; the final states are related,
according to (3). And thus they are equal, by (4).
Identity extension confirms that the chosen notion of coupling relation is suited
to the chosen form of encapsulation. (Here, encapsulation means private fields and
objects not input or output.) It is typically a straightforward consequence of the
definitions.
For program refinement, identity can be replaced by inequality in step (4). In
this paper we do not emphasize refinement, but the requisite adaptation of our
results is straightforward. For applications in program analysis, other relations are
used in step (4), e.g., for secure information flow the relation expresses equivalence
from the point of low-security observers [Volpano et al. 1996].3
The abstraction theorem is a non-trivial property of the language. It would fail,
for example, if the language had constructs that allowed client programs to read
the private fields of Bool —or to enumerate the names of the private fields, or to
query the number of boolean fields that are currently true. Such operations would
be considered strange indeed.
Familiar operations on pointers, however, can also violate abstraction. For example, with pointer arithmetic one can distinguish between two representations that
differ only in the size of storage used (e.g., representing a boolean value using one
bit of an integer versus one bit of a character). Even in the absence of pointer
arithmetic, shared references lead to the following problem.
2.2 Representation exposure
Consider the following class OBool which provides functionality similar to that of
Bool, in fact using Bool. For clarity we have chosen different method names, to
emphasize that we are not comparing this class with Bool.
class OBool extends Object {
Bool g;
unit init(){ self.g := new Bool; self.g.set(true) }
unit setg(bool x){ self.g.set(x) }
bool getg(){ result := self.g.get() } }
To simplify the formal development, we sidestep the complicated interactions between subclassing and method calls in constructors by confining attention to constructors without parameters or method calls. In cases where this is inadequate,
an ordinary method can be used (like init in this example).
Here is an alternate implementation of OBool.
3 Our

formulation of the abstraction theorem can be applied directly to prove command and class
equivalences for a specific program. For applications of simulation in static analysis, the problem
is usually to show that a syntax directed system of types and effects approximates some property
like secure information flow, for all programs in a language. We have not attempted to formulate
an abstraction theorem general enough to apply directly in such analyses; they use analysis-specific
typing systems rather than the language’s own types and syntax. But the essence of our result
is that the language is relationally parametric, given suitable confinement conditions. Indeed,
in work subsequent to this paper, Banerjee and Naumann [2002b] use the same language and
semantic model for a relational analysis of secure information flow.
ACM Journal Name, Vol. V, No. N, Month 20YY.

10

·

A. Banerjee and D. Naumann

class OBool extends Object {
Bool g;
unit init(){ self.g := new Bool; self.g.set(false) }
unit setg(bool x){ self.g.set(¬ x) }
bool getg(){ result := ¬(self.g.get()) } }
To describe the connection between the two implementations a suitable basic coupling (recall (1) in Sect. 2.1) is the following relation between an object state o for
the first implementation of OBool and o′ for the alternate one:
(o.g = nil = o′ .g) ∨ (o.g 6= nil 6= o′ .g ∧ o.g.f = ¬(o′ .g.f)) .

(∗)

If o and o′ are newly constructed, the first disjunct holds; method init establishes
the second disjunct. Invocations of setg and getg maintain the relation: From
related initial states, either both abort (due to dereferencing nil because init has
not been called) or both terminate in related states.
For these implementations, it is not just a private field that is to be encapsulated,
but also the object referenced by that field. This is apparent in the coupling (∗)
which involves both. To describe the roles of the objects involved, we call class
OBool an owner class. Its instances “own” objects of class Bool, their representation
objects, which are called reps for short. Together, an owner and its reps constitute
what we call an island (cf. Fig. 1), following Hogg [1991].
Here is a suitable client for OBool.
class Main extends Object {
String inout;
unit main(){ OBool z := new OBool in z.init();
if . . . self.inout. . . then z.setg(true) else z.setg(false) fi;
self.inout := convertToString(z.getg()) } }
This does not distinguish between the two implementations of OBool nor does it
violate the intended encapsulation boundary.
Suppose we add to both versions of OBool the following method which “leaks” a
reference to the rep object.
Bool bad(){ result := self.g }
The method gives its caller an alias to the object pointed to by the private field
g. This makes the location of the encapsulated object visible to clients. In and of
itself, access to this location is not harmful.4 Like the other methods, method bad
preserves (∗). But a client class C can exploit the leak as in the following command.
OBool z := new OBool in z.init();
Bool w := z.bad() in if w.get() then skip else abort fi
4 To

make this clear, one could assume that, for both versions of OBool, the Bool object is allocated
at the same location. The assumption can be formalized by adding a conjunct o.g = o′ .g to
coupling (∗) and assuming that method init preserves this equality. It is then preserved by all
the methods of OBool including bad. Another justification is given in Sect. 10 where we show
formally how the language is “parametric in locations”.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

11

The command aborts if the new OBool is an object o′ for the second implementation
of OBool, but it does not abort for an object o for the first implementation. The
client command preserves the relation (∗), indeed it does not alter the state of the
objects it accesses. But the relation is not the identity for the rep object states: we
have o.g = o′ .g but o.g.f is not equal to o′ .g.f. So the relation is not the identity
for the client to which the reps are visible. An attempt to argue using the steps in
Sect. 2.1 breaks down because identity extension (4) fails.
The abstraction theorem, step (3), can also fail. Consider the following client
command.
OBool z := new OBool in z.init(); Bool w := z.bad() in w.set(true)
This does not preserve relation (∗). To see why, suppose o, o′ are a related pair
of OBool objects assigned to z and satisfying (∗). After the assignment to w, the
effect of w.set(true) is to make o.g.f = o′ .g.f, contrary to the relation (∗). This is
very different from the effect of z.setg(true).
The examples show that both ingredients of representation independence —
identity extension and preservation— can fail if a rep is leaked. The challenge is
to confine pointers in a way that disallows harmful leaks and thus admits a robust
representation independence property —without imposing impractical restrictions.
The challenge is made more difficult by various features of Java-like languages, for
example, type casts. We consider casts now; other challenges are deferred to Sect. 3.
Suppose we change the return type for method bad, attempting to hide the type
of the rep object.
Object bad(){ result := self.g }
Class Object is the root of the subclassing hierarchy so by subsumption it allows
references to objects of any class. The client can use a (Bool) cast to assert that
the result of z.bad() has type Bool. (In a state where the assertion is false, the cast
would cause abortion.)
OBool z := new OBool in z.init();
Bool w := (Bool)(z.bad()) in if w.get() then skip else abort fi
Again, the client is dependent on representation.
Note that the cast could not be used if the scope of class name Bool did not
include the client. This suggests a focus on modules (“packages” in Java) for
confinement of pointers, as has been studied by Vitek and Bokowski [2001] among
others (see Sect. 12). But in our example the field has private scope, each rep is
associated with a single owner, and the coupling relation is expressed in terms of
a single owner. Our results account for this sort of instance-based encapsulation,
which is common in practice and which is similar to the value-oriented notions used
for representation independence in functional languages [Reynolds 1984; Mitchell
1986; 1991].
2.3 Overview of results
In the examples above, class OBool is viewed as providing an abstraction. It is
just as sensible to consider Bool as providing an abstraction for which OBool is a
client. We do not annotate programs with a fixed designation of owners and reps.
ACM Journal Name, Vol. V, No. N, Month 20YY.

12

·

A. Banerjee and D. Naumann

Rather, we study how to reason about a class, say Own, one has chosen to view as
an abstraction with encapsulated representation. Objects of any subclass of Own
are also considered to be owners. A second class, say Rep, is designated as the
type of reps for Own. (In practice, Rep could be an interface or class type; this
generalization is straightforward but would complicate the formalization.)
A complete program is a closed collection of class declarations, called a class
table. We consider an idealized Java-like language similar to the sequential fragment of C++ (without pointer arithmetic), Modula-3, Oberon, C#, Eiffel, and
other class-based languages. It includes subclassing and dynamic dispatch, class
oriented visibility control, recursive types and methods, type casts and tests (Java’s
instanceof), and a simple form of module.
Roughly speaking, a class table CT is confined, for Own and Rep, if all of its
methods preserve confinement. A confined heap is one where the objects can be
partitioned into some owner islands (recall Fig. 1) along with a block of client
objects as in Fig. 5. Furthermore, there are no references from clients to reps. (We
use the term client for all objects except owners and reps.)
Sect. 3 discusses confinement in more detail and the formal definitions are the
subject of Section 6. The full significance of the definitions does not become clear
until Sect. 9 where we study subclasses of Own: an object of such a type inherits
the methods and private fields of Own, which manipulate reps. To be useful, owner
subclasses must have some access to reps. On the other hand, full access cannot
be granted; to do so would be to study not the class as unit of encapsulation but a
class together with its subclasses, which would be revised in concert.
Our objective is to compare versions of Own that may use different reps. We say
CT and CT ′ are comparable if they are identical except for having different versions
of class Own, and those two versions declare the same public methods. The two
versions of Own may well use different rep classes, say Rep and Rep′ . Without loss
of generality, our formalization has Rep and Rep′ both present in CT and CT ′ .
An interesting question is how to formalize basic couplings, step (1) of the proof
method outlined in Sect. 2.1. To allow useful data structures, we need to allow
representations to include pointers to client objects (e.g., elements of the queue in
Fig. 1). But if the programmer is required to define a relation involving the state of
objects outside the encapsulated data, how can this be done in a modular way? We
have chosen to use relations on the encapsulated state only. Put differently: those
things on which a coupling depends are considered as part of the island. Although
other alternatives merit study, this one makes for transparent application of the
formal results to interesting examples (this is done in Sects. 8 and 9). Moreover, it
is straightforward to define the induced coupling.
A basic coupling is a relation between a pair of owner islands for comparable CT
and CT ′ . A simple example is given by (∗) above in Sect. 2.2. More interesting is the
observer example, discussed in Sect. 3, which uses a linked list of client objects (the
observers). In Fig. 7 on page 44, a basic coupling is depicted in which the observer
objects occur as dangling pointers from the corresponding islands. The point is
that both versions are manipulating the same observer objects in the same way,
including the invocation of methods on those objects. So the state of the observer
objects is not relevant in the basic coupling —nor could it be, if the argument is to
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

13

be carried out in a modular way independent of the particular clients.
In a related pair of islands, both owners have the same class, which may well be
a proper subclass of Own.
The induced coupling relation for heaps relates h to h′ just if there are confining
partitions for which corresponding islands are pairwise related by the basic coupling.
Moreover, there is an exact correspondence between client objects in h and h′ .
Primitive values are related by equality. Locations are related by an arbitrary
bijection.
The induced relation is a simulation if it is preserved by the methods of class
Own in CT and in CT ′ . A method declared in one version of Own may be inherited
in the other version; it is the behavior of those methods that matters.
The abstraction theorem says that a simulation is preserved by all methods of all
classes, provided that both class tables are confined. The identity extension lemma
says that the induced relation is the identity, after garbage collection, for client
states in which no owners are reachable.
Sect. 7 gives the formal definitions for couplings and simulation in the special case
where locations of objects other than reps are related by equality. The abstraction
and identity extension results are proved there in detail. Sect. 10 generalizes the
definitions to allow an arbitrary bijection on locations; abstraction and identity
extension are proved for the general case. The special case is of interest because it is
adequate for some applications in program analysis (e.g., [Banerjee and Naumann
2002b]) and for non-trivial examples like those of Sect. 3 (as shown in Sect. 8).
Examples that require the general case are given in Sect. 9; they are subclasses
of Own that construct reps and pass them to methods of Own as in the factory
pattern [Gamma et al. 1995]. Notation is more complicated for the general case
but the proofs are not very different from the special case.
These results are proved in terms of a semantic formulation of confinement; indeed, the details of this formulation come directly from what is needed in the proofs.
Sect. 11 gives a syntax-directed static analysis: typing rules that characterize safe
programs and a proof that safety implies confinement (soundness). Our objective
is to round out the story by showing how confinement can be achieved in practice, not to give a definitive treatment of static analyses. But our analysis accepts
many natural examples and the constraints are clearly motivated in the proof of
soundness. The analysis is modular: It does not require code annotations and
the only constraint it imposes on client programs is that they cannot manufacture
representation objects.
3. OWNERSHIP CONFINEMENT
This section considers two substantial examples of representation-independence.
The first is an object-oriented version of an example given by Meyer and Sieber
[1988] as a challenge for semantics of Algol. It illustrates the expressiveness of
object-oriented constructs, specifically the use of callbacks which go against the
hierarchical calling structure which typifies the simplest forms of procedural and
data abstraction.
The second example is an instance of the observer pattern [Gamma et al. 1995]
which is widely used in object-oriented programs. In addition to callbacks it involves
ACM Journal Name, Vol. V, No. N, Month 20YY.

14

·

A. Banerjee and D. Naumann

a non-trivial data structure and outgoing references from representation objects to
clients. Note that we use the term client not just for objects that use an abstraction
(by instantiating it or calling its methods) but for any objects except instances of
the abstraction of interest or its encapsulated representation.
The section concludes with an overview of our semantic notion of confinement.
3.1 Callbacks
Meyer and Sieber [1988] consider the following pair of Algol commands:
var n := 0; P(n := n+2); if n mod 2 = 0 then abort else skip fi

(∗)

var n := 0; P(n := n+2); abort

(†)

Both invoke some procedure P, passing to it the command n := n+2 that acts on
local variable n. (That is, P is passed a parameterless procedure whose calls have
the effect n := n+2.) For any P, the commands are equivalent. The reason is that in
the first example n is invariably even: P is declared somewhere not in the scope of
n so the variable can only be affected by (possibly repeated) executions of n := n+2
and this maintains the invariant.
The difficulty in formalizing this argument is due to the difficulty of capturing
the semantics of lexically scoped local variables and procedures in a language where
local variables can be free in procedures that can be passed as arguments to other
procedures. (It appears even more difficult, and remains an open problem, to cope
with assignment of such procedures to variables [O’Hearn and Tennent 1997].)
Now we consider a Java-like adaptation of the example, due to Peter O’Hearn.
In place of local variable n it uses a private field g in a class A. Instead of passing
the command n := n+2 as argument, an A-object passes a reference to itself; this
gives access to a public method inc that adds 2 to the field.
class A extends Object {
int g; // (the default integer value is 0)
unit callP(C y){ y.P(self); if self.g mod 2 = 0 then abort else skip fi }
unit inc(){ self.g := self.g + 2 } }
In the context of this class and some declaration of class C with method P, the
Algol command (∗) corresponds to the command
C y := new C in A x := new A in x.callP(y)

(‡)

This aborts because after calling y.P, method callP aborts. The command (†) also
corresponds to (‡) but in the context of an alternative implementation of class A:
class A extends Object {
int g;
unit callP(C y){ y.P(self); abort }
unit inc(){ self.g := self.g + 2 } }
In Example 8.3, we use the abstraction theorem to prove equivalence of the two
versions using coupling relation
o.g = o′ .g ∧ o.g mod 2 = 0 .
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

15

This relation is preserved by arbitrary P because P can affect the private field g
only by calls to inc.
As Reynolds [1978] shows (see also [Reddy 1998]), instance-based object-oriented
constructs can be expressed in Algol-like languages, but the latter are in some ways
significantly more powerful. The Java version of the example can be seen as giving
an explicit closure to represent the command n := n+2 in the form of method inc.
Indeed the simplicity of the semantic model for our language can be explained by
saying the language is defunctionalized [Reynolds 1972; Banerjee et al. 2001] and
lacks true higher order constructs. If the example is written in such a language,
P ranges over more limited procedures than in Algol. The root problem for Algol
semantics [Reynolds 1981b; O’Hearn and Tennent 1995] and proof rules [Olderog
1983; German et al. 1989] is the interaction between arbitrary nesting of variable
and procedure declarations and possibility of passing procedures as arguments. In
imperative languages like C and Modula-3, procedures can be passed as arguments
and even stored in variables, but only if their free variables are in outermost scope.
This restriction greatly simplifies implementation of the language, and it suffices
to admit simple but adequate semantic models.5 The constructs of a Java-like
language offer similar expressive power and also admit simple models.
The example also illustrates what are known as callbacks in object-oriented programs. When an A-object invokes y.P(self) it passes a reference to itself, by which
y may invoke a method on the A-object which is in the middle of executing method
callP —a callback to A. If in (‡) we replace x.callP(y) by x.callP(self), and assume
that (‡) is a constituent of a method of class C, then we get a callback to C.
The point of the Algol example is modular reasoning about (∗) and (†) independent from the definition of P. For the object-oriented version we can also consider
reasoning independent from subclasses of A. If instead of (‡) we consider a method
unit m(C y, A x){ x.callP(y) }
then there is the possibility that m is passed an argument x of some subtype of A
that overrides inc. By dynamic binding, the overriding implementation would be
invoked by callP and our reasoning above would no longer be sound. For modular
reasoning, we could require that any overriding declaration of inc must preserve
the intended invariant that g is even. To impose such a requirement —and a
corresponding one for callP— is to require behavioral subclassing [Liskov and Wing
1994; Dhara and Leavens 1996]. One important application of simulations is in the
formalization of behavioral subclassing but that is beyond the scope of this paper.
Unlike much work on reasoning about object-oriented programs, our results
do not depend on behavioral subclassing. Representation independence holds for
clients and abstractions that do not exhibit behavioral subclassing (see Sect. 9.2).
3.2 The observer pattern
In this subsection we consider variations on an often-used design known as the
observer pattern [Gamma et al. 1995] which involves a non-trivial recursive data
5 Naumann

[2002] uses such a model to prove an abstraction theorem and apply it to MeyerSieber examples. The simpler of their examples can be proved directly in the model without use
of simulations [Naumann 2001].
ACM Journal Name, Vol. V, No. N, Month 20YY.

16

·

A. Banerjee and D. Naumann

class Observer extends Object { // “abstract class” to be overridden in clients
unit notify(){ abort } }
class Node extends Object { // rep for Observable
Observer ob;
Node nxt; // next node in list
unit setOb(Observer o){ self.ob := o }
unit setNext(Node n){ self.nxt := n }
Observer getOb(){ result := self.ob }
Node getNext(){ result := self.nxt } }
class Observable extends Object { // owner
Node fst; // first node in list
unit add(Observer ob){ Node n := new Node; n.setOb(ob); n.setNext(self.fst); self.fst := n }
unit notifyAll(){ Node n := self.fst; while n 6= null do n.getOb().notify(); n := n.getNext() od } }
Fig. 2.

First version of observer pattern, in procedural style.

structure using multiple rep objects and outgoing references to client objects. Further variations are given in Sect. 8.
We focus attention on the abstraction provided by an Observable object (sometimes called the “subject”). It maintains a list of so-called observers to be notified
when some event occurs. Its public method add allows the addition of an observer
object to the list. The public method notifyAll represents the event of interest; its
effect is to invoke method notify on each observer in the list. What notify does is
not relevant, so long as it is confined.6
The abstraction involves a collection of objects, a well-worn example for data
representations. Simple collections are essentially mutable sets of pointers to client
objects. Testing whether a reference is in the set requires only pointer equality. To
facilitate lookup by key, and to facilitate implementations like binary search trees,
it may be necessary for the abstraction to invoke a comparison method on the client
objects in the collection. This is similar to the call to notify in the observer pattern.
In the first version of the observer example, Fig. 2, most of the work is done
by the owner class Observable, which uses rep class Node to store observers in a
singly linked list. A more object-oriented version appears in Fig. 8 of Sect. 8; it
exemplifies the use of class-based visibility.
Fig. 3 gives example client classes AnObserver and Main. Class AnObserver records
notifications in its state. Method main constructs and initializes an Observable,
installs an observer, and invokes notifyAll; upon termination, ob.count = 1 and no
Observable is reachable.
Fig. 4 gives another version of Observable, using a sentinel node [Cormen et al.
1990], for the sake of an example. A more compelling use of sentinels is the version
of Fig. 9 (in Sect. 8), which also uses subclassing and dynamic dispatch.
In Sect. 8 we show equivalence of the versions of Figs. 2 and 4 as an application
of the abstraction theorem and identity extension. The coupling relation describes
6 In

Java, class Object declares methods notify and notifyAll. Here we assume that no superclass
of Observer declares notify and no superclass of Observable declares notifyAll. In the Java versions
of our examples we use different names.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

17

class AnObserver extends Observer {
int count;
unit notify(){ self.count := self.count+1 } }
class Main extends Object {
AnObserver ob;
unit main(){
ob := new AnObserver; Observable obl := new Observable; obl.add(ob); obl.notifyAll() } }
Fig. 3.

Example client for Observable.

class Node2 extends Object { // rep for Observable
Observer ob;
Node2 nxt;
unit setOb(Observer o){ self.ob := o }
unit setNext(Node2 n){ self.nxt := n }
Observer getOb(){ result := self.ob }
Node2 getNext(){ result := self.nxt } }
class Observable extends Object // owner {
Node2 snt; // sentinel node pointing to list
con{ self.snt := new Node2 }
unit add(Observer ob){
Node2 n := new Node2; n.setOb(ob); n.setNext(self.snt.getNext()); self.snt.setNext(n); }
unit notifyAll(){
Node2 n := self.snt.getNext(); while n 6= null do n.getOb().notify(); n := n.getNext() od } }

Fig. 4.

Version of observable that uses sentinel node, in procedural style

the correspondence between a pair of lists, one with and one without a sentinel node
(see Fig. 7). It is enough to say that the same Observer locations are stored in the
lists, in the same order. The state of the Observer is not relevant —nor could it be
in a modular treatment, as class Observer has no fields. To reason about outgoing
calls, namely to notify, it is enough to show that the two implementations make the
same calls. Those calls may lead to calls back to the Observable, but encapsulation
ensures that those calls are the only way the behavior of notify can depend on, or
affect, the Observable.
Except for the bad method of Sect. 2.1, all of the examples discussed so far satisfy
the confinement conditions discussed next.
3.3 Confinement
We need a notion of confinement to prevent representation exposures that invalidate simulation-based reasoning, as discussed in Sect. 2.1. A related issue is how to
formulate simulation. In all the examples, our discussion centered on a corresponding pair of instances for two implementations of the owner class. In particular, the
coupling relations are described for a pair of instances as discussed in Sect. 2.3.
A class- or module-based notion of confinement might rule out leaks, but we aim
for an instance-based notion of simulation suited to the kind of examples we have
discussed. These involve an abstraction provided by a single instance (the owner
object) using a representation accessed via its private fields. So we need to prevent
problematic sharing not only between client and owner but also between different
ACM Journal Name, Vol. V, No. N, Month 20YY.

18

·

A. Banerjee and D. Naumann

Main

Observable
Node

Observer
Fig. 5. Confinement example.
Rounded boxes are
instances of the indicated
class. Solid arrows represent
allowed pointers.
Dashed
boxes indicate owner islands,
each consisting of one owner
and its reps.

Node
Observer
Node

Observer

Observable

PSfrag replacements

Node

Node

instances of the owner class.
Fig. 5 illustrates instance-based owner confinement; in this case Nodes are confined to their owning Observable. Following Hogg [1991], we use the term island for
the sub-heap consisting of an owner and its reps. Dashed lines in the Figure depict
two islands. Our notion of owner confinement imposes four conditions on islands;
here are the first three:
(1) there are no references from a client object to a rep;
(2) there are no references from an owner to reps in a different island;
(3) there are no references from a rep into a different island.
The Figure exhibits most allowed references, but we also allow an owner to reference
another owner (see Fig. 6 on page 33). An example is given in Sect. 9.1. Note that
heap confinement is a state predicate. The full definition, formalized in Sect. 6,
deals with preservation of this predicate by commands and also with leaks via
parameter passing in outgoing method calls from island to client.
In class-based languages with inheritance, there is a subclass (or “protected”)
interface in addition to the public one. This raises the possibility of expressing
encapsulation of reps for not only (instances of) the owner class but also its subclasses. We have chosen the alternative that subclasses are like clients in that fields
they declare may not point to reps. To the list of conditions above we add:
(4) references from an owner’s fields to its reps are only in the private fields of the
owner class.
In order not to abandon the expressiveness of subclassing, however, we allow subclass methods to manipulate reps: they may be constructed, stored in local variACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

19

ables, and passed to the owner. This fits well with the factory pattern [Gamma
et al. 1995] which allows owner behavior to be adapted in owner subclasses without violating encapsulation. To balance the paper, we have deferred the relevant
examples to Sect. 8.
Confinement is formulated using class names. Two incomparable class names,
Own and Rep, are designated. An object is considered to be an owner (respectively,
a rep) if its type is Own (resp. Rep) or a subtype thereof. Incomparability is a mild
restriction that enforces a widely-followed discipline of distinguishing between rep
objects (e.g., nodes in a linked list) and objects representing abstractions (e.g., a
list). The technical benefit of incomparability is that if C and D are incomparable,
which we write C 6≤
> D, then an expression of type C never has a value of type D.
We aim for a perspicuous separation between the semantic property needed for
the abstraction theorem and the syntactic conditions used for static analysis. The
“semantic” property in fact includes conditions on method signatures. For example, we impose the restriction that the return type of a public owner method is
incomparable to Rep; this disallows method bad of Sect. 2.1.
Our use of types to formulate alias restrictions allows heterogeneous data structures, but is slightly restrictive in that there is a single common superclass for all
reps. For more flexibility in practical applications, our theory could be adapted by
taking Own and Rep to be “class types” (“interfaces” in Java), rather than class
implementations. The generalization is straightforward and not illuminating.
The more substantial restriction is due to the fact that class Object is comparable to all classes. Because Java lacks parametric polymorphism, Object is
often used to express generics, e.g., a list containing elements of arbitrary type. A
method to enumerate the list would have return type Object, which violates our
restriction on owner methods. This restriction could be dropped in favor of more
sophisticated conditions to ensure that no rep is returned (see Sect. 12). But in
practice many generics have some sort of constraint expressed by a class or interface type —like Observer in our examples, or Comparable for data structures that
depend on an ordering. These do not run afoul of our restriction. In any case, the
use of Object for generics is widely deplored because it undercuts the benefits of
typing; parametric types are clearly preferable.
Some works on confinement have considered all the confinement properties intended to be satisfied by a program, using hierarchical notions of ownership [Clarke
et al. 2001; Müller 2002]. For example, a Set could own the header of a list which in
turn owns the nodes of the list. This is not necessary for our purposes (see Sect. 12).
To analyse the abstraction provided by the set, we would consider both the header
and nodes to be reps, with a common superclass Rep. On the other hand, to replace
one header implementation by another, Set is irrelevant; we choose Own to be the
header and Rep for the nodes.
4. SYNTAX
This section formalizes the language, for which purpose we adapt some notations
from Featherweight Java [Igarashi et al. 2001].7 To avoid burdening the reader with
straightforward technicalities we deliberately confuse surface syntax with abstract
7 But

the languages differ, e.g., ours has imperative features and private fields.
ACM Journal Name, Vol. V, No. N, Month 20YY.

·

20

A. Banerjee and D. Naumann

syntax. We do not distinguish between classes and class types. We confuse syntactic
categories with names of their typical elements. Barred identifiers like T indicate
finite lists, e.g., T f stands for a list f of field names with corresponding types T .
The bar has no semantic import; T has nothing to do with T .
The grammar is based on given sets of class names (with typical element C), field
names (f ), method names (m), and names (x) for parameters and local variables.
In most respects self and result are like any other variables but self cannot be the
target of assignment.
Grammar
T ::= bool | unit | C

data type

CL ::= class C extends C { T f ; con{ S } M } class declaration
M ::= T m(T x) {S}

method declaration

S ::= x := e | e.f := e
| x := new C

assign to variable, to field
object construction

e

|

x := e.m(e) | x := super.m(e)

method calls

|
|

T x := e in S
if e then S else S fi | S; S

local variable block
conditional, sequence

::= x | null | true | false | it
|
|

e.f | e = e
e is C | (C) e

variable, constant
field access, equality test
type test, cast

Without formalizing it precisely, we assume there is a class Object with no fields
or methods which can be used as a superclass. Additional primitive types, such as
integers, can be treated in the same way as bool and unit (integers can also be
represented, e.g., in unary using linked lists).
In the formal language, expressions do not have side effects. Object construction, new, occurs only as a command x := new C that assigns to a local variable.
Method calls are not expressions but rather occur in special assignments x := e.m(e)
to allow both heap effects and a return value.
Remark 4.1 (syntactic sugar) In examples we use several abbreviations:
—A method call command e.m(e), e.g., self.g.set(true), abbreviates a call assigning
to an otherwise unused local variable.
—Assignment of a new object to a field abbreviates a local block assigning the new
object to a variable that is then assigned to the field.
—Methods that return values but do not mutate state are used in expressions, e.g.,
the argument in self.inout := convertToString(z.getg()) and the target object in
n.getOb().notify(). These are easily desugared using fresh variables and suitable
assignments.
As the language has general recursion, we omit loops. For desugaring loops it would
be convenient to have local or private method declarations, but the module-scoped
methods added in Sect. 10 suffice. The issue is discussed in Sect. 8.1.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

21

A program is given as a class table CT , a finite partial function sending class
name C to its declaration CT (C) which may make mutually recursive references to
other classes. Well formed class tables are characterized using typing rules which
are expressed using some auxiliary functions that in turn depend on the class table,
as is needed to allow mutual recursion. Consider a declaration
CT (C) = class C extends D { T 1 f ; con{ S1 } M } .
To refer to the constructor, we define constr C = S1 . For the direct superclass of
C, we define super C = D. Let M be in the list M of method declarations, with
M = T m(T 2 x) {S2 } .
We record the typing information by defining mtype(m, C) = T 2 →T . (Note that
T 2 →T is not a data type in the language.) The parameter names are given by
pars(m, C) = x. If m has no declaration in CT (C) but mtype(m, D) is defined then
m is an inherited method: we define mtype(m, C) = mtype(m, D) and pars(m, C) =
pars(m, D). For the declared fields, we define type(f , C) = T 1 and dfields C =
(f : T 1 ). Here f : T 1 denotes a finite mapping of field names to types. To include
inherited fields, we define fields C = dfields C ∪fields D and assume f is disjoint from
the names in fields D. The built-in class Object has no methods and fields(Object)
is the empty list.
A typing context Γ is a finite mapping from variable and parameter names to
data types, such that self ∈ d om Γ. Whereas the Java format T x is used in code to
give x type T, it is written x:T in typing contexts. Typing of commands for methods
declared in class C is expressed using judgements Γ ⊢ S where Γ self = C. Moreover,
if mtype(m, C) = T →T then Γ x = T and Γ result = T .8 For brevity, we sometimes
say “command” to refer to a derivable judgement Γ ⊢ S. The judgement Γ ⊢ e : T
says that expression e has type T . The constructor is typed using a judgement
self : C ⊢ S : con which is distinguished from the typing of S as a command, as the
former is used to define the semantics of S as a constructor, which in turn is used
in the semantics of object construction (new).
Definition 4.2 (subtyping , ≤) The class table determines a subtyping relation
≤ as follows. If T or U is bool or unit then define T ≤ U iff T = U . For class
types C and D, define C ≤ D iff either C = D or super C ≤ D.
Subsumption is built into the rules for specific constructs. For example, the assignment rule allows x : D, y : E, self : C ⊢ x := y provided that E ≤ D.
The constructor for one class may construct objects of other classes (Fig. 4 is
an example). But we prefer not to model divergence due to cyclic constructor
dependencies as in the following.
class B extends Object { B f ; con{ self.f := new C} }
class C extends B { con{ skip } }
(Recall that to initialize a C object both the B- and C-constructor are applied.)
8 In [Banerjee and Naumann 2002a] we make C an explicit, and redundant, part of the judgement,
and we use separate return statements rather than variable result.

ACM Journal Name, Vol. V, No. N, Month 20YY.

22

·

A. Banerjee and D. Naumann

Definition 4.3 (constructor dependence, ⊏) For B, C ranging over declared
classes, we say that C has constructor dependence on B, written B ⊏ C, iff B ⊏
(super C) or x := new B occurs in constr C, for some x.
Note that B ⊏ C just if the constructor of C or one of its ancestor classes contains
new B (by which we mean x := new B for some x). The transitive closure ⊏+ has
B ⊏+ C just if construction of a C-object entails construction of a B-object. For
the example above we have C ⊏ B and C ⊏ C.
Definition 4.4 (well formed class table) A class table is well formed provided
it satisfies the following conditions.
—Each class declaration class C extends D { T f ; con{ S } M } is well formed,
that is, each method declaration M in M is well formed, and self : C ⊢ S : con,
according to the rules to follow.
—If C occurs as the type of a field or parameter in some class then CT (C) is
defined. No field or method has multiple declarations in a class.
—The subclass relation ≤ is antisymmetric.
—Transitive constructor dependence, ⊏+ , is antisymmetric and irreflexive.
The rules are straightforward renderings of the typing rules for Java, for private
fields, public methods and public classes [Arnold and Gosling 1998].
Typing of constructors
S = constr C

self : C ⊢ S no method calls occur in S
self : C ⊢ S : con

Typing of method declarations
x : T , self : C, result : T ⊢ S
mtype(m, super C) is undefined or equals T →T
pars(m, super C) is undefined or equals x
C ⊢ T m(T x){S}

In this method rule, the condition on mtype is the standard invariance restriction
on method types, as in Java [Arnold and Gosling 1998; Abadi and Cardelli 1996].
The last antecedent in the rule, concerning pars(m, D), ensures that all declarations
of a method use the same parameter names. This loses no generality and slightly
streamlines the formalization of the semantic domains in the sequel.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

23

Typing of expressions
Γ ⊢ x : Γx Γ ⊢ null : B

Γ ⊢ it : unit Γ ⊢ true : bool Γ ⊢ false : bool

Γ ⊢ e1 : T 1 Γ ⊢ e2 : T 2
Γ ⊢ e1 = e2 : bool

Γ ⊢ e : (Γ self)

Γ ⊢ e:D B ≤ D
Γ ⊢ (B) e : B

(f : T ) ∈ dfields(Γ self)
Γ ⊢ e.f : T

Γ ⊢ e:D B ≤ D
Γ ⊢ e is B : bool

The rule for equality test allows comparison of arbitrary data types, and is reference equality in the case of class types. But if e1 and e2 have types not related
by ≤, the test e1 = e2 is false except when both are nil. The rule for field access
enforces private visibility: only a method declaration in class C can access fields
declared in CT (C). It can access those fields on any object of its type; to access
its own fields the expression is self.f . The rule for cast is standard.9
Typing of commands

Γ ⊢ e:T

Γ ⊢ e1 : (Γ self) (f : T ) ∈ dfields(Γ self)
Γ ⊢ e2 : U U ≤ T
Γ ⊢ e1 .f := e2

T ≤ Γ x x 6= self
Γ ⊢ x := e

Γ ⊢ e : D mtype(m, D) = T →T
Γ ⊢ e : U U ≤ T x 6= self T ≤ Γ x
Γ ⊢ x := e.m(e)
B ≤ Γx

mtype(m, super(Γ self)) = T →T
Γ ⊢ e : U U ≤ T x 6= self T ≤ Γ x
Γ ⊢ x := super.m(e)

x 6= self B 6= Object
Γ ⊢ x := new B

Γ ⊢ e : bool Γ ⊢ S1 Γ ⊢ S2
Γ ⊢ if e then S1 else S2 fi

Γ ⊢ e:U

Γ ⊢ S1 Γ ⊢ S2
Γ ⊢ S1 ; S2
U ≤ T x 6= self (Γ, x : T ) ⊢ S
Γ ⊢ T x := e in S

The command rules have hypotheses involving partial functions which must be
defined for the hypothesis to be satisfied. For example, in the rule for super calls,
mtype(m, super C) must be defined and equal to T →T .
Each expression and command construct is the conclusion of exactly one typing
rule, and there are no other rules. Thus we have the following.
Lemma 4.5 A typing Γ ⊢ S or Γ ⊢ e : T has at most one derivation.
9 It is not adequate for expressions that arise through substitutions used in program logic (see Cavalcanti and Naumann [1999]) and in small-step semantics (see Igarashi et al. [2001]); the latter
source uses the term “stupid cast” for the typing rule that allows (B) e when B is not a subclass
of the static type of e.

ACM Journal Name, Vol. V, No. N, Month 20YY.

24

·

A. Banerjee and D. Naumann

Definition 4.6 (inheritance) Method m is inherited in C from B if C ≤ B,
there is a declaration for m in B, and there is no declaration for m in any D such
that C ≤ D < B. To make the class table explicit, we also say m is inherited from
B in CT (C).
Because the language has single inheritance, the subtyping relation ≤ is a tree: if
D ≤ B and D ≤ C then B ≤ C or C ≤ B. If mtype(m, C) is defined for some C
then it is defined for all subclasses of C. For a given method name m and class C,
there is a unique ancestor class declaring m that is least with respect to ≤.
Lemma 4.5 allows proofs by structural induction on typings. The following notion
facilitates induction on inheritance chains.
Definition 4.7 (method depth) For any m and C such that mtype(m, C) is
defined, the method depth of C for m in CT is defined by depth(m, C) = 1 +
depth(m, super C) if mtype(m, super C) is defined; otherwise, depth(m, C) = 0.
An immediate consequence is that if mtype(m, C) is defined and depth(m, C) = 0
then CT (C) has a declaration for m.
Finally, we consider ramifications of constructor dependence. Note that Object 6⊏
C for all C, by the typing rule for new.
Definition 4.8 (semantic dependence, ≪) As an auxiliary notation, we define
B - C iff {D | D ⊏+ B} ⊆ {D | D ⊏+ C} and write B ≺ C if this inclusion is
proper. For classes B, C declared in the class table, define B ≪ C iff B ≺ C or
both B - C and B > C.
Lemma 4.9 For a well formed class table we have the following.
(1) ≪ is well founded.
(2) super C ≪ C for all C.
(3) B ⊏ C implies B ≪ C for all B and C.
Proof. Note that - is a preorder but not antisymmetric, so ≪ is not a lexicographic order per se. To prove (1), define deps C = {D | D ⊏+ C} for any C. Then
we have B ≪ C iff (deps B, B) ⋖ (deps C, C), where ⋖ is defined by (X, B) ⋖ (Y, C)
iff X ( Y or X ⊆ Y and B > C (where ( means proper subset). This is logically
equivalent to: X ( Y or X = Y and B > C, which shows that the definition is the
lexicographic coupling of ( and >. As ( here is for finite subsets of declared class
names, both ( and > are well founded, hence so is their lexicographic coupling.
For (2), if D ⊏+ super C then D ⊏+ C by definition of ⊏; hence super C - C.
Also, super C > C, so (2) holds by definition of ≪.
For (3), suppose B ⊏ C. Then, by transitivity, {D | D ⊏+ B} ⊆ {D | D ⊏+ C}.
Also, we have B ⊏+ C but B 6⊏+ B, by well formedness of the class table, so the
inclusion is proper. That is, B ≺ C, whence B ≪ C by definition of ≪.
5. SEMANTICS
This section defines the semantic domains, then the semantics of expressions and
commands, and finally the semantics of well formed class tables.
Because methods are associated with classes rather than with instances, the
semantic domains are rather simple. There are no recursive domain equations
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

25

to be solved: subclassing (≤) is acyclic and the cycle of recursive references via
class fields is broken via the heap. Mutually recursive method invocations can arise
through direct calls on a single object and also through callbacks between reachable
objects, as for example in the observer pattern. We impose no restrictions on such
calls. A fixpoint construction is used for the method environment which comprises
the semantics of the class table.
The interdependence between constructors and object construction commands
(new) is a bit complex; things pertaining to constructors may be skipped on first
reading. As a way of explaining the fine points, we prove in some detail that the
semantics is well defined (Lemma 5.7).
Often we write = between expressions involving partial functions such as those
used in typing. Unless otherwise indicated, it means strong equality: both sides
are defined and equal.
5.1 Semantic domains
The state of a method in execution is comprised of a heap h, which is a finite10
partial function from locations to object states, and a store η, which assigns locations and primitive values to the local variables and parameters given by a typing
context Γ.11 An object state is a mapping from field names to values. Function
application associates to the left, so h ℓ f is the value of field f of the object h ℓ at
location ℓ.
A command denotes a function mapping each initial state (h, η) either to a final
state (h0 , η0 ) or to the distinguished value ⊥. We use the term global state for
(h, η), to distinguish it from object states. The improper value ⊥ represents nontermination as well as runtime errors: attempts to dereference nil or cast a location
to a type it does not have.
In some languages it is a runtime error to dereference a dangling pointer, i.e.,
one not in the domain of the heap. In Java dangling pointers cannot arise: there
is no command for deallocation and a correct garbage collector never deallocates
reachable objects. For our purposes, garbage collection need not be modelled.
Commands act on heaps and stores that are closed in the sense that all locations
that occur are in the domain of the heap. The following paragraphs formalize our
assumptions about locations and then define the semantic domains.
For locations, we assume that a countable set Loc is given, along with a distinguished value nil not in Loc. To track each object’s class we assume given a
function loctype : Loc → ClassNames such that for each C there are infinitely many
locations ℓ with loctype ℓ = C. We use the term heap for any partial function h
such that d om h ⊆fin Loc and each h ℓ is an object state of type loctype ℓ. Object
states are formalized later. Because the domain of a heap is finite, the assumption
about loctype ensures an adequate supply of fresh locations.
Definition 5.1 (allocator, parametric) An allocator is a location-valued function fresh such that loctype(fresh(C, h)) = C and fresh(C, h) 6∈ dom h, for all
10 The

preliminary version [Banerjee and Naumann 2002a] of this paper has a bug: infinite heaps
are allowed, and it is not required that there be unallocated locations at every type.
11 In [Banerjee and Naumann 2002a] we use the term “environment” for η, wishing to avoid the
irrelevant connotations of “stack”; here we use “store”, following Reynolds [2001].
ACM Journal Name, Vol. V, No. N, Month 20YY.

26

·

A. Banerjee and D. Naumann

C, h. An allocator is parametric if dom h1 ∩ locs C = dom h2 ∩ locs C implies
fresh(C, h1 ) = fresh(C, h2 ).
For example, taking Loc = N, a parametric allocator is given by the function
fresh(C, h) = min{ℓ | loctype ℓ = C ∧ ℓ 6∈ dom h}.
Typical implementations encode the object class as part of its state. One could
uncurry this representation of heaps and take Loc to be N × ClassN ames. Then
fresh(C, h) could return (n, C) where n is the least address of an unused memory
segment of sufficient size for the state of C. This is an allocator but not parametric
because the presence of objects of one class affect the availability of memory for
objects of other classes.
We define the semantics in terms of an arbitrary allocator fresh. The assumption of parametricity is stated explicitly where it is needed, namely for the first
abstraction theorem (Sect. 7) but not the second (Sect. 10). Parametricity of the
allocator is a reasonable assumption for some applications but not all. The assumption streamlines the proof of the abstraction theorem, allowing us to highlight
other issues.
In addition to heaps, it is convenient to name a number of other semantic categories that are explained in due course.
Semantic categories
θ ::= T | Γ | state C | Heap | Heap ⊗ Γ | Heap ⊗ T | θ⊥ | C, x, T →T | MEnv

In order to define the more complicated semantic domains, we need to define
closed stores. Stores are among the simpler semantic domains, which are defined
as follows.
Semantics of types, object states, and stores
[[bool]]
[[unit]]
[[C]]
[[state C]]
[[Γ]]

=
=
=
=
=

{true, false}
{it}
{nil} ∪ locs(C↓)
{s | d om s = d om(fields C) ∧ ∀(f : T ) ∈ fields C • sf ∈ [[T ]]}
{η | d om η = d om Γ ∧ η self 6= nil ∧ ∀x ∈ d om η • η x ∈ [[Γ x]]}

We write locs C for {ℓ ∈ Loc | loctype ℓ = C}, and locs(C↓) for {ℓ | loctype ℓ ≤ C}.
There is no independent meaning for C↓. As small dot has another use, we use the
fat dot • to separate a bound variable from its scope. Note that [[Γ]] is defined for
Γ both with and without result in its domain.
Definition 5.2 (closed heap and store) A heap h is closed, written closed h,
iff rng(h ℓ) ∩ Loc ⊆ d om h, for all ℓ ∈ d om h. A store η ∈ [[Γ]] is closed in heap h,
written closed(h, η), iff rng η ∩ Loc ⊆ d om h.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

27

Recall that fresh locations should occur nowhere in the global state. For a closed
store and heap, this follows from the requirement that fresh(C, h) 6∈ dom h.12
Semantics of global states and methods

[[Heap]]
[[Heap ⊗ Γ]]
[[Heap ⊗ T ]]
[[θ⊥ ]]
[[C, x, T →T ]]
[[MEnv ]]

=
=
=
=
=
=

{h | d om h ⊆fin Loc ∧ closed h ∧ ∀ℓ ∈ d om h • hℓ ∈ [[state (loctype ℓ)]]}
{(h, η) | h ∈ [[Heap]] ∧ η ∈ [[Γ]] ∧ closed(h, η)}
{(h, d) | h ∈ [[Heap]] ∧ d ∈ [[T ]] ∧ (d ∈ Loc ⇒ d ∈ d om h)}
[[θ]] ∪ ⊥ (where ⊥ is some fresh value not in [[θ]])
[[Heap ⊗ (x : T , self : C)]] → [[(Heap ⊗ T )⊥ ]]
{µ | ∀C, m • µCm is defined iff mtype(m, C) is defined,
and µCm ∈ [[C, pars(m, C), mtype(m, C)]] if µCm defined }

Just as a class declaration CT (C) gives a collection of method declarations, the
semantics of a class table is a method environment that assigns to each class C a
method meaning µ C m for each m declared or inherited in C.
For the fixpoint construction of the method environment denoted by a class
table, we need to impose order on the semantic domains. We use the term complete partial order for a poset with least upper bounds of countable ascending
chains [Davey and Priestley 1990]. The degenerate case is ordering by equality,
which is the order we use for the semantics of T , Γ, state C, Heap, (Heap ⊗ Γ),
and (Heap ⊗ T ). Then [[(Heap ⊗ Γ)⊥ ]] and [[(Heap ⊗ T )⊥ ]] are complete partial orders with the “flat” order: ⊥ is below anything and other comparable elements
are equal. The set [[C, x, T →T ]] is defined to be the space of total functions
[[Heap ⊗ (x : T , self : C)]] → [[(Heap ⊗ T )⊥ ]], all of which are continuous because
Heap ⊗ (x : T , self : C) is ordered by equality. The function space itself is ordered
pointwise, making it a complete partial order with minimum element λ(h, η) • ⊥.
Finally, we order [[MEnv ]] pointwise. All method environments µ in [[MEnv ]] have
the same domain, determined by CT , so this is also a complete partial order, taken
pointwise. It has a minimum element, namely λC • λm • λ(h, η) • ⊥.
Whereas [[state C]] consists of the states for objects of exactly class C, the set
[[C]] is downward closed. For data types T1 , T2 we have T1 ≤ T2 ⇒ [[T1 ]] ⊆ [[T2 ]].
Definition 5.3 (incomparable, 6≤
>) We write C 6≤
> B for C  B ∧ C 6≥ B. For a
list C, C 6≤
> B means C 6≤
> B for all C in C.
Lemma 5.4 For classes C, B, if C 6≤
> B then [[C]] ∩ [[B]] = {nil}. For primitive T
we have [[T ]] ∩ [[B]] = ∅.
The result is a direct consequence of the definitions. We often use the contrapositive:
if there is a non-nil location in both [[B]] and [[C]] then B ≤ C or C ≤ B.
12 If

dangling pointers were allowed, the definition of freshness would need to be with respect to
both the store and all object states in the heap. The issue becomes apparent in the proof of
Lemma 6.16 in the sequel, which uses closure. Most of the other definitions and results can be
formulated without restricting heaps to be closed, so we mistakenly neglected closure in [Banerjee
and Naumann 2002a].
ACM Journal Name, Vol. V, No. N, Month 20YY.

28

·

A. Banerjee and D. Naumann

5.2 Semantics of expressions, commands, constructors and methods
For expressions and commands, the semantics is defined by induction on typing
derivations. As a consequence of uniqueness of typing derivations, Lemma 4.5, the
semantics is a function of typings. The meaning of a command Γ ⊢ S will be defined
to be a function
[[Γ ⊢ S]] ∈ [[MEnv ]] → [[Heap ⊗ Γ]] → [[(Heap ⊗ Γ)⊥ ]] .
The meaning of an expression Γ ⊢ e : T will be defined to be a function
[[Γ ⊢ e : T ]] ∈ [[Heap ⊗ Γ]] → [[T⊥ ]]
such that the result value is always in the domain of the heap if it is a location.13
This is part of Lemma 5.7, the proof of which serves as an exposition for some
details of the semantic definitions.
The command and expression constructs are strict in ⊥, except, as usual, for the
then- and else-commands in if −fi. To streamline the treatment of ⊥ in the semantic
definitions we use a metalanguage construct which some readers will recognize as the
bind operation of the lifting monad [Moggi 1991]. The construct let d = E1 in E2
has the following meaning: If the value of E1 is ⊥ then that is the value of the
entire let expression; otherwise, its value is the value of E2 with d bound to the
value of E1 .
We let (h, η) ∈ [[Heap ⊗ Γ]] in the following definitions. Identifiers are as in
the corresponding typing rules. For semantic values we use the identifier d, but
sometimes ℓ for elements of the sets [[C]].
For expressions the semantics is straightforward; we choose the Java semantics
for casts and tests.

Semantics of expressions

13 We

have chosen a simple but slightly inelegant formulation. We express closure of the result
for commands in the semantic domain whereas for expressions there is no returned heap and
we express closure as a property of the semantic function. The presentation could be made
more elegant by introducing categories exp(Γ, T ) and com(Γ) with [[com(Γ)]] = [[MEnv ]] →
[[Heap ⊗ Γ]] → [[(Heap ⊗ Γ)⊥ ]] and imposing the restriction on return values in the definition of
[[exp(Γ, T )]] as a subset of [[Heap ⊗ Γ]] → [[T⊥ ]]. We could even restrict the meanings to those
that are confined, but the gain in elegance would come at the expense of complexity that not
all readers would find illuminating. We have chosen to treat confinement and parametricity as
properties to be proved after the semantics is defined, downplaying the model as an independent
structure. Thus little would be gained by naming categories exp(Γ, T ) and com(Γ).
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

[[Γ ⊢ x : T ]](h, η)
[[Γ ⊢ null : B]](h, η)
[[Γ ⊢ it : unit]](h, η)
[[Γ ⊢ true : bool]](h, η)
[[Γ ⊢ false : bool]](h, η)
[[Γ ⊢ e1 = e2 : bool]](h, η)

[[Γ ⊢ e.f : T ]](h, η)
[[Γ ⊢ (B) e : B]](h, η)
[[Γ ⊢ e is B : bool]](h, η)

·

29

=
=
=
=
=
=

ηx
nil
it
true
false
let d1 = [[Γ ⊢ e1 : T1 ]](h, η) in
let d2 = [[Γ ⊢ e2 : T2 ]](h, η) in
if d1 = d2 then true else false
= let ℓ = [[Γ ⊢ e : (Γ self)]](h, η) in
if ℓ = nil then ⊥ else h ℓ f
= let ℓ = [[Γ ⊢ e : D]](h, η) in
if ℓ = nil ∨ loctype ℓ ≤ B then ℓ else ⊥
= let ℓ = [[Γ ⊢ e : D]](h, η) in
if ℓ 6= nil ∧ loctype ℓ ≤ B then true else false

The semantics of commands is defined by structural induction on the command,
except for object construction x := new C which also depends on the constructor
semantics of the constructor, constr C, of C. That in turn depends on the constructor of super C, and on the command semantics of constr C. Well foundedness
of this dependence is part of the proof of Lemma 5.7.
In the semantics of commands, we write fields B 7→ defaults as an abbreviation
for the function sending each f ∈ d om(fields B) to the default value for type(f, B).
The defaults are false for bool, it for unit, and nil for classes. Function update or
extension is written, e.g., [η | x 7→ d]. We write ⇂ for domain restriction: if x is in
the domain of η then η ⇂ x is the function like η but without x in its domain.

Semantics of commands

ACM Journal Name, Vol. V, No. N, Month 20YY.

30

·

A. Banerjee and D. Naumann

[[Γ ⊢ x := e]]µ(h, η)
[[Γ ⊢ e1 .f := e2 ]]µ(h, η)

= let d = [[Γ ⊢ e : T ]](h, η) in (h, [η | x 7→ d])
= let ℓ = [[Γ ⊢ e1 : (Γ self)]](h, η) in
if ℓ = nil then ⊥ else
let d = [[Γ ⊢ e2 : U ]](h, η) in
([h | ℓ 7→ [hℓ | f 7→ d]], η)
[[Γ ⊢ x := new B]]µ(h, η)
= let ℓ = fresh(B, h) in
let h1 = [h | ℓ 7→ [fields B 7→ defaults]] in
let η1 = [self 7→ ℓ] in
let h0 = [[self : B ⊢ constr B : con]]µ(h1 , η1 ) in
(h0 , [η | x 7→ ℓ])
= let ℓ = [[Γ ⊢ e : D]](h, η) in
[[Γ ⊢ x := e.m(e)]]µ(h, η)
if ℓ = nil then ⊥ else
let x = pars(m, D) in
let d = [[Γ ⊢ e : U ]](h, η) in
let η1 = [x 7→ d, self 7→ ℓ] in
let (h1 , d1 ) = µ(loctype ℓ)m(h, η1 ) in
(h1 , [η | x 7→ d1 ])
= let ℓ = η self in
[[Γ ⊢ x := super.m(e)]]µ(h, η)
let x = pars(m, Γ self) in
let d = [[Γ ⊢ e : U ]](h, η) in
let η1 = [x 7→ d, self 7→ ℓ] in
let (h1 , d1 ) = µ(super(Γ self))m(h, η1 ) in
(h1 , [η | x 7→ d1 ])
[[Γ ⊢ S1 ; S2 ]]µ(h, η)
= let (h1 , η1 ) = [[Γ ⊢ S1 ]]µ(h, η) in
[[Γ ⊢ S2 ]]µ(h1 , η1 )
[[Γ ⊢ if e then S1 else S2 fi]]µ(h, η) = let b = [[Γ ⊢ e : bool]](h, η) in
if b then [[Γ ⊢ S1 ]]µ(h, η) else [[Γ ⊢ S2 ]]µ(h, η)
[[Γ ⊢ T x := e in S]]µ(h, η)
= let d = [[Γ ⊢ e : U ]](h, η) in
let η1 = [η | x 7→ d] in
let (h1 , η2 ) = [[(Γ, x : T ) ⊢ S]]µ(h, η1 ) in
(h1 , (η2 ⇂x))

Method calls of the form x := e.m(e) are dynamically bound: the method meaning is determined by loctype ℓ in the semantic definition, where ℓ is the value of
e. By typing, loctype ℓ ≤ D and pars(m, loctype ℓ) = pars(m, D). Super-calls are
statically bound: the method meaning used, µ(super C)m, is determined by the
static class C. Note that if mtype(m, super C) is defined, as required by the typing
rule, then pars(m, C) = pars(m, super C).
The meaning of a command S as a constructor is a function
[[self : C ⊢ S : con]] ∈ [[MEnv ]] → [[Heap ⊗ self : C]] → [[Heap ⊥ ]] .
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

31

Dependence on [[MEnv ]] is a formal technicality: the semantic definition uses the
command semantics of S, but the typing rule disallows method calls in S.
Semantics of constructor
[[self : C ⊢ S : con]]µ(h, η) = let B = super C in
let S0 = constr B in
let h1 = if B 6= Object
then [[self : B ⊢ S0 : con]]µ(h, η) else h in
let (h0 , −) = [[self : C ⊢ S]]µ(h1 , η) in
h0
Note that if [[self : B ⊢ S0 : con]]µ(h, η) or [[self : C ⊢ S]]µ(h1 , η) is ⊥ then so is
[[self : C ⊢ S : con]]µ(h, η). The result ⊥ is possible due to nil dereferences and cast
failures but not divergence (because there are no method calls or cyclic constructor
dependencies).
Semantics of method declaration
Suppose M is a method declaration in CT (C), with M = T m(T x){S}. Its
meaning [[M ]] is the total function [[MEnv ]] → [[C, x, T →T ]] defined by
[[M ]]µ(h, η) = let η1 = [η | result 7→ default ] in
let (h0 , η0 ) = [[x : T , self : C, result : T ⊢ S]]µ(h, η1 ) in
(h0 , η0 result)
For precision in the semantics of a method inherited in C from B we make an
explicit definition for the domain-restriction of a method meaning in [[B, x, T →T ]]
to the global states (h, η) in [[Heap ⊗ x : T , self : C]].
Definition 5.5 (restr ) For d ∈ [[B, x, T →T ]] and C ≤ B, define restr(d, C), an
element of [[C, x, T →T ]], by restr(d, C)(h, η) = d(h, η).
Semantics of class table and its approximation chain µj
The semantics of a well formed class table CT , written [[CT ]], is the least upper
bound of the ascending chain µ ∈ N → [[MEnv ]] defined as follows.
µ0 C m = λ(h, η) • ⊥
if m is declared or inherited in C
µj+1 C m = [[M ]]µj
if m is declared as M in C
µj+1 C m = restr ((µj+1 B m), C) if m is inherited in C from B
Remark 5.6 (On proofs) We give some proofs in considerable detail. To avoid
repetition, we use the same identifiers as in the relevant semantic definition for
each case —often different from those in the statement of the result being proved—
taking care to avoid ambiguity. This saves explicit introduction of the identifiers
ACM Journal Name, Vol. V, No. N, Month 20YY.

32

·

A. Banerjee and D. Naumann

or mention of the ranges and scopes of quantification. But it requires the reader to
keep an eye on the semantic clauses. Often, without remark, we consider only the
case where the outcome and various intermediate values are non-⊥, as the ⊥ cases
are straightforward.
Lemma 5.7 (semantics is well defined and typed) Let CT be well formed.
(1) If C ≤ B then for any Γ with self 6∈ d om Γ we have [[Heap ⊗ Γ, self : C]] ⊆
[[Heap ⊗ Γ, self : B]].
(2) If Γ ⊢ e : T then [[Γ ⊢ e : T ]] ∈ [[Heap ⊗ Γ]] → [[T⊥ ]].
(3) If (h, η) ∈ [[Heap ⊗ Γ]] and d = [[Γ; C ⊢ e : T ]](h, η) with d 6= ⊥ then (h, d) ∈
[[Heap ⊗ T ]].
(4) If Γ ⊢ S then [[Γ ⊢ S]] ∈ [[MEnv ]] → [[Heap ⊗ Γ]] → [[(Heap ⊗ Γ)⊥ ]].
(5) [[CT ]] is well defined.
Proof. (1) follows easily from the fact that C ≤ B implies [[C]] ⊆ [[B]].
For (2), inspection of the definitions shows that [[Γ; C ⊢ e : T ]](h, η) is in [[T⊥ ]].
It is property (h, d) ∈ [[Heap ⊗ T ]], i.e., (3), that we need explicitly in some proof
steps. This holds because (h, η) is closed and no expression creates fresh locations.
Property (4) requires a straightforward but not entirely trivial check that, for any
µ, [[Γ; C ⊢ S]]µ(h, η) is in [[(Heap ⊗ Γ)⊥ ]]. For example, in the case of method call
x := e.m(e) we need the fact that µCm is in [[C, pars(m, C), mtype(m, C)]] regardless
of whether m is declared or inherited in C. The store η1 is passed to the method
meaning µ(loctype ℓ)m determined by the type, loctype ℓ, of the target. Note that
η1 self = ℓ and µ(loctype ℓ)m is from a declaration in loctype ℓ or a superclass, so η1
is in its domain by (1). Of course the call aborts if ℓ = nil .
For (5), acyclicity of ≤ ensures that the semantics of the class table is well founded
on inheritance depth. And (1) ensures that the definition µj+1 C m for an inherited
method yields a value in the semantic domain [[C, pars(m, C), mtype(m, C)]]. We
only take fixpoints for method environments, which form a complete partial order
with bottom. The fixpoint is well defined because the meaning [[M ]] of a method
declaration M is a continuous functions of the method environment. This is because
each [[Γ ⊢ S]] is a continuous function on method environments —which in turn
depends on the fact that the semantic definitions for commands are continuous in
their constituent commands and expressions.
The semantics of object construction commands (new) is mutually dependent
on the semantics of constructors. This is resolved as follows.
First, the semantics of constructors is defined by well founded recursion on the
order ≪ on classes. For semantics of self : B ⊢ constr B : con we use both (a) the
constructor semantics of self : (super B) ⊢ constr(super B) : con and (b) the command semantics for constr B. For (a), note that super C ≪ C by Lemma 4.9. For
(b), note that if constr C uses new B for other classes B, we have B ⊏ C by a
condition on well formed class tables; then B ≪ C by Lemma 4.9. Note that there
is no dependence on the method environment.
Finally, for semantics of methods we need all constructors as there is no restriction
on which objects can be constructed. The semantics of methods is by structural
recursion on method bodies, using the semantics of constructors.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

clients

Ch

owners

Ohj

Ohi

reps

Rhj

Rhi

PSfrag replacements

·

33

Fig. 6. Confinement scheme for island j. Dashed boxes are partition
blocks. Solid lines indicate allowed
references and dotted lines indicate
prohibited ones. There is no restriction within blocks.

6. CONFINEMENT RAMIFIED
Our aim is to support reasoning where simulations are specified on a per-island
basis, where an island consists of a single owner and its reps.14 This section formalizes a semantic notion of confinement suited to this purpose. In particular, it
takes into account the limited access to reps allowed for owner subclasses, which is
discussed further in Sect. 9.
6.1 Confinement of states
As discussed in Sect. 3.2 we assume that class names Own and Rep are given, such
that Own 6≤
> Rep and thus [[Own]] ∩ [[Rep]] = {nil}. As an abbreviation, we write
locs(Own↓, Rep↓) for locs(Own↓) ∪ locs(Rep↓).
We say heaps h1 and h2 are disjoint if d om h1 ∩ d om h2 = ∅. Let h1 ∗ h2 be the
union of h1 and h2 if they are disjoint, and undefined otherwise.
We shall partition the heap as h = Ch ∗ . . . where Ch contains client objects and
the rest is partitioned into islands of the form Oh ∗ Rh consisting of a singleton
heap Oh with an owner object and a heap Rh of its representation objects. In such
a partition, the heaps Ch, Oh, and Rh need not be closed. An example is Fig. 5 in
Sect. 3.3; the general scheme is depicted in Fig. 6. Our use of the word “partition”
is slightly non-standard: we allow the blocks Rh i and Ch to be empty.
Definition 6.1 (admissible partition) An admissible partition of heap h is a
set of pairwise disjoint heaps Ch, Oh 1 , Rh 1 , . . . , Oh k , Rh k , for k ≥ 0, with
h = Ch ∗ Oh 1 ∗ Rh 1 ∗ . . . ∗ Oh k ∗ Rh k
14 In

particular, this entails describing how a simulation is established by an owner constructor
acting on a single owner object. As constructors have no parameters, one could define the semantics in terms of constructors applied to a single object and yielding a small heap. But such
a constructor will in fact be executed in a larger heap. Suppose (h, η) ∈ [[Heap ⊗ Γ]], so that
everything reachable from η is already in h. If h′ is a heap, not necessarily closed, such that
h′ ∗ h is in [[Heap]], then it is immediate from the definitions that (h′ ∗ h, η) is in [[Heap ⊗ Γ]]. For
any S and µ we have [[Γ ⊢ S]]µ(h, η) = ⊥ iff [[Γ ⊢ S]]µ(h′ ∗ h, η) = ⊥, as can be shown using the
fact that [[Γ ⊢ e : T ]](h′ ∗ h, η) = [[Γ ⊢ e : T ]](h, η). (Strictly speaking, this depends on µ having the
property; and then one shows that [[CT ]] has the property.) What is not true is the following: if
(h0 , η0 ) = [[Γ ⊢ S]]µ(h, η) then [[Γ ⊢ S]]µ(h′ ∗ h, η) = (h′ ∗ h0 , η0 ). The reason is that the allocator
fresh depends on the domain of the entire heap, and we have made no assumptions to relate its
behavior on h and h′ ∗ h.
We have not checked the details but it seems clear that if (h0 , η0 ) = [[Γ ⊢ S]]µ(h′ ∗ h, η) then
there is h′0 such that h0 = h′ ∗ h′0 and (h′0 , η0 ) ∈ [[Heap ⊗ Γ]]. Also, for S without method calls and
satisfying the dependency condition for constructors (Def. 4.4), if h0 = [[Γ ⊢ S : con]]µ(h′ ∗ h, η)
then there is h′0 such that h0 = h′ ∗ h′0 . But to be useful for our purposes this property would
have to be strengthened to take partitions into account.
ACM Journal Name, Vol. V, No. N, Month 20YY.

34

·

A. Banerjee and D. Naumann

and for all i (1 ≤ i ≤ k)
—d om Oh i ⊆ locs(Own↓) and size(d om Oh i ) = 1
—d om Rh i ⊆ locs(Rep↓)
—d om Ch ∩ locs(Own↓, Rep↓) = ∅

(owner blocks)
(rep blocks)
(client blocks)

Definition 6.2 (confined heap, confining partition, 6❀) To say that no object in h1 contains a reference to an object in h2 , we define 6❀ by
h1 6❀ h2 ⇔ ∀ℓ ∈ d om h1 • rng(h1 ℓ) ∩ d om h2 = ∅ .
To say that no object in h1 contains a reference to an object in h2 except via a field
in f , we define 6❀f by
h1 6❀f h2 ⇔ ∀ℓ ∈ d om h1 • rng((h1 ℓ)⇂f ) ∩ d om h2 = ∅ .
A heap h is confined, written conf h, iff it has a confining partition. A confining
partition is an admissible partition such that for all j, i with j 6= i we have
(1) Ch 6❀ Rh j
(2) Oh j ❀
6 Rh i

(clients do not point to reps)
(owners do not share reps)

(reps are private to Own)
(3) Oh j 6❀g Rh j where g = d om(dfields(Own))
(4) Rh j ❀
6 Oh i ∗ Rh i
(reps are confined to their islands)
A heap may have several admissible partitions, because there is no inherent order
on islands and because unreachable reps can be put in any island. The definitions
and results do not depend on choice of partition. We have not found a workable
formulation that determines unique partitions. To describe the effect of confined
commands on partitions we use the following.
Definition 6.3 (extension of confining partition, ✂) Define h ✂ h0 iff h is
confined and for any confining partition of h,
h = Ch ∗ Oh 1 ∗ Rh 1 ∗ . . . ∗ Oh k ∗ Rh k

(k ≥ 0),

there is a confining partition of h0 ,
h0 = Ch 0 ∗ Oh 01 ∗ Rh 01 ∗ . . . ∗ Oh 0n ∗ Rh 0n ,
that is an extension in the sense that it satisfies the following:
—n ≥ k
—d om(Ch) ⊆ d om(Ch 0 )
—d om(Oh j ) ⊆ d om(Oh 0j ) for all j ≤ k
—d om(Rh j ) ⊆ d om(Rh 0j ) for all j ≤ k
Confinement of a store depends on the class in which it may occur. For owners
and reps it depends on the domain of the heap as well.
Definition 6.4 (confined store, global state) Let h be a confined heap and η
be a store in [[Γ, self : C]] for some Γ. We say η is confined in h for C iff
(1) C  Rep ∧ C  Own ⇒ rng η ∩ locs(Rep↓) = ∅
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

35

(2) C ≤ Own ⇒ rng η ∩ locs(Rep↓) ⊆ d om(Rh j )
for some confining partition and j with η self ∈ d om(Oh j )
(3) C ≤ Rep ⇒ rng η ∩ locs(Own↓, Rep↓) ⊆ d om(Oh j ∗ Rh j )
for some confining partition and j with η self ∈ d om(Rh j )
A global state (h, η) is confined, written conf C (h, η), iff h is confined and η is
confined in h for C.
Apropos the examples in Sect. 2.1, take Rep to be Bool and suppose the sequence
z := new OBool; w := z.bad() occurs in a method of some client class. Executed
in a confined initial state, the state after assignment of a new OBool to z is still
confined. The assignment to w then yields a state where the heap is confined but
the client’s store is not.
6.2 Confinement of commands and methods
A confined command is one that preserves confinement of global states. Because
command meanings depend on the method environment and expression meanings,
confinement for those is formalized first. We need to ensure that a method call
yields a heap confined for the caller. This is achieved using the condition h ✂ h0
in the following.
Definition 6.5 (confined method environment) Method environment µ is confined, written conf µ, if and only if the following holds for all C and m with
mtype(m, C) defined. Let mtype(m, C) = T →T and pars(m, C) = x. For all
(h, η) ∈ [[Heap ⊗ x : T , self : C]], if conf C (h, η) and µCm(h, η) 6= ⊥ then
(1) C  Rep ⇒ conf C (h0 , η) ∧ h ✂ h0 ∧ d 6∈ locs(Rep↓)
(2) C ≤ Rep ⇒ conf C (h0 , η) ∧ h ✂ h0
∧ (d ∈ locs(Own↓, Rep↓) ⇒ d ∈ d om(Oh j ∗ Rh j ))
for some confining partition h0 = Ch ∗ Oh 1 ∗ Rh 1 . . .
and j with η self ∈ d om(Rh j )
where (h0 , d) = µCm(h, η).
Condition (1) fails for method bad of the example in Sect. 2.1, regardless of whether
the return type of bad is taken to be Object or Bool.
The conditions for confinement of expressions are like those for confined stores
—after all, a store provides the meaning for the expression x. The conditions are
somewhat different for confined method environments, because methods are public
and can be called both by clients and from within an owner island. (In Sect. 9,
Def. 6.5 is refined to allow module-scoped owner methods to return reps.) Also,
confinement of commands does not explicitly require heap extension h ✂ h0 like
Def. 6.5 does, because it is a consequence of the other conditions (see Lemma 6.16).
Definition 6.6 (confined expression) Let C = Γ self. Expression Γ ⊢ e : T is
confined iff for any (h, η), if conf C (h, η) and [[Γ ⊢ e : T ]](h, η) 6= ⊥ then the following
hold, where d = [[Γ ⊢ e : T ]](h, η).
(1) C  Rep ∧ C  Own ⇒ d 6∈ locs(Rep↓)
(2) C ≤ Own ⇒ (d ∈ locs(Rep↓) ⇒ d ∈ d om(Rh j ))
for some confining partition and j with η self ∈ d om(Oh j )
ACM Journal Name, Vol. V, No. N, Month 20YY.

36

·

A. Banerjee and D. Naumann

(3) C ≤ Rep ⇒ (d ∈ locs(Own↓, Rep↓) ⇒ d ∈ d om(Oh j ∗ Rh j ))
for some confining partition and j with η self ∈ d om(Rh j )
Definition 6.7 (confined command) Let C = Γ self. Command Γ ⊢ S is confined iff
— conf µ ∧ conf C (h, η) ∧ [[Γ ⊢ S]]µ(h, η) 6= ⊥ ⇒ conf C (h0 , η0 ), for any µ and any
(h, η), where (h0 , η0 ) = [[Γ ⊢ S]]µ(h, η)
—if S is a method call then it has confined arguments (see below).
Confinement of arguments means that the store η1 passed in the semantics of
method call is confined for the callee.
Definition 6.8 (confined arguments) Let C = Γ self. A call Γ ⊢ x := e.m(e)
has confined arguments provided the following holds. Suppose U is the static type
of e and D the static type of e. For any (h, η) with conf C (h, η), let
d = [[Γ ⊢ e : U ]](h, η)

ℓ = [[Γ ⊢ e : D]](h, η)

η1 = [x 7→ d, self 7→ ℓ] .

If ℓ 6= ⊥, ℓ 6= nil , and d 6= ⊥ then conf (loctype ℓ) (h, η1 ).
A super-call Γ ⊢ x := super.m(e) has confined arguments provided the following
holds. Suppose U is the static type of e. For any (h, η) with conf C (h, η), let
d = [[Γ ⊢ e : U ]](h, η)

ℓ = η self

η1 = [x 7→ d, self 7→ ℓ] .

If d 6= ⊥ then conf (super C) (h, η1 ).
A purely semantic formulation would call class table CT confined just if [[CT ]]
is a confined method environment. But under simple restrictions, confinement of
[[CT ]] follows from confinement of method bodies and constructors. Thus we choose
the following.
Definition 6.9 (confined class table) Class table CT is confined iff for every
C and every m with mtype(m, C) = T →T the following hold.
(1) If m is declared in C by T m(T x){S} then S and all its constituents are
confined.
(2) If the constructor declaration in C is con{ S } then S and all its constituents
are confined.
(3) If C ≤ Own then T 6≤
> Rep.
(4) If m is inherited in Own from some B > Own then T 6≤
> Rep.
(5) No m is inherited in Rep from any B > Rep.
In Sect. 10 we add module-scoped methods on which condition (3) need not be
imposed. This condition ensures that owner methods do not return reps, which is
not ensured by confinement of the method body. Condition (5) is needed because
confinement of a method inherited from B > Rep depends on the arguments,
including self, being confined at B where reps are disallowed. Invocation of such
a method on an object of type Rep (or a subclass) would yield a store with self a
rep. A more refined restriction is to disallow inheritance into Rep only for methods
which leak self; see Sect. 12.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

37

Example 6.10 Condition (3) precludes the bad method of Sect. 2.1, for both return
types Object and Bool. Except for this, all examples in Sect. 2 yield confined class
tables (e.g., a well formed class table is obtained by combining Figs. 2 and 3).
One way to prove confinement for these examples is to check that they are safe
according to the static analysis of Sect. 11. For this one uses the desugarings of
Remark 4.1.
6.3 Properties of confinement
We need a number of results about confinement. The most important is that the semantics of a confined class table is a confined method environment (Theorem 6.17).
This depends on Lemma 6.16 which says that confined commands extend heap partitions, provided that method meanings have this property.
Lemma 6.11 If T is bool or unit, then every Γ ⊢ e : T is confined.
Proof. Direct from the definitions: confinement only pertains to locations.
Lemma 6.12 Suppose rng η ∩ locs(Rep↓) = ∅ and C ≤ B. Then for any h and
any η ∈ [[Γ, self : C]] we have conf C (h, η) iff conf B (h, η).
Proof. Straightforward. See Appendix.
Lemma 6.13 If conf C (h, η) and h ✂ h0 then conf C (h0 , η).
Proof. Straightforward. See Appendix.
Although confining partitions are not unique, a given confining partition of an
initial state can be extended to one on the final state for any command. This
is Lemma 6.16 below, which depends on the analogous property for constructors,
Lemma 6.15. From the proof of the latter, we factor out the induction step as
a somewhat complicated separate result, Lemma 6.14, because it is also used in
Sect. 11 to show soundness of the static analysis. Skip on first reading!
Lemma 6.14 Let µ be a method environment. Suppose we have the following:
(1) self : C ⊢ S is a confined command.
(2) for any B with an occurrence of new B in S we have B ⊏ C and moreover no
method calls occur in S.
(3) for any B with an occurrence of new B in S, and also for B = super C unless
super C = Object, the following holds for any (h, η) with conf B (h, η):
[[self : B ⊢ S0 : con]]µ(h, η) 6= ⊥ ⇒ h ✂ h1 ,
where S0 = constr B and h1 = [[self : B ⊢ S0 : con]]µ(h, η).
Then for any (h, η) with conf C (h, η), if [[self : C ⊢ S : con]]µ(h, η) 6= ⊥ then h ✂ h0
where h0 = [[self : C ⊢ S : con]]µ(h, η).
Proof. Assume (1–3) hold. To show the conclusion for the non-⊥ case, consider any (h, η) with conf C (h, η) and let h1 be as in the semantics of S as a
constructor. If super C = Object then h1 = h and thus h ✂ h1 . Otherwise,
h1 = [[self : super C ⊢ constr(super C) : con]]µ(h, η) and h ✂ h1 holds by hypothesis
(3). Now by semantics, h0 = [[self : C ⊢ S]]µ(h1 , η).
ACM Journal Name, Vol. V, No. N, Month 20YY.

38

·

A. Banerjee and D. Naumann

To show that h ✂ h0 , we can argue by induction on the structure of S. Note
that S has no method calls, by hypothesis (2), so µ is not relevant. Moreover, for
any object construction the result holds by hypothesis (3). We omit the rest of
the argument, which uses hypothesis (1): it is exactly the same as in the proof
of Lemma 6.16 below, except for appealing to hypothesis (2) for the case of new,
where that proof appeals to Lemma 6.15.
Lemma 6.15 (extension by constructors) Suppose self : C ⊢ constr C is confined, for all C. Then for any (h, η) with conf C (h, η) we have
[[self : C ⊢ S : con]]µ(h, η) 6= ⊥ ⇒ h ✂ h0

where h0 = [[self : C ⊢ S : con]]µ(h, η) .

Proof. This is exactly the conclusion of Lemma 6.14. We prove it by well
founded induction on C, using ≪ which is well founded by Lemma 4.9(1). For
any C and S, it suffices to show that the hypotheses (1–3) of Lemma 6.14 hold
for classes smaller than C with respect to ≪. First, (1) holds by hypothesis of the
present Lemma. By well formedness of the class table, there are no method calls
in constr C, and moreover if new B occurs in S then B ⊏ C; this is hypothesis (2).
Now from Lemma 4.9 and well formedness of the class table we have that B ≪ C
for every new B that occurs in S and also super C ≪ C. Thus by the induction
hypothesis we have (3).
Lemma 6.16 (extension by commands) Suppose Γ ⊢ S is confined and all its
constituents are confined. Suppose moreover that self : B ⊢ constr B is confined, for
all B. Let C = Γ self. For any µ, h, η with conf µ and conf C (h, η)
[[Γ ⊢ S]]µ(h, η) 6= ⊥ ⇒ h ✂ h0

where (h0 , −) = [[Γ ⊢ S]]µ(h, η) .

Proof. By structural induction on S. Let C = Γ self. We assume a confining
partition h = Ch ∗ Oh 1 ∗ Rh 1 ∗ . . . ∗ Oh k ∗ Rh k is given (k may be 0, i.e., there
need not be any islands). We show how to construct confining partition h0 =
Ch 0 ∗ Oh 01 ∗ Rh 01 ∗ . . . that extends the given one.
Case Γ ⊢ e1 .f := e2 . From [[Γ ⊢ e1 .f := e2 ]]µηh 6= ⊥ and Lemma 5.7(3) we have
that ℓ ∈ d om h where ℓ = [[Γ ⊢ e1 : C]](h, η). By semantics, h0 = [h | ℓ 7→ [hℓ | f 7→
d]]. We partition h0 using the given partition for h. That is, the domain for each
block of the updated heap h0 is the same as the corresponding block for h. Clearly
this extends the partition for h. To show that this partition is confining for h0 , it
suffices to show that the update of hℓf to d satisfies the confinement property for
ℓ. We argue by cases on loctype ℓ
—loctype ℓ  Own ∧ loctype ℓ  Rep. Then Def. 6.2(1) applies; it requires d 6∈
locs(Rep↓). By typing, loctype ℓ ≤ C, so C  Own ∧ C  Rep. Thus by confinement of e1 (a constituent of e1 .f := e2 and therefore confined by hypothesis), we
have by Def. 6.6(1) that d 6∈ locs(Rep↓).
—loctype ℓ ≤ Own. Def. 6.2(2) and (3) apply here. Letting j be the index of the
island with {ℓ} = d om(Oh 0j ) = d om(Oh j ), we must show both Oh 0j 6❀ Rh 0i (for
i 6= j) and Oh 0j 6❀g Rh 0j . By typing, loctype ℓ ≤ C, so C ≤ Own or Own ≤ C by
the tree property of ≤. We argue by cases on C.
—Own < C. By Own 6≤
> Rep, we have C  Rep so confinement of e2 at C yields
d 6∈ locs(Rep↓). Thus Oh 0j 6❀ Rh 0i and Oh 0j 6❀g Rh 0j .
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

39

—C ≤ Own. By confinement of e2 , if d ∈ locs(Rep↓) then d ∈ d om(Rh 0j )
so Oh 0j 6❀ Rh 0i for i 6= j. If C = Own then, by the typing rule for field
update, f is in the private fields g of Own, so the update cannot violate
Oh 0j 6❀g Rh 0j . If C < Own then d 6∈ locs(Rep↓) because if d is a rep then there
would be no confining partition, contradicting confinement of h0 which holds
by confinement of S.
—loctype ℓ ≤ Rep. Def. 6.2(4) applies in this case: we need to show Rh 0j 6❀
Oh 0i ∗ Rh 0i where i 6= j and j is the island for ℓ in the partition of h. By typing,
loctype ℓ ≤ C, hence C ≤ Rep or Rep < C. But if Rep < C then C 6≤
> Own and
the confinement condition for e1 (Def. 6.6(1)) at C contradicts loctype ℓ ≤ Rep,
so we have C ≤ Rep. Now confinement of e2 yields d ∈ locs(Own↓, Rep↓) ⇒ d ∈
d om(Oh j ∗ Rh j ). This proves Rh 0j 6❀ Oh 0i ∗ Rh 0i , because d om(Oh j ∗ Rh j ) =
d om(Oh 0j ∗ Rh 0j ).
Case Γ ⊢ x := new B. In the semantic definition, h1 = [h | ℓ 7→ [fields B 7→
defaults]] where ℓ = fresh(B, h). Define Bh = [ℓ 7→ [fields B 7→ defaults]] so
h1 = h ∗ Bh. Let η1 = [self 7→ ℓ]. Next, we argue that h ✂ h1 and conf B (h1 , η1 ).
Because h is closed, ℓ is not in the range of any object state in h. To construct an
extending partition it suffices to deal with the new object, as its addition cannot
violate confinement of existing objects. (This would not be the case if dangling
pointers were allowed, unless further restrictions are imposed on fresh.) We define
the extension and argue by cases on B.
—B  Own ∧ B  Rep. For a confining partition of h1 we extend that for h
by defining Ch 0 = Ch ∗ Bh and using the given partition of owner islands.
Because defaults contains no locations, this is a confining partition and we have
conf B (h1 , η1 ).
—B ≤ Own. We extend the partition by adding an island Oh 0k+1 ∗ Rh 0k+1 with
Oh 0k+1 = Bh and Rh 0k+1 = ∅. This is a confining partition because defaults has
no locations and we have conf B (h1 , η1 ) because rng η1 has no reps.
—B ≤ Rep. We can obtain a confining extension by adding Bh to any of the
Rh i , as defaults has no locations. As rng η1 = {ℓ}, we have conf B (h1 , η1 ) by
definition.15
This concludes the argument for h ✂ h1 and conf B (h1 , η1 ). These let us apply
Lemma 6.15 for constrB to get h1 ✂ h0 where h0 = [[self : B ⊢ constr B : con]]µ(h1 , η1 ).
Then h ✂ h0 by transitivity of ✂.
Case Γ ⊢ x := e.m(e). As e.m(e) is confined, its argument values are confined.
Thus we can obtain the result directly from confinement of µ, which explicitly
stipulates h ✂ h0 , and semantics of e.m(e).
The remaining cases are straightforward. See Appendix.
15 In this case we have C ≤ Own or C ≤ Rep, as otherwise the command would not be confined.
To show conf C (h1 , η) in this case, we would have to we put ℓ in Rh j , choosing j such that η self
is in the jth island. But we are only showing the extension of the partition for this lemma. For
soundness of the static analysis, we do have to show conf C (h1 , η).

ACM Journal Name, Vol. V, No. N, Month 20YY.

40

·

A. Banerjee and D. Naumann

Theorem 6.17 Suppose that CT is confined. Then the semantics [[CT ]] is confined, as is each µj in the approximation chain used to define it.
The proof uses fixpoint induction, which is only sound for inclusive predicates,
i.e., those closed under limits of ascending chains. For confinement of method
environments the definition is given pointwise, ultimately unfolding to the property
that the semantics of each method body preserves confinement. This definition, as
well as the one for the simulation R later, is in the usual form of logical relations.
By the structure of the definition, and continuity of the semantics, the property is
an inclusive predicate.16
Proof. Confinement of [[CT ]] follows by fixpoint induction from confinement
of µi for all i, which we show by induction on i. The base case holds because
µ0 Cm = λ(h, η) • ⊥, for any C, m, and this is confined by definition.
For the induction step, suppose conf µi , to show conf µi+1 . Consider an arbitrary
m. We argue for all C with mtype(m, C) defined, by induction on method depth
(Def. 4.7) of C for m. The base case is C such that depth(m, C) = 0. In this case,
CT (C) has a declaration
T m(T x){S} .
Suppose conf C (h, η) and µi+1 Cm(h, η) 6= ⊥. Let (h0 , d) = µi+1 Cm(h, η), which
by definition of µi+1 is obtained as
η1 = [η | result 7→ default ]
(h0 , η0 ) = [[x : T , self : C, result : T ⊢ S]]µi (h, η1 )
d = η0 result
Default values do not violate confinement so conf C (h, η1 ). As CT is confined,
S and its constituents are confined. By Lemma 6.16 we have h ✂ h0 , so by
Lemma 6.13 we have conf C (h0 , η). To show the confinement condition for µi+1 Cm
it remains to deal with the result value d. We have conf C (h0 , η0 ) by confinement
of S. We argue by cases on C.
—C  Own ∧ C  Rep. We need d 6∈ locs(Rep↓), for Def. 6.5(1), and this follows
from conf C (h0 , η0 ) by Def. 6.4(1).
—C ≤ Own. We need d 6∈ locs(Rep↓), and since by typing we have d ∈ [[T⊥ ]],
Def. 6.9(3) ensures T 6≤
> Rep and hence d 6∈ locs(Reps↓). (Note that semantic
confinement of η0 at C ≤ Own allows reps, so it is not enough for this case).
—C ≤ Rep. Then we need d ∈ locs(Own↓, Rep↓) to imply that d is in the domain
of Oh j ∗ Rh j for some partition and island j such that η self ∈ d om(Oh j ∗ Rh j ).
This follows from conf C (h0 , η0 ) by Def. 6.4(3).
This concludes the base case of the induction on depth.
For the induction step, i.e., depth(m, C) > 0, m may be inherited or declared in
C. If it is declared in C the argument is the same as for the case depth(m, C) = 0
above. Suppose m is inherited in C from B. Now µi+1 Cm = restr ((µi+1 Bm), C)
by definition of µi+1 . By induction on depth µi+1 Bm satisfies the confinement
16 See

Ploto’s notes.

ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

41

condition for m, B. To show the condition for µi+1 Cm, suppose conf C (h, η). We
claim that conf B (h, η). Using the claim, we argue as follows. If µi+1 Bm(h, η) 6= ⊥,
let (h0 , d) = µi+1 Bm(h, η). By induction on depth we have conf B (h0 , η) and h ✂
h0 . By Lemma 6.13 we obtain conf C (h0 , η). It remains to show the confinement
condition for d and to prove the claim. We argue by cases on C.
In the following non-rep cases, the claim holds by Lemma 6.12. To apply the
Lemma, we just need to show that rng η ∩ locs(Rep↓) = ∅.
—C  Own∧C  Rep. In this case, we have rng η∩locs(Rep↓) = ∅ by confinement
of η at C, Def. 6.4(1).
—C ≤ Own < B. Then Own inherits m from B > Own, so by confinement of the
class table, Def. 6.9(4), we have T 6≤
> Rep. Also, Own 6≤
> Rep, so by Lemma 5.4
we have no reps in rng η.
In the preceding cases, the condition imposed on d by Def. 6.5(1) for class C is
d 6∈ locs(Rep↓). But this same condition is imposed for class B, and it holds by
induction on depth. For the remaining cases we prove the claim conf B (h, η) as
follows.
—C < B ≤ Own. Both B and C impose the same condition (Def. 6.4(2)).
—C < B ≤ Rep. Both C and B impose the same conditions on η (Def. 6.4(3)).
In these two cases the requirement for d at C, Def. 6.5(2) or (1), is the same as for
B, so it holds by induction on depth.
The case C ≤ Rep < B cannot occur in a confined class table. If m is inherited in
C ≤ Rep from B then it is inherited in Rep from B, and this is explicitly disallowed
in Def. 6.9(5).
7. FIRST ABSTRACTION THEOREM
This section formulates and proves the central result of the paper. First, we make
precise the idea of comparing two class tables that differ only in their implementation of class Own. Then we define basic coupling: a relation between single
instances of class Own for the two implementations. This induces the coupling
relations for other data types, for heaps containing multiple instances of Own, and
for method meanings. Related method meanings have the simulation property:
if initial states are coupled, then so are outcomes. The main theorem says that if
methods of Own have the simulation property, then so do all methods of all classes.
7.1 Comparing class tables
We compare two implementations of a designated class Own. They can have
completely different declarations, so long as methods of the same signatures are
present —declared or inherited— in both. They can use different reps, distinguished by class name Rep for one implementation and Rep′ for the other. We
allow Rep = Rep′ . For simplicity, we assume that both Rep and Rep′ are in each
of the two compared class tables.17
17 An

alternative formulation would consider different declarations of Own together with associated
class tables in which Rep or Rep′ but not both are declared. But these could be combined into
class tables fitting our formulation.
ACM Journal Name, Vol. V, No. N, Month 20YY.

42

·

A. Banerjee and D. Naumann

Definition 7.1 (comparable class tables, non-rep classes) Suppose class names
Own, Rep, Rep′ are given, such that Own 6≤
> Rep and Own 6≤
> Rep′ . We say C is a
non-rep class iff C  Rep and C  Rep′ . Well formed class tables CT and CT ′ are
comparable provided the following hold.
(1) CT and CT ′ are identical except for their values on Own. (In particular,
CT (Rep) = CT ′ (Rep) and CT (Rep′ ) = CT ′ (Rep′ ).)
We write ⊢, ⊢′ for the typing relations determined by CT, CT ′ respectively,
and similarly for the auxiliary functions, such as mtype, mtype′ . We also write
[[−]], [[−]]′ for the respective semantics and assume that the same allocator, fresh,
is used for both [[−]] and [[−]]′ .
(2) super Own = super′ Own.
(3) For any m, either mtype(m, Own) and mtype′ (m, Own) are both undefined or
both are defined and equal.
Example 7.2 Let CT be given by Figs. 2 and 3. Let CT ′ be given by Figs. 4 and
3 together with Observer from Fig. 2. These are comparable.
Instead of condition (3), one could require that CT (Own) and CT ′ (Own) declare the same methods. But that would disallow some situations that occur in
practice. Suppose class C extends B by adding a method m implemented using
calls to methods inherited from B. This might be the easiest way to achieve desired functionality for m, but there could be an alternative data structure that is
more efficient for m and for the methods of B. An alternative implementation of
C could add that data structure and override the methods of B to use it. One can
argue that the program is poorly designed, e.g., because space for attributes of B is
wasted in C objects. Better designs are possible in languages with interface types
separate from classes. Nonetheless, such examples do arise in practice. Allowing
them complicates the proof of Theorem 7.20 but none of the other results. The
main consequence we need from condition (3) is the following.
Lemma 7.3 If mtype(m, C) is defined then depth(m, C) = depth′ (m, C).
Proof. Straightforward. See Appendix.
One can imagine a theory in which an owner subclass C < Own has different
declarations in CT and CT ′ . But we are concerned with an abstraction provided
by a single class rather than by a collection of classes, so CT (C) = CT ′ (C) here.
In Sect. 7.3 we impose a restriction on owner subclasses that is needed for the first
abstraction theorem. The issue is explored in Sect. 8 and the restriction lifted in
Sect. 10.
7.2 Coupling relations and simulation
The definitions are organized as follows. A basic coupling R is a suitable relation
on islands. This induces a family of coupling relations, R θ for each θ. Then comes
the definition of simulation, a coupling that is preserved by all methods of Own
and established by the constructor.
Definition 7.4 (basic coupling) Given comparable class tables, a basic coupling
is a binary relation R on heaps —not necessarily closed— such that the following
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

43

holds: For any h, h′ , if R h h′ then there is a location ℓ with loctype ℓ ≤ Own and
partitions h = Oh ∗ Rh and h′ = Oh ′ ∗ Rh ′ such that
(1) d om Oh = {ℓ} = d om Oh ′
(2) d om(Rh) ⊆ locs(Rep↓) and d om(Rh ′ ) ⊆ locs(Rep′ ↓)
(3) hℓf = h′ ℓf for all (f : T ) ∈ d om(fields(loctype ℓ)) with f 6∈ g and f 6∈ g ′ , where
g = d om(dfields(Own)) and g ′ = d om(dfields′ (Own))
Example 7.7 below shows why we allow R to act on heaps that are not closed.
Although R is unconstrained for the private fields and reps, condition (3) determines it for fields of subclasses of Own. Once we have defined the induced relation
R, item (3) will be equivalent to the condition R (type(f, loctype ℓ)) (hℓf ) (h′ ℓf ).
Because CT and CT ′ are well formed, the declared field names g and g ′ do not
occur as fields of subclasses or superclasses of Own. In (3), f ranges over fields of
both subclasses and superclasses; except for g and g ′ , we have fields C = fields′ C
for all C. The typing relations ⊢ and ⊢′ are also the same except for class Own.
Example 7.5 Sect. 2.2 discusses this coupling relation:
(o.g = nil = o′ .g) ∨ (o.g 6= nil 6= o′ .g ∧ o.g.f = ¬(o′ .g.f)) .
For this example we take both Rep and Rep′ to be Bool, and Own to be OBool.
The displayed formula can be interpreted as relation R which relates h to h′ just if
either h = [ℓ1 7→ [g 7→ nil ]] and h′ = [ℓ1 7→ [g 7→ nil ]] or else
h = [ℓ1 7→ [g 7→ ℓ2 ], ℓ2 7→ [f 7→ d]] and h′ = [ℓ1 7→ [g 7→ ℓ3 ], ℓ3 7→ [f 7→ ¬d]]
for some boolean d and locations ℓ1 in locs OBool and ℓ2 , ℓ3 in locs Bool. We assume
that the class table contains only Bool, OBool, and some client classes. If OBool
had subclasses, the relation on their fields would be determined by condition (3)
above.
Example 7.6 Sect. 3.1 uses the formula o.g = o′ .g ∧ o.g mod 2 = 0. This can be
interpreted as the basic coupling R that relates h to h′ just if there is some ℓ with
loctype ℓ ≤ A, h and h′ have domain {ℓ}, and h ℓ g = h′ ℓ g = 2 × m for some integer
m ≥ 0.
Example 7.7 The Observer examples show why we allow R to relate non-closed
heaps. Consider the version in Fig. 2. Here Rep is Node, Own is Observable, and
there is a client class Observer. Fig. 5 illustrates two instances of this simple data
structure. Fig. 4 gives code for an alternative version which uses an extra node as
sentinel for the list. The sentinel does not point to an Observer. Fig. 7 depicts a
corresponding pair of heaps for the two alternatives, using arrows without destination objects to indicate dangling pointers. Upon initialization of an Observable,
there are no installed Observers, so for the version of Fig. 2 we should have fst = nil .
But in the alternative version, this should correspond to snt holding the location of
a Node with ob = nil . This is established by the constructor in Fig. 4. An attempt
at formalizing the correspondence is as follows:
(o.fst = nil = o′ .snt.nxt) ∨ (o.fst 6= nil 6= o′ .snt.nxt ∧ α(o.fst) = α′ (o′ .snt.nxt)
where α, α′ are functions that yield the list of locations in the ob fields of successive
nodes. But how should this formula be interpreted if, say, o’.snt = nil or there is
ACM Journal Name, Vol. V, No. N, Month 20YY.

44

·

PSfrag replacements
A. Banerjee
and D. Naumann
ℓ

ℓ

Observable
Fig. 7. Basic coupling example. Labels indicate locations as described in
Example 7.7. Note dangling pointers
ℓ2 and ℓ4 and sentinel node ℓ′0 .

Observable
ℓ1
Node
ℓ3
Node

ℓ2

ℓ′0
Node2
ℓ′1
Node2
ℓ′3

ℓ4

Node2

sharing such as a chain with cyclic tail? Separation logic [Reynolds 2001] offers a
precise way to formulate such definitions but its development is at an early stage.
We simply sketch the coupling in terms of semantics: R h h′ iff either h and h′ have
the form
h = [ ℓ 7→ [fst 7→ nil ]]
h′ = [ ℓ 7→ [snt 7→ ℓ′0 ], ℓ′0 7→ [ob 7→ nil , nxt 7→ nil ]]
or they have the form
h = [ ℓ 7→ [fst 7→ ℓ1 ], ℓ1 7→ [ob 7→ ℓ2 , nxt 7→ ℓ3 ], ℓ3 7→ [ob 7→ ℓ4 , nxt 7→ . . .], . . .]
h′ = [ ℓ 7→ [snt 7→ ℓ′0 ], ℓ′0 7→ [ob 7→ nil , nxt 7→ ℓ′1 ],
ℓ′1 7→ [ob 7→ ℓ2 , nxt 7→ ℓ′3 ], ℓ′3 7→ [ob 7→ ℓ4 , nxt 7→ . . .], . . .]
for some locations ℓ in locs(Observable), ℓ1 , ℓ3 , . . . in locs(Node), ℓ′0 , ℓ′1 , ℓ′3 , . . . in
locs(Node2), and ℓ2 , ℓ4 , . . . in locs(Observer↓).
Note that the owners are at the same location, ℓ, as are the referenced client
objects at ℓ2 , ℓ4 , . . .. No correspondence is required between locations ℓ1 , ℓ3 , . . . and
ℓ′0 , ℓ′1 , ℓ′3 , . . . of reps.
A basic coupling induces a relation R Heap on arbitrary heaps by requiring that
they have confining partitions such that islands can be put in correspondence so that
pairs are related by R. The formal definition uses the induced relation R (state C)
for object states of non-rep classes C  Own, and this in turn is defined in terms
of R C for non-rep classes C  Own. For uniformity, we give the definition of
R for all θ, but forcing the case for θ = state Own to be false, as the compared
states have different fields. Aside from the ramifications of heap confinement, the
definition is induced in the standard way for logical relations.
Definition 7.8 (coupling relation, R θ) In the context of a basic coupling with
given relation R, we define for each θ a relation R θ ⊆ [[θ]] × [[θ]]′ as follows.
For heaps h, h′ , we define R Heap h h′ iff there are confining partitions of h, h′ ,
with the same number n of owner islands, such that
—R (Oh i ∗ Rh i ) (Oh ′i ∗ Rh ′i ) for all i in 1..n
—d om(Ch) = d om(Ch ′ )
—R (state (loctype ℓ)) (hℓ) (h′ ℓ) for all ℓ ∈ d om(Ch)
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

45

For other categories θ we define R θ as follows.
R bool d d′
⇔ d = d′
R unit d d′
⇔ d = d′
′
RC dd
⇔ d = d′
R Γ η η′
⇔ ∀x ∈ d om Γ • R (Γx) (ηx) (η ′ x)
′
R (state C) s s
⇔
C  Own ∧ ∀f ∈ d om(fields C) • R (type(f, C)) (s f ) (s′ f )
R (θ⊥ ) α α′
⇔ (α = ⊥ = α′ ) ∨ (α 6= ⊥ 6= α′ ∧ R θ α α′ )
R (Heap ⊗ Γ) (h, η) (h′ , η ′ ) ⇔ R Heap h h′ ∧ R Γ η η ′
R (Heap ⊗ T ) (h, d) (h′ , d′ ) ⇔ R Heap h h′ ∧ R T d d′
⇔ ∀(h, η) ∈ [[Heap ⊗ Γ]], (h′ , η ′ ) ∈ [[Heap ⊗ Γ]]′ •
R (C, x, T →T ) d d′
R (Heap ⊗ Γ) (h, η) (h′ , η ′ ) ∧ conf C (h, η) ∧ conf C (h′ , η ′ )
⇒ R (Heap ⊗ T )⊥ (d(h, η)) (d′ (h′ , η ′ ))
where Γ = [x 7→ T , self 7→ C]
R MEnv µ µ′
⇔ ∀C, m • (C is non-rep) ∧ (mtype(m, C) is defined)
⇒ R (C, pars(m, C), mtype(m, C)) (µ C m) (µ′ C m)
The gist of the abstraction theorem is that if methods of Own are related by R
then all methods are. We can now express this conclusion as R MEnv [[CT ]] [[CT ′ ]]′ .
To express the antecedent, note that the relation applicable to a method m of Own
is R (Own, x, T →T ) where mtype(m, Own) = T →T and pars(m, Own) = x. The
definition of R (C, x, T →T ) quantifies over confined initial states but does not
require confinement of outcomes.18 The antecedent will also take into account that
methods may be declared or inherited.
Although the definition is technically intricate, the core idea is the extension of a
basic coupling, for a single owner instance, to a heap containing potentially many
owners. This idea is given straightforward expression using heap partitions. By
contrast, sharing of representations between owners would require a more complicated form of extension (see Sect. 12).
We aim to define per-instance simulations, and in particular the establishment of
such a relation by a constructor of class Own on a single island. But to formulate
this semantically we describe the constructor’s action on a heap in which other
islands may be present. The reason is that there is not an easy way to connect a
constructor’s action on a small heap with its action on a larger one (see Footnote 14).
Definition 7.9 (simulation) A simulation is a coupling R such that the following
hold.
(1) (constructors of Own establish R) For any ℓ ∈ locs(Own↓), any h, h′ with
18 One

might think that R Heap could be defined in terms of admissible partitions without the
assumption of confinement. But because partitions are not unique this leads to difficulties: a heap
could be confined with respect to one partition but related with respect to another.
ACM Journal Name, Vol. V, No. N, Month 20YY.

46

·

A. Banerjee and D. Naumann

R Heap h h′ , and any µ, µ′ , let
h1
h′1
h0
h′0

= [h | ℓ 7→ [fields(loctype ℓ) 7→ defaults]]
= [h′ | ℓ′ 7→ [fields(loctype ℓ′ ) 7→ defaults ′ ]]
= [[self : (loctype ℓ) ⊢ constr(loctype ℓ) : con]]µ(h1 , [self 7→ ℓ])
= [[self : (loctype ℓ) ⊢′ constr(loctype ℓ) : con]]µ′ (h′1 , [self 7→ ℓ])

Then R h0 h′0 .
(2) (methods of Own preserve R) Let µ ∈ N → [[MEnv ]] (resp. µ′ ∈ N → [[MEnv ]]′ )
be the approximation chain in the definition of [[CT ]] (resp. [[CT ′ ]]′ ). For every
m with mtype(m, Own) defined, the following implications hold for every i,
where x = pars(m, Own) and T →T = mtype(m, Own).
(a) R MEnv µi µ′i ⇒ R (Own, x, T →T ) ([[M ]]µi ) ([[M ′ ]]′ µ′i )
if m has declaration M in CT (Own) and M ′ in CT ′ (Own)
(b) R MEnv µi µ′i ⇒ R (Own, x, T →T ) ([[M ]]µi ) (restr ([[MB ]]′ µ′i , Own))
if m has declaration M in CT (Own) and is inherited from B in CT ′ (Own),
with MB the declaration of m in B
(c) R MEnv µi µ′i ⇒ R (Own, x, T →T ) (restr([[MB ]]µi , Own)) ([[M ′ ]]′ µ′i )
if m has declaration M ′ in CT ′ (Own) and is inherited from B in CT (Own),
with MB the declaration of m in B
In the case where constructors in Own and its subclasses are skip, condition (1)
simply says that the default values are related. Note that it also precludes aborting constructors, as R applies to heaps but not to ⊥; this is convenient but not
necessary.
The following properties are straightforward consequences of the definition.
Lemma 7.10 For all h, h′ and all locations ℓ 6∈ locs(Rep↓, Rep′ ↓), if R Heap h h′
then ℓ ∈ d om h ⇔ ℓ ∈ d om h′ .
Lemma 7.11 [[T ]] = [[T ]]′ for all T , and [[Γ]] = [[Γ]]′ for all Γ.
Lemma 7.12 For any data type T , R T is the identity relation on [[T ]] and R T⊥
is the identity relation on [[T⊥ ]].
Lemma 7.13 If U ≤ T and R U d d′ then R T d d′ .
7.3 Restricting reps in owner subclasses
The preceding properties express a strong connection between locations for related
heaps. To ensure that this connection is preserved by object construction, we shall
assume the allocator is parametric. But it is not reasonable to require that related
heaps have the same rep locations, so parametricity cannot be exploited for reps.
As a result, the present form of simulation is not adequate for construction of reps in
subclasses of Own, although such construction is allowed by confinement. The first
abstraction theorem depends on an assumption expressed in the following terms.
Definition 7.14 (new rep in sub-owner) We say CT has a new rep in a subowner if, for some B ≤ Rep or B ≤ Rep′ , an object construction new B occurs in
some method declaration in a class C < Own.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

47

If CT has no new reps in sub-owners then neither does a comparable CT ′ . The
examples in Sects. 2 and 3 have no new reps in sub-owners; examples which do are
given in Sect. 8.
In the rest of Sect. 7 we make the following assumption. It is used in the proof
of Lemma 7.23 on which the first abstraction theorem depends. For the second
abstraction theorem the second sentence will be dropped.
Assumption 7.15 First, CT and CT ′ are confined class tables for which a simulation R is given. Second, CT has no new reps in sub-owners and the allocator is
parametric in the sense of Def. 5.1.
7.4 Identity extension
A typical formulation of identity extension is that R T is the identity on any type
T for which it is the identity on all primitive types b that occur in T . The reason is
that no value of type b can occur in a value of type T if b does not occur in T —but
this fails with extensible records and structural subtyping, and with procedures that
may have global variables [Naumann 2002]. It can be made to work using namebased (declaration) subclassing [Cavalcanti and Naumann 2002]: in the context of
a complete class table, one can consider the classes that have no attributes with
subclasses in which b occurs. For our purposes here it is enough to deal with the
heap.
In our language, R T is the identity for every data type T (Lemma 7.12), but
that is only because the interesting data is in the heap —which is not typed at
all.19 In general, [[state Own]] 6= [[state Own]]′ and R(state Own) is not the identity.
Related heaps can contain owner objects with different states that may point to
completely different rep objects. But consider executing a method on an object o
from whose fields no Own objects are reachable, i.e., Own objects are not part of
the representation of o. The resulting heap may contain Own objects that were
assigned to local variables, but if the method is confined then those objects are
unreachable in the final state.
Definition 7.16 (garbage collection, Own-free) For a set or list d of values,
define the heap gc(d, h) to be the restriction of h to cells reachable from d. For
(h, η) ∈ [[Heap ⊗ Γ]], define collect(h, η) = (gc(rng η, h), η). Extend collect to
[[(Heap ⊗ Γ)⊥ ]] by collect ⊥ = ⊥.
Say h is Own-free just if d om h ∩ locs(Own↓) = ∅ and η is Own-free just if
rng η ∩ locs(Own↓) = ∅.
Lemma 7.17 (identity extension) Suppose R (Heap ⊗ Γ) (h, η) (h′ , η ′ ) and
Γ self is non-rep. Let (h, η) and (h′ , η ′ ) be confined at Γ self. If collect(h, η) and
collect(h′ , η ′ ) are Own-free then collect(h, η) = collect(h′ , η ′ ).
Proof. In confined heaps, reps are only reachable from owners. Now the argument is a straightforward induction using the definition of R.

19 Nor

would we want to impose a typing system on the heap, as it would likely preclude unbounded
data structures [Grossman et al. 2000].
ACM Journal Name, Vol. V, No. N, Month 20YY.

48

·

A. Banerjee and D. Naumann

Lemma 7.18 For any R given by Def. 7.8 from a basic coupling, if h ∈ [[Heap]]
is Own-free then R Heap h h. If, in addition, (h, η) ∈ [[Heap ⊗ Γ]] and rng η is
Own-free then R (Heap ⊗ Γ) (h, η) (h, η).
Proof. If h is Own-free and confined then it has no reps; its admissible partition
is a single block, the clients. For such a heap it is immediate from the definition
of R that R Heap h h. If rng Γ is Own-free then R Γ η η is also direct from the
definition.
7.5 Abstraction theorem
The main theorem says that if methods of Own preserve the coupling relation then
so do all methods.20 The proof depends on lemmas for constructors and commands.
These are given following the theorem. The other main ingredient for the proof is
the following connection between R and the semantics of inherited methods.
Lemma 7.19 Suppose C and all class names in T are non-rep, and B < C. If
R (C, x, T →T ) d d′ then R (B, x, T →T ) (restr(d, B)) (restr(d′ , B)) where restr is
the restriction to global states of B (see Def. 5.5).
Proof. Straightforward, using Lemma 5.7(1). See Appendix.
Theorem 7.20 (abstraction) R MEnv [[CT ]] [[CT ′ ]]′ .
Proof. We show that the relation holds for each step in the approximation chain
in the semantics of class tables. That is, we show by induction on i that
R MEnv µi µ′i

for every i ∈ N .

The result R MEnv [[CT ]] [[CT ′ ]]′ then follows by fixpoint induction, as [[CT ]] and
[[CT ′ ]]′ are defined to be the fixpoints of these ascending chains. Admissibility of
fixpoint induction is discussed preceding the proof of Theorem 6.17.
For the base case, we have R (C, pars(m, C), mtype(m, C)) (µ0 C m) (µ′0 C m) for
every m, C because λ(h, η) • ⊥ relates to itself.
For the induction step, suppose
R MEnv µi µ′i .

(∗)

We must show R MEnv µi+1 µ′i+1 , that is, for every non-rep C and every m with
mtype(m, C) defined:
R (C, x, T →T ) (µi+1 C m) (µ′i+1 C m)

(†)

where x = pars(m, C) and T →T = mtype(m, C). For arbitrary m we show (†) for
all C with mtype(m, C) defined, using a secondary induction on depth(m, C). We
have depth′ (m, C) = depth(m, C) (Lemma 7.3).
The base case is the unique C with depth(m, C) = 0; here m is declared in both
CT (C) and CT ′ (C). We go by cases on C. If C = Own, we get (†) from the
20 Readers

familiar with Reynolds [1984] may expect that, as our language has fixpoints, the result
only holds for couplings that are ⊥-strict and join-complete. But our basic couplings have this
property, trivially, because heaps are ordered by equality. The induced coupling is strict and
join-complete by construction.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

49

assumption that R is a simulation. In detail: Using (∗) and Def. 7.9(2a) we get
R (Own, x, T →T ) ([[M ]]µi ) ([[M ′ ]]′ µ′i ) ,
whence (†) by definition of µi+1 and µ′i+1 . The other case is C a non-rep class
different from Own. Then by Def. 7.1(1) of comparable class tables we have
CT (C) = CT ′ (C) and in particular both class tables have the same declaration
T m(T x) {S} .
To show (†), suppose conf C (h, η), conf C (h′ , η ′ ), R Heap h h′ , and R Γ η η ′ ,
where Γ = x : T , self : C. Then by Lemma 7.23 below, using R MEnv µi µ′i , the
results from S are related. That is, either [[Γ ⊢ S]]µi (h, η) = ⊥ = [[Γ ⊢′ S]]′ µ′i (h′ , η ′ )
or neither is ⊥. In the latter case, (h0 , η0 ) is related to (h′0 , η0′ ) where (h0 , η0 ) =
[[Γ ⊢ S]]µi (h, η) and (h′0 , η0′ ) = [[Γ ⊢′ S]]′ µ′i (h′ , η ′ ). Then, by definition of R Γ,
R Γ η0 η0′ implies R T (η0 result) (η0′ result). Thus (†) holds by definition of µi+1
and µ′i+1 . This concludes the base case of the secondary induction.
For the induction step, suppose depth(m, C) > 0. By induction on depth we
have, by definition of depth,
R (C, x, T →T ) (µi+1 (super C) m) (µ′i+1 (super C) m) .

(‡)

′

If m is declared in both CT (C) and CT (C) then the argument is the same as in the
base case of the secondary induction. If m is inherited in both CT (C) and CT ′ (C)
then (‡) follows from (†) because the semantics defines µi+1 C m by restriction
from (µ′i+1 (super C) m) and restriction preserves simulation. (This is Lemma 7.19,
which is applicable because if B > Own and m is inherited in Own from B then
T 6≤
> Rep and T 6≤
> Rep′ by confinement of CT, CT ′ , Def. 6.9(4).) The remaining
possibility is that m is declared in CT (C) and inherited in CT ′ (C) from some B
(or the other way around). Then C = Own, by comparability of CT and CT ′ .
Using Def. 7.9(2b) and (∗) we get
R (Own, x, T →T ) ([[M ]]µi ) (restr([[MB ]]µ′i , Own))
and thus (†) by definition of µi+1 and µ′i+1 .
Lemma 7.21 (establishment by constructors) Let µ and µ′ be any method
environments. Then the following holds for any non-rep class C 6= Own.
For all (h, ℓ) ∈ [[Heap ⊗ C]] and (h′ , ℓ′ ) ∈ [[Heap ⊗ C]], if conf C (h, η1 ), conf C (h′ , η1′ )
and R (Heap ⊗ C) (h, ℓ) (h′ , ℓ′ ) then R Heap ⊥ h0 h′0 , where
η1 = [self 7→ ℓ]
η1′ = [self 7→ ℓ′ ]

h0 = [[self : C ⊢ constr C : con]]µ(h, η1 )
h′0 = [[self : C ⊢′ constr C : con]]µ′ (h′ , η1′ )

Proof. By well founded induction on C with respect to ≪. Suppose conf C (h, η),
conf C (h′ , η ′ ), and R (Heap ⊗ C) (h, ℓ) (h′ , ℓ′ ). Let h1 = [[self : C ⊢ S : con]]µ(h, η)
be as in the semantics of S as a constructor, and similarly for h′1 . If super C =
Object then h1 = h and thus R Heap h1 h′1 by hypothesis. Otherwise, h1 =
[[self : super C ⊢ constr(super C) : con]]µ(h, η) and we get R Heap h1 h′1 by the induction hypothesis noting that super C ≪ C by Lemma 4.9. It follows that
R (Heap ⊗ C) (h1 , ℓ) (h′1 , ℓ′ ).
It remains to show R Heap ⊥ h0 h′0 , where h0 , h′0 are obtained by applying the
command semantics of constr C to (h1 , ℓ) and (h′1 , ℓ). This holds because, taking S
ACM Journal Name, Vol. V, No. N, Month 20YY.

50

·

A. Banerjee and D. Naumann

to be constr C in the claim below, we get R (Heap ⊗ C)⊥ (h0 , η0 ) (h′0 , η0′ ) and thus
either both outcomes are ⊥ or R Heap h0 h′0 .
Claim: For all self : C ⊢ S such that S has no method calls and every new B
in S has B ⊏ C, for all (h, η) and (h′ , η ′ ), if conf C (h, η), conf C (h′ , η ′ ), and
R (Heap ⊗ Γ) (h, η) (h′ , η ′ ) then
R (Heap ⊗ Γ)⊥ ([[Γ ⊢ S]]µ(h, η)) ([[Γ ⊢′ S]]′ µ′ (h′ , η ′ )) .
Proof of the claim is by induction on the structure of S. Note that by hypothesis
S has no method calls, so µ is not relevant. The argument is exactly the same as
in the proof of Lemma 7.23 below, except for the case of new. In the proof of
Lemma 7.23, the case of new appeals to the present Lemma for constructors. To
prove the claim for this case, the argument is the same except for appealing to the
main induction hypothesis; this is sound because the claim includes the hypothesis
that if new B occurs in S then B ⊏ C and thus B ≪ C by Lemma 4.9.
Lemma 7.22 (preservation by expressions) For any non-rep class C 6= Own
and any constituent expression Γ ⊢ e : T of a method declared in C, the following holds: For all (h, η) ∈ [[Heap ⊗ Γ]] and (h′ , η ′ ) ∈ [[Heap ⊗ Γ]]′ , if R (Heap ⊗
Γ) (h, η) (h′ , η ′ ) then
R (T⊥ ) ([[Γ ⊢ e : T ]](h, η)) ([[Γ ⊢′ e : T ]]′ (h′ , η ′ )) .
Proof. By induction on the derivation of Γ ⊢ e : T . For each case of e, we give
an argument assuming that Γ, C, T, η, η ′ , h, h′ satisfy the hypotheses of the Lemma.
Case Γ ⊢ (B) e : B. Induction on e yields that R D⊥ ℓ ℓ′ (or else both denotations of e are ⊥). By confinement of e, as C 6= Own and C is non-rep, we have
ℓ 6∈ locs(Rep↓) and ℓ′ 6∈ locs(Rep′ ↓). Thus, ℓ′ = ℓ by Lemma 7.12. Hence either
both semantics yield ℓ, whence R B⊥ ℓ ℓ, or both yield ⊥ and again R B⊥ ⊥ ⊥.
Case Γ ⊢ e is B : bool. The argument is similar to that for type cast.
Case Γ ⊢ e.f : T . By induction on e we have R C⊥ ℓ ℓ′ , hence ℓ = ℓ′ by
Lemma 7.12. In the non-⊥ case, ℓ 6= nil . By closure of the heaps, ℓ ∈ d om h
and ℓ ∈ d om h′ . We consider cases on whether C < Own. Consider confining
partitions (Ch ∗ Oh 1 ∗ Rh 1 . . .) = h and (Ch ′ ∗ Oh ′1 ∗ Rh ′1 . . .) = h′ that have
corresponding islands as in the definition of R Heap. In the case C < Own, we
have ℓ ∈ locs(Own↓) and hence ℓ in some d om(Oh i ). From R Heap h h′ we have
R (Oh i ∗ hRepi ) (Oh ′i ∗ hRep′i )
and thus ℓ ∈ d om(Oh ′i ) by basic coupling Def. 7.4(1). Since C 6= Own, we know by
visibility that f is not in the private fields g of Own. Thus, as type(f, loctype ℓ)) =
T , we have R T (hℓf ) (h′ ℓf ) by Def. 7.4(3) and Lemma 7.12.
Finally, in the case C  Own (recall that C is non-rep and C 6= Own by hypothesis, we have ℓ ∈ d om(Ch) and hence ℓ ∈ d om(Ch ′ ) by definition R Heap.
Hence R (state (loctype ℓ)) (hℓ) (h′ ℓ) and thus R T (hℓf ) (h′ ℓf ) by definition of
R (state (loctype ℓ)).
The remaining cases are straightforward. See Appendix.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

51

Lemma 7.23 (preservation by commands) Suppose R is a simulation, and
moreover µ and µ′ are confined method environments such that R MEnv µ µ′ .
Then the following holds for any non-rep class C 6= Own. For any constituent
command Γ ⊢ S in a method declaration in CT (C) and any (h, η) and (h′ , η ′ ), if
conf C (h, η), conf C (h′ , η ′ ), and R (Heap ⊗ Γ) (h, η) (h′ , η ′ ) then
R (Heap ⊗ Γ)⊥ ([[Γ ⊢ S]]µ(h, η)) ([[Γ ⊢′ S]]′ µ′ (h′ , η ′ )) .
Proof. For any C, the proof is by structural induction on Γ ⊢ S.
Case Γ ⊢ x := e. As CT is confined, constituent e of the assignment is confined.
So by Lemma 7.22 we have R T⊥ d d′ . Hence, by R Γ η η ′ and definition of R Γ,
we have R Γ [η | x 7→ d] [η ′ | x 7→ d′ ] whence the result.
Case Γ ⊢ e1 .f := e2 . By Lemma 7.22 for e1 we have R C ℓ ℓ′ , hence ℓ = ℓ′
by Lemma 7.12. By Lemma 7.22 for e2 we have R U d d′ and hence R T d d′
by Lemma 7.13, where (f : T ) ∈ dfields C as in the typing rule. To conclude the
argument it suffices to show
R Heap [h | ℓ 7→ [hℓ | f 7→ d]] [h′ | ℓ 7→ [h′ ℓ | f 7→ d′ ]] .

(∗)

Consider confining partitions (Ch ∗ Oh 1 ∗ Rh 1 . . .) = h and (Ch ′ ∗ Oh ′1 ∗ Rh ′1 . . .) = h′
that correspond as in the definition of R Heap h h′ . We argue by cases on C.
—C < Own: Then loctype ℓ ≤ C < Own. From typing we have e1 : C and hence
there is some i with {ℓ} = d om(Oh i ) and by R Heap h h′ we get
R (Oh i ∗ Rh i ) (Oh ′i ∗ Rh ′i )
and so {ℓ} = d om(Oh ′i ). By typing and C 6= Own, field f is not in the private
fields g of Own. So (∗) follows from R Heap h h′ and R T d d′ .
—C  Own: As C is non-rep, we have ℓ ∈ d om Ch and thus ℓ ∈ d om Ch ′ by
hypothesis R Heap h h′ . Moreover, R (state (loctype ℓ)) (hℓ) (h′ ℓ) and so by
R T d d′ we get R (state (loctype ℓ)) [hℓ | f 7→ d] [h′ ℓ | f 7→ d′ ]. Hence (∗).
Case Γ ⊢ x := new B. By confinement of CT , this command is confined and
hence the final states are confined: conf C (h0 , η0 ) and conf C (h′0 , η0′ ). We have C 
Rep and C 6= Own. In the case C 6< Own confinement of η0 and η0′ implies rng η0 ∩
locs(Rep↓) = ∅ = rng η0′ ∩ locs(Rep′ ↓). So ℓ 6∈ locs(Rep↓) and ℓ′ 6∈ locs(Rep′ ↓),
hence by typing B is non-rep. In the case C < Own, we have B non-rep by
Assumption 7.15 (no reps in sub-owners). Either way, B is non-rep so Lemma 7.10
applies, to yield d om h ∩ locs B = d om h′ ∩ locs B. Thus by parametricity of f resh
we have ℓ = fresh(B, h) = fresh(B, h′ ) = ℓ′ . So, by Lemma 7.12 and R Γ η η ′ we
have R Γ η0 η0′ .
It remains to show R Heap ⊥ h0 h′0 in order to get the final result R (Heap ⊗
Γ)⊥ (h0 , η0 ) (h′0 , η0′ ). We argue by cases on B.
—B  Own: Writing fields′ for the fields given by CT ′ , we have fields B = fields′ B
and thus R (state B) [fields B 7→ defaults] [fields′ B 7→ defaults]. So, as B is
non-rep and B 6= Own, we can add ℓ to Ch and Ch ′ to get partitions that
witness R Heap h1 h′1 . We also have conf B (h1 , η1 ) and conf B (h′1 , η1′ ) because
conf h, conf h′ , and defaults do not contain any locations. Now by Lemma 7.21
ACM Journal Name, Vol. V, No. N, Month 20YY.

52

·

A. Banerjee and D. Naumann

we get R Heap ⊥ h0 h′0 . Combining this with what was shown above we have
R (Heap ⊗ Γ)⊥ (h0 , η0 ) (h′0 , η0′ ).
—B ≤ Own: By basic coupling, Def. 7.9, we have R Heap ⊥ h0 h′0 .
Case Γ ⊢ x := e.m(e). By Lemma 7.22 for e we have R D⊥ ℓ ℓ′ , hence ℓ = ℓ′ by
′
Lemma 7.12. Let η1 = [self 7→ ℓ, x 7→ d] and η1′ = [self 7→ ℓ, x 7→ d ]. By confinement
of x := e.m(e) (Def. 6.7) we have confined arguments, i.e., conf (loctype ℓ) (h, η1 )
′
and conf (loctype ℓ) (h′ , η1′ ). By Lemma 7.22 for e we have R U ⊥ d d and hence
′
R U d d as we are considering the non-⊥ case. Thus R [x : T , self : loctype ℓ] η1 η1′
by Lemma 7.13. From R MEnv µ µ′ we get
R (loctype ℓ, x, T →T ) (µ(loctype ℓ)m) (µ′ (loctype ℓ)m)
hence, as h, h′ , η1 , η1′ are confined and related, R (Heap ⊗ T )⊥ (h1 , d1 ) (h′1 , d′1 ),
where (h1 , d1 ) = µ(loctype ℓ)m(h, η) and (h′1 , d′1 ) = µ′ (loctype ℓ)m(h′ , η ′ ). Thus
R T d1 d1 and R Heap h1 h1 . It remains to show that the updated stores [η | x 7→
d1 ] and [η ′ | x 7→ d′1 ] are related for Γ. This follows from R T d1 d′1 and T ≤ Γ x,
using Lemma 7.13.
The remaining cases are similar. See Appendix.
8. APPLICATIONS AND FURTHER EXAMPLES
In this section we use the abstraction theorem to show some program equivalences
for the examples discussed in Sections 2 and 3. Then we discuss further variations
on the observer pattern.
To establish the hypothesis of the abstraction theorem for the examples we use
the couplings given as examples in Sect. 7.2. Both the theorem and these couplings
are defined in terms of the semantics. To show that the couplings are simulations
we argue directly in terms of the semantics. For practical purposes in program
verification, the abstraction theorem would be expressed syntactically as a proof
rule and rules for program constructs would be used to establish the simulation
property [Reynolds 1981a; Jones 1986; Morgan and Gardiner 1990; de Roever and
Engelhardt 1998]. Adequate proof rules for a language like ours remains an open
challenge (see Sect. 12).
8.1 Program equivalence
We take program to mean a well formed class table CT together with a command
Γ ⊢ S. We consider the object states reachable from variables of Γ to be the inputs and outputs of the program. For example, if S is the body of method main in
Sect. 2.1 then Γ is self:Main and what can be reached is self and the string self.inout.
We restrict attention to confined programs, meaning that CT and Γ ⊢ S are confined. Thus, by Theorem 6.17 the method environment [[CT ]] is confined. To prove
program equivalence using the abstraction theorem, we need to both introduce and
eliminate a simulation. Elimination is by identity extension Lemma 7.17 and introduction is by the related Lemma 7.18. There is a small technicality: To establish
the hypothesis of Lemma 7.23, we require w.o.l.o.g. that S occurs in some method
of CT .
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

53

We compare programs only for class tables CT, CT ′ that are comparable in the
sense of Def. 7.1, and with commands in the same context Γ. As commands denote
functions on global states, the obvious notion of equivalence is that [[Γ ⊢ S]] and
[[Γ ⊢′ S ′ ]]′ are equal as functions. By Lemma 7.11, [[Γ]] = [[Γ]]′ for any Γ, but
in general the semantic domains differ for owner object states which may have
different private fields. A global state (h, η) ∈ [[Heap ⊗ Γ]] for CT need not be an
element of [[Heap ⊗ Γ]]′ for CT ′ . However, an Own-free heap in [[Heap]] is also an
element of [[Heap]]′ . So we compare command meanings on the Own-free states.
Definition 8.1 (client program equivalence) Suppose programs CT, (Γ ⊢ S)
and CT ′ , (Γ ⊢′ S ′ ) are such that CT, CT ′ are comparable and confined, and moreover S (resp. S ′ ) occurs in CT (resp. CT ′ ). The programs are equivalent iff
collect([[Γ ⊢ S]]µ̂(h, η)) = collect([[Γ ⊢′ S ′ ]]′ µ̂′ (h, η))
for all confined and Own-free (h, η) ∈ [[Heap ⊗ Γ]], where µ̂ = [[CT ]] and µ̂′ =
[[CT ′ ]]′ .
If Γ self ≤ Own then η cannot be Own-free. The resulting vacuous quantification
makes the definition equate all commands for such Γ. But we are only interested
in using the definition for clients. Simulation is the relation of interest between
owners.
The static analysis for confinement Sect. 11 can be used to show that each of the
following examples is confined for the appropriate Own and Rep.
Example 8.2 Consider the command S comprising the body of method main of
class Main in Sect. 2.1 and take Γ = (self : Main). As CT we take the declarations
of Main, Bool, and the first version of OBool. For CT ′ we use the second version
of OBool. Let Rep and Rep′ be Bool and Own be OBool.
To show that CT, (Γ ⊢ S) is equivalent to CT ′ , (Γ ⊢ S), recall the basic coupling
of Example 7.5 and let R be the induced coupling. Let (h, η) be any confined state
for Γ, noting that Main 6≤
> Own so η is Own-free. Let µ̂ = [[CT ]] and µ̂′ = [[CT ′ ]]′ .
To show
collect([[Γ ⊢ S]]µ̂(h, η)) = collect([[Γ ⊢′ S ′ ]]′ µ̂′ (h, η)) ,

(∗)

note first that R (Heap ⊗ Γ) (h, η) (h, η) by Lemma 7.18. It is straightforward to
show that R is established by the constructors and preserved by the methods of
OBool; thus R is a simulation. The abstraction theorem yields R MEnv µ̂ µ̂′ . This
in turn justifies application of the preservation Lemma 7.23 to command S, as its
context M ain is a non-rep class 6= Own. Thus the outcomes [[Γ ⊢ S]]µ̂(h, η) and
[[Γ ⊢′ S ′ ]]′ µ̂′ (h, η) are related by R. By definition of R, either both outcomes are ⊥,
in which case (∗) holds by definition of collect, or the outcomes are non-⊥ states
(h0 , η0 ) and (h′0 , η0′ ) with R (Heap ⊗ Γ) (h0 , η0 ) (h′0 , η0′ ). Note that h0 and h′0 each
contains at least one owner, the one constructed in S. But M ain 6≤
> Own, so rng η0
and rng η0′ are Own-free. Moreover, the owners were reached only by variable z
which is local in S; they are not reachable via fields of the objects h0 (η self) or
h′0 (η ′ self). That is, both collect(h0 , η0 ) and collect(h′0 , η0′ ) are Own-free. Thus
by identity extension Lemma 7.17 we have collect(h0 , η0 ) = collect(h′0 , η0′ ) which
concludes the proof of (∗).
ACM Journal Name, Vol. V, No. N, Month 20YY.

54

·

A. Banerjee and D. Naumann

This proof depends on parametricity of the allocator, because that is needed
for the abstraction theorem. The same argument will go through, however, for the
second abstraction theorem in the sequel which drops parametricity of the allocator.
Example 8.3 Recall the Meyer-Sieber-O’Hearn example from Sect. 3.1, and in
particular the command
C y := new C in A x := new A in x.callP(y)

(‡)

Take (‡) to be the body of method main in
class Main extends Object { unit main(){ . . . } }
To be very precise we need to include a class
class Rep extends Object { }
so we can take Rep and Rep′ to be Rep which is not comparable to the classes C
and A of interest. Let Own be A. Let CT consist of the declarations of A, Rep,
Main, and an arbitrary class
class C extends Object { unit P(A z){ . . . } . . . }
such that methods of C satisfy the confinement conditions. Then CT and CT ′
are confined, because no reps are constructed or manipulated. We use the basic
coupling of Example 7.6. To appeal to the abstraction theorem, we must argue
that R is a simulation. The constructors are skip and the default value 0 for
field g establishes the relation. Preservation by inc is straightforward because both
versions have the same code and it makes no method calls. We give the details
for preservation by callP. The relevant condition is Def. 7.9(2a). To show it for
callP, suppose i ≥ 0 and R MEnv µi µ′i . Note that µi and µ′i are confined, by
Theorem 6.17. Suppose that R (Heap⊗y : C, self : A) (h, η) (h′ , η ′ ) with conf A (h, η)
and conf A (h′ , η ′ ). In both versions of callP, the body is a sequence and the first
command is y.P(self). Let η1 = [z 7→ η self, self 7→ η y] and η1′ = [z 7→ η ′ self, self 7→
η ′ y] be the environments for semantics of this call. By definition of R we get
R (Heap ⊗ z : A, self : C) (h, η1 ) (h′ , η1′ ). From the hypothesis conf A (h, η) we get
conf C (h, η1 ) and likewise conf C (h′ , η1′ ). Applying the hypothesis R MEnv µ µ′ to
these environments we get that either µCP (h, η1 ) = ⊥ = µCP (h, η1 ) or neither are
⊥ and R (Heap ⊗ unit) (h0 , it ) (h′0 , it ) where (h0 , it ) = µCP (h, η1 ) and (h′0 , it ) =
µ′ CP (h′ , η1′ ). The call is desugared to an assignment of the result value to a local
but the value is discarded for both versions, so the states following the calls are
(h0 , η) and (h′0 , η ′ ) and we have R (Heap ⊗ y : C, self : A) (h0 , η) (h′0 , η ′ ). In these
states we have h0 ℓg = h′0 ℓg ∧ h0 ℓg mod 2 = 0. So the command
if self.g mod 2 = 0 then abort else skip fi
aborts, as does its counterpart which is simply abort. This concludes the argument
that the bodies of callP are related.
Having established the antecedents of the abstraction theorem, we conclude that
the command (‡) preserves R. By semantics of the second version of A we know
callP aborts, so both interpretations of (‡) abort. The programs are equivalent.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

55

This example is handled without using the identity extension Lemma 7.17, but
that is only because the example uses abortion. In subsequent examples the proof
needs all the steps of the one for Example 8.2. The steps are not spelled out in
detail; only the interesting bits are highlighted.
Example 8.4 We consider the observer pattern, taking Own to be Observable. Let
CT be given by the first version, Fig. 2, together with the client given in Fig. 3.
Let CT ′ be given by the sentinel version of 4 together with Fig. 3. We consider
equivalence for the command self:Main,ob:AnObserver ⊢ S where S is the body of
Main.main. Because obl is local to S, no owners are reachable in the final state.
Taking Rep, Rep′ to be Node,Node2, we use the coupling relation of Example 7.7.
Clearly the constructors establish the relation. To show that method add preserves
it, note that the bodies of these methods are both sequential compositions; both
construct a new node and then set its ob field to the value passed as a parameter.
The next step is to add it to the beginning of the list; the difference between the
two versions is that self.snt.nxt is assigned in Fig. 4 whereas self.fst is assigned in
Fig. 2. Both versions of add then invoke methods on the new node n. In practice
one would argue in terms of the behavior of those methods. Note that they need not
preserve the relation; it is just that their behavior is used to maintain the relation.
To give a precise argument in terms of the semantics, we consider cases on i. For
i = 0, both µi and µ′i make every method abort, in which case the body of add
aborts due to method calls. As the methods in class Node and class Node2 are not
recursive, their semantics is already completely defined for i = 1, so for i > 0 the
behavior of add is to insert nodes at the head of the list, maintaining the relation.
The remaining owner method is notifyAll. Again, the two versions are similar
except for skipping over the sentinel node. To argue that the calls to getNext act
correctly one considers cases as in the proof for add. For the calls to notify on
the Observer objects, recall that by the relation, the related lists contain the same
Observer pointers in the same order. The two versions thus make the same series
of invocations of notify. Each of those calls preserves the relation by hypothesis
R MEnv µi µ′i .
The last step of the argument, concerning invocations of notify, is like reasoning
about invocations of P in Example 8.3. This example has the additional complication of calls to objects within the owner island. The case distinction between
i = 0 and i > 0 is needed because our argument is purely in semantic terms. In a
practical proof system, one would reason only in terms of the actual semantics of
the methods involved rather than its approximants.
Strictly speaking, use of Lemma 7.23 depends on desugaring the examples, and
the desugarings Remark 4.1 do not include loops. We return to this issue in Sect. 9.
Example 8.5 Suppose we change the client of Fig. 3 to use the following.
class AnObserver extends Observer { unit notify(){ skip } }
Then in Fig. 4 we can replace the body of Observable.notifyAll by skip and still
have equivalence with the implementation of Fig. 2. What changes with respect to
Example 8.4 is that the two implementations do not make the corresponding calls
to notify. But because AnObserver.notify is skip, calling it has the same effect as
not calling it; in particular, the relation is preserved.
ACM Journal Name, Vol. V, No. N, Month 20YY.

56

·

A. Banerjee and D. Naumann

class Node1 extends Object{ // rep for Observable
Observer ob;
Node1 nxt;
unit setOb(Observer o){ self.ob := o }
unit add(Node1 n){
Observer o := n.ob; n.ob := self.ob; self.ob := o; n.nxt := self.nxt; self.nxt := n }
unit notifyAll(){ self.ob.notify(); if self.nxt 6= null then self.nxt.notifyAll() else skip fi } }
class Observable extends Object{ // owner
Node1 fst;
unit add(Observer ob){
Node1 n := new Node1; n.setOb(ob); if self.fst = null then self.fst := n else self.fst.add(n) fi}
unit notifyAll(){ if self.fst 6= null then self.fst.notifyAll() else skip fi} }
Fig. 8.

Version of the observer pattern in object-oriented style: nodes are active.

class Node3 extends Object { // rep for Observable
Node3 nxt;
unit notif(){ skip }
unit notifyAll(){ self.notif(); if self.nxt 6= null then self.nxt.notifyAll() else skip fi }
unit add(Observer ob){ NodeO n := new NodeO; n.setOb(ob); n.nxt := self.nxt; self.nxt := n } }
class NodeO extends Node3 { // rep subclass
Observer ob;
unit setOb(Observer o){ self.ob := o }
unit notif(){ self.ob.notify() } }
class Observable extends Object{ // owner
Node3 snt;
con{ self.snt := new Node3 }
unit add(Observer ob){ self.snt.add(ob) }
unit notifyAll(){ self.snt.notifyAll() } }
Fig. 9. Sentinel in object-oriented style. In class Node3, method add constructs an object of the
subclass NodeO and method notifyAll uses dynamic dispatch of notif.

The argument here is not modular: by contrast with the preceding example, here
we reason directly in terms of the client code.
8.2 Further variations on observer
Fig. 8 gives another implementation of Observable, using a singly linked list but
with most of the work delegated to methods of Node1. Method add of class Node1
in the Figure is an example of class-based visibility: The private fields of object n
are both assigned and read.
Unlike the example of Sect. 3.1, where method P is called once by callP, method
Observable.notifyAll invokes notify on multiple objects —and multiple times if some
of those are aliases. By sharing state, it is possible for multiple observers to detect
the order in which they are notified. In our versions of Observable, method add
maintains the set in last-in order. In Fig. 8, method add in Node1 shuffles pointers
to maintain the last-in order.
A less awkward version, using a sentinel node, is given in Fig. 9.
The following example indicates the limits of what can be proved using the abstraction theorem. For this discussion, instead of treating loops as syntactic sugar
we assume they are in the language. The semantic clause would use a fixpoint
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

57

but this is separate from the fixpoint of the approximation chain used for method
meanings. Thus for each i > 0 the full semantics of a loop is defined in µi .
Example 8.6 Consider the versions given by Figs. 2 and 8. The data structures
are very similar; essentially the identity coupling can be used. (It is not literally
the identity, because because Node and Node1 are distinct classes and thus the
sets [[Node]] and [[Node1]] have no non-nil location in common. But that is just the
reflection of a coding trick in our formalization of semantics.) The bodies of add
and notifyAll in the two versions have significant differences in the calling graph,
and in particular notifyAll in one version uses a loop whereas in the other it calls
a recursive method in Node1. To reason about these would require proving a loop
invariant and verifying specifications for methods add and notifyAll in Node1. But
for this one wants the final semantics of the program, not the approximate one
given by µi and µ′i . For given i, the semantics of notifyAll is only defined up to
recursion depth i; for a list longer than that, the loop in Fig. 2 works correctly but
the recursion in Fig. 8 aborts.
By contrast, equivalence between Figs. 4 and 8 can be shown by an argument
similar to that in Example 8.4. They do not have the same method call graph, but
the called methods are not recursive so one can argue by cases for i = 0 and i > 0.
If the loop in Fig. 2 is treated as syntactic sugar for a method call then the
equivalence has a complicated proof in terms of corresponding unfoldings of the
semantic approximations. But this is an accidental feature of the example.
Example 8.6 might lead one to wonder whether there is a flaw in the definition
of simulation. Instead of requiring that owner methods preserve the relation given
any approximating and related environments µi , µ′i , perhaps it should be enough
to consider the final semantics [[CT ]], [[CT ′ ]]′ . But this is not a sufficiently strong
induction hypothesis to prove the abstraction theorem. In fact the example reflects
a limitation in most theories of simulation and logical relations: what can be shown
equivalent are programs with the same structure in some sense; see Sect. 12.
Example 8.7 Equivalence between the versions given by Figs. 8 and 9 can be
shown by an argument similar to that in Example 8.4. The basic coupling is
like that of Example 7.7 with minor changes: Rep, Rep′ are named Node1,Node3
and the sentinel is at location ℓ′0 ∈ locs(Node3) whereas the locations ℓ′1 , ℓ′3 , . . .
following it are in locs(NodeO). The method call graphs are not identical for the
two versions and dynamic dispatch is used in the second version for Node3.notif.
But the differences involve non-recursive methods and it suffices, as in Example 8.4,
to consider two cases for µi , µ′i , namely i = 0 and i > 0.
9. OWNER SUBCLASSING: THE PROTECTED INTERFACE
This section considers examples involving subclasses of the owner class. Rather
than formalizing the “protected” construct of Java, we address the issues using a
module construct. We augment the syntax to designate certain methods as having
module scope, meaning that they cannot be called by clients. The confinement
conditions for these methods are relaxed.
ACM Journal Name, Vol. V, No. N, Month 20YY.

58

·

A. Banerjee and D. Naumann

9.1 Owner subclassing and module scope
The code for notifyAll in Observable of Fig. 2 uses a loop. Here is an equivalent
version using a tail recursive helper method doNotif.
unit notifyAll(){ doNotif(self.fst) }
unit doNotif(Node n){
if n 6= null then n.getOb().notify(); doNotif(n.getNext()) else skip fi }
In a language with nested method declarations, doNotif could be declared within
notifyAll. Absent that, it could be given private scope, allowing its calls only in
Observable. But the language of Sects. 4–8 has only public methods. To apply our
abstraction theorem to the desugared version we would have to include a suitable
implementation of doNotif in every version. This can be done for the examples in
this paper, but it is awkward.
In Sect. 9.3 we add module-scoped methods to the language. These suffice for
desugaring loops and for interactions between reps and owners. In the sequel we
focus on their use in subclasses of Own.
Fig. 10 is a variation on the observer pattern in which class Observable has subclass ObservableAcc. For accounting purposes it keeps track of the number of times
each observer has been notified. To this end, the rep class NodeAcc overrides
method notifyAll of the client class Node4. Such examples have led to our treatment of owner subclasses: They are distinguished from clients in that their methods
may manipulate reps, but unlike Own they cannot store reps in fields.
Method addn has been added to Observable, so that ObservableAcc can construct
reps of the subtype NodeAcc and install although fst is a private field not visible
in ObservableAcc. Method Observable.getFirst is also added for this purpose. But
getFirst leaks a rep; it cannot be allowed in the public interface. One possibility
is to treat getFirst and addn as visible only in subclasses of Observable. Instead,
we give them module scope, meaning that calls to getFirst and addn are allowed in
subclasses of both Observable and Node4.
Method add in class ObservableAcc constructs a rep, violating the condition “no
reps in sub-owners” in Assumption 7.15. That assumption is needed for the first abstraction theorem because methods of an owner subclass are like clients in that they
must preserve the induced relation. That means in particular that they manipulate
related —i.e., equal— rep locations. (By contrast, methods of Own preserve the
basic coupling which need not impose a correspondence on rep locations.) But if we
compare two versions, one with sentinel node and one without, the parametricity
condition for fresh will not apply and the new objects in ObservableAcc.add will
be at different locations. The solution, given in Sect. 10, is to relax equality to
bijection.
This relaxation is needed anyway, to avoid unobservable distinctions. As an
example, suppose we add to class Observable in Fig. 2 the following method:
String version(){ result := new String(“vsn 0”) }
Consider an alternative that is identical in every way except for the following:
String version(){ result := new String(“trash”); result := new String(“vsn 0”) }
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

59

class Node4 extends Object { // rep for Observable
Observer ob;
Node4 nxt;
unit setOb(Observer o){ self.ob := o }
unit setNext(Node4 n){ self.nxt := n }
Observer getOb(){ result := self.ob }
Node4 getNext(){ result := self.nxt }
Node4 getNextPri(){ result := self.nxt }
unit notifyAll(){ self.ob.notify(); if self.nxt 6= null then self.nxt.notifyAll() else skip fi } }
class NodeAcc extends Node4 {
int notifs;
unit notifyAll(){ self.notifs := self.notifs+1; super.notifyAll() }
int notifications(Observer o){ result := 0;
if self = self.getOb() then result := notifs
else if self.getNext() 6= null then result := (NodeAcc)(self.getNext()).notifications(o)
else skip fi }}
class ObservableSup extends Object { // superclass of owner; ”abstract” class
unit add(Observer ob){ abort }
unit notifyAll(){ abort }
class Observable extends ObservableSup { // owner
Node4 fst; // first node of list
Node4 getFirst(){ result := self.fst } // module scope
unit add(Observer ob){ Node4 n := new Node4; self.addn(ob,n) }
unit addn(Observer ob, Node4 n){ n.setNext(self.fst); n.setOb(ob); self.fst := n } // module scope
unit notifyAll(){ self.fst.notifyAll() }
class ObservableAcc extends Observable {
unit add(Observer ob){ Node4 n := new NodeAcc(); self.addn(ob,n) }
int notifications(Observer ob){ result := ((NodeAcc)(self.getFirst())).notifications(ob) } }

Fig. 10. Version with owner and rep subclasses and super-call. The owner also has a superclass. The
two versions of getNext in Node4 are needed for later examples.

According to Def. 7.9, the induced relation for locations of type String is equality.
But, even if the allocator is parametric, the locations returned by these two methods
are not equal. (So condition (2a) fails in Def. 7.9 of simulation.) But they cannot
be distinguished; this claim is justified by the generalized theory of Sect. 10, where
the induced relation allows an arbitrary bijection between locations of client types
like String. For this example, the bijection would be extended to relate the returned
results from the two versions.
Returning to the example in Fig. 10, the interface betweeen Observable and its
subclass ObservableAcc is awkwardly designed. An improvement is to use the factory pattern [Gamma et al. 1995] so that add itself can be inherited. In Fig. 11, we
add method makeNode, which should have module scope, and remove addn.
To illustrate that owners may reference each other, let us add a method allNotifications which reports the number of times a given observer has been notified by
any observable in a group thereof. In the code of Fig. 12, groups are represented by
cyclic lists. An ObservableAccG is initially in a singleton group; groups grow using
method joinGroup.
These examples show subclasses of reps and owners. There is inheritance into
the owner but not into the rep. Inheritance into reps is disallowed by our definition
of confined class table, because to handle it requires a more sophisticated analysis
ACM Journal Name, Vol. V, No. N, Month 20YY.

60

·

A. Banerjee and D. Naumann

class Observable extends ObservableSup {
Node4 fst;
Node4 getFirst(){ result := self.fst } // module scope
Node4 makeNode(){ result := new Node4 } // module scope
unit add(Observer ob){ Node4 n := makeNode(); n.setNext(self.fst); n.setOb(ob); self.fst := n }
unit notifyAll(){ self.fst.notifyAll() } }
class ObservableAcc extends Observable {
Node4 makeNode(){ result := new NodeAcc } // module scope
int notifications(Observer ob){ result := ((NodeAcc)(self.getFirst())).notifications(ob) } }
Fig. 11.

Variation on Fig. 10 using factory pattern. Node4 and NodeAcc are as in Fig. 10.

class ObservableAccG extends ObservableAcc {
ObservableAccG peer;
con{ self.peer := self }
unit joinGroup(ObservableAccG o){ // pre: self.peer=self and o.peer is cyclic list of length ≥ 1
self.peer := o.peer; o.peer := self }
int allNotifications(Observer ob){
result := self.notifications(ob); ObservableAccG p := self.peer;
while p 6= self do result := result + p.notifications(ob); p := p.peer od } }

Fig. 12.

Extension of Fig. 10 or Fig. 11 with grouped owners.

class Observable extends ObservableSup {
Node4 snt;
con{ snt := new Node4 }
Node4 getFirst(){ result := self.snt.getNextPri() } // module scope
Node4 makeNode(){ result := new Node4 } // module scope
unit add(Observer ob){
Node4 n := makeNode(); n.setNext(self.snt.getNextPri()); n.setOb(ob); self.snt.setNext(n) }
unit notifyAll(){ self.snt.getNextPri().notifyAll() } }

Fig. 13.

Variation on Fig. 11 using sentinel.

to prevent leaks via self; a suitable analysis of “anonymous methods” is discussed
in Sect. 12. Inheritance into owners also needs restriction; we have chosen a simple
restriction that nonetheless allows the preceding examples.
Finally, let us consider an alternative version of Fig. 11 to illustrate the consequences of allowing the owner class, but not its subclasses, to differ in comparable
class tables. In Fig. 11 the subclass ObservableAcc manipulates reps, both constructing a new NodeAcc and invoking method notifications declared in NodeAcc.
Although an alternative version of Observable could use an entirely different type
of nodes internally, it has to provide method getFirst with return type Node4. Because clients can manipulate objects of class ObservableAcc, methods of that class
must preserve the relation and this only holds if methods they invoke preserve the
relation. So coupling must be preserved not only by public methods of Observable
but also by those module scope methods that are invoked in ObservableAcc. As
a simple example, Fig. 13 gives an alternative that uses Node4 and differs from
Fig. 11 only in using a sentinel node.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

61

9.2 On behavioral subclassing
Behavioral subclassing [Liskov and Wing 1994] is very useful for reasoning about
specific examples. However, as mentioned earlier, it is not required in general for
representation independence. Client, rep, or owner subclasses may fail to exhibit
behavioral subclassing. To illustrate the point let us consider two revisions of
Fig. 10, both of which violate behavioral subclassing. For the first example, we add
an overriding declaration to NodeAcc:
Node4 getNext(){ abort }
This causes NodeAcc to fail to be a behavioral subclass of Node4 by most definitions.
(It also prevents the intended functioning of the added method NodeAcc.notifications
and its callers). Nonetheless, there is still a simulation between Figs. 11 and 13.21
Making this true is the reason Fig. 13 uses getNextPri instead of getNext.
The second revision makes malicious use of a type test. We add nothing to
NodeAcc, but rather revise Node4 as follows:
unit notifyAll(){ if self is NodeAcc then abort else self.ob.notify() fi;
if self.nxt 6= null then self.nxt.notifyAll() else skip fi }
Method notifyAll in NodeAcc now fails to behave properly. In some sense, the
revised Node4 is non-monotonic with respect to subclassing. Again, there is still
a simulation between Figs. 11 and 13. Method notifyAll aborts for ObservableAcc
objects in both versions.
9.3 Formalization of module-scoped methods
In Sect. 8 we saw the need for methods that are effectively private to Own, for
desugaring loops, and also for methods in Own that cannot be called by clients but
can be called in subclasses of Own. There is also a need for methods of owners and
reps that can be called by each other but not by clients. For simplicity, we address
these needs with a simple notion: Own, Rep, and their subclasses are considered
to be inside a module, and methods may be designated as being visible only inside
the module.
To avoid belaboring the formalization, we make no change to the concrete syntax.
We assume that a class table designates the class names Own and Rep and is
equipped with a predicate mscope with the interpretation that mscope(m, C) means
this method has package scope. The following changes are made to the definitions
of preceding sections.
(1) For a well formed class table, mscope must satify conditions that reflect what in
practice would be achieved by declaring Rep, Own, and their subclasses inside
the module. If mscope(m, C) then
—C ≤ Own or C ≤ Rep,
—mtype(m, B) is undefined for B > Own and B > Rep, and
—B ≤ C implies mscope(m, B).
21 Here

we consider a class table comprised of Node4, NodeAcc, and ObservableSup from Fig. 10,
along with the overriding declaration NodeAcc.getNext and also Observable and ObservableAcc
from Fig. 11. The alternative class table is the same except for using Observable from Fig. 13.
ACM Journal Name, Vol. V, No. N, Month 20YY.

62

·

A. Banerjee and D. Naumann

(2) The typing rule for method call has an added restriction that module-scoped
methods are only visible within the module:
Γ ⊢ e : D mtype(m, D) = T →T
Γ ⊢ e : U U ≤ T x 6= self T ≤ Γ x
mscope(m, D) ⇒ Γ self ≤ Own ∨ Γ self ≤ Rep
Γ ✄ x := e.m(e)
(3) For method environments, the confinement condition of Def. 6.5(1) is replaced
by the following:
—C ≤ Own∧mscope(m, C) ⇒ conf C (h0 , η)∧h ✂ h0 ∧(d ∈ locs(Rep↓) ⇒ d ∈
d om(Rhj )) for some confining partition and j with η self ∈ d om(Oh j )
—C  Rep ∧ (C  Own ∨ ¬mscope(m, C)) ⇒ conf C (h0 , η) ∧ h ✂ h0 ∧ d 6∈
locs(Rep↓)
(4) For confinement of class tables, the restriction of Def. 6.9(3) is only applied to
methods with ¬(mscope(m, C)).
(5) For simulation, Def. 10.10 in the sequel revises Def. 7.9(2) to require preservation of the relation only for public methods, that is, if ¬(mscope(m, Own)). But
those module-scoped methods that are called in sub-owners must also preserve
the relation.
To formalize this, we define prot(m, C) just if C ≤ Own, mscope(m, Own), and
there is a call to m in some subclass of Own.
(6) Comparable class tables must agree on the public and protected methods of
Own. Def. 7.1(1) is extended to require that mscope(m, C) = mscope′ (m, C)
for all C 6= Own. Moreover, if mtype(m, Own) is defined then the following
hold (and mutatis mutandis for mtype′ ):
—¬mscope(m, Own) implies mtype′ (m, Own) = mtype(m, Own) and ¬mscope′ (m, Own),
and
—prot(m, Own) implies mtype′ (m, Own) = mtype(m, Own) and mscope′ (m, Own)
(which in turn implies prot′ (m, Own)).
Example 9.1 Method doNotif in Sect. 9.1 can be given module scope. It would not
be called in owner subclasses, so it is not required to be present in a comparable class
table. Method getFirst of Observable in Fig. 10 is called in subclass ObservableAcc,
so prot(getFirst, Observable) holds and getFirst must be present in a comparable
class table (and be simulated).
Results of Sections 5 and 6 hold for the extended language; the only proof affected
by the changes is that of Theorem 6.17 which says that [[CT ]] is confined if CT is
confined. The result holds for the revised definitions; the necessary revisions for
the proof are as follows:
—In the base case of the induction on depth, the argument proving confinement
of µi+1 Cm for the result value d goes by cases on C. The argument for the
case C ≤ Own still holds for m with ¬mscope(m, C). For the case C ≤ Own
and mscope(m, C), the revised definition requires the result value d to satisfy
d ∈ locs(Rep↓) ⇒ d ∈ d om(Rhj ) for some confining partition and j with η self ∈
d om(Oh j ). This follows by definition from conf C (h0 , η0 ).
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

63

—In the step of the induction on depth, there is case analysis on C and B, proving
claim conf B (h, η) and confinement of the result value d. For the case C ≤
Own < B, the argument still holds, noting that ¬mscope(m, C) because in a well
formed class table module-scoped methods do not occur outside owner and rep
classes. For the cases C < B ≤ Own and C < B ≤ Rep, the arguments still hold,
noting that the restrictions on mscope ensure mscope(m, B) = mscope(m, C) so
the relevant conditions are the same.
10. SECOND ABSTRACTION THEOREM
This section improves the first abstraction theorem in two ways. First, the result
applies to the language extended with modules (see Sect. 9.3). The module-scoped
methods of the two versions of Own can be different unless they are used in subclasses of Own. The second improvement is that parametricity of the allocator is
no longer required (cf. Sect. 7.3). To compare behaviors of two versions of a program we use a bijection between locations rather than equality. This can be seen as
expressing that the language is parametric in locations, which would fail if the language had pointer arithmetic. As discussed in Sect. 9.1, allowing bijection handles
the problem with new reps in sub-owners that necessitates Assumption 7.15. Moreover, it allows coarsening of the notion of equivalence for commands and method
meanings so that, for example, the bodies of the two versions of method version in
Sect. 9.1 are equivalent.
These extensions are enough to treat all the examples in Sect. 9.1 in addition to
those of Sect. 8 (except Example 8.6, for reasons discussed there).
Definition 10.1 (typed bijection) A typed bijection is finite bijective function
σ from Locs to Locs such that σ ℓ = ℓ′ implies loctype ℓ = loctype ℓ′ .
Throughout the section we let σ range over typed bijections and sometimes omit
the word “typed”. To express how bijections cut down to bijections on blocks of
partitions, we use the notation σ(X) for the direct image of X through σ.
Definition 10.2 (basic coupling) Given comparable class tables, a basic coupling is a function G that assigns to each typed bijection a binary relation G σ on
heaps (not necessarily closed heaps) that satisfies the following. For any σ, h, h′ , if
G σ h h′ then there are partitions h = Oh ∗ Rh and h′ = Oh ′ ∗ Rh ′ and locations ℓ
and ℓ′ in locs(Own↓) such that
(1) σ ℓ = ℓ′ and {ℓ} = d om Oh and {ℓ′ } = d om Oh ′
(2) d om(Rh) ⊆ locs(Rep↓) and d om(Rh ′ ) ⊆ locs(Rep′ ↓)
(3) G σ (type(f, loctype ℓ)) (hℓf ) (h′ ℓ′ f ) for all (f : T ) ∈ d om(fields(loctype ℓ)) with
f 6∈ g = d om(dfields(Own)) and f 6∈ g ′ = d om(dfields′ (Own)).
Item (3) uses the induced coupling G defined below; it is a harmless forward reference because the definition of G for data types does not depend on G (or G) for
heaps. Note that we do not require d om σ to include the reps, nor do we disallow
that it includes some of them.
Definition 10.3 (coupling relation, G) In the context of a basic coupling with
given relation G, and for each typed bijection σ, relations G σ θ ⊆ [[θ]] × [[θ]]′ as
ACM Journal Name, Vol. V, No. N, Month 20YY.

·

64

A. Banerjee and D. Naumann

follows. (Note that in the case of method meanings and method environments
there is no dependence on σ.)
For heaps h, h′ , we define G σ Heap h h′ iff there exist confining partitions of
h, h′ , with the same number n of owner islands, such that
—d om σ ⊆ d om h and rng σ ⊆ d om h′
—G σ (Oh i ∗ Rh i ) (Oh ′i ∗ Rh ′i ) for all i in 1..n
—σ(d om(Ch)) = d om(Ch ′ ), i.e., σ restricts to a bijection between d om(Ch) and
d om(Ch ′ )
—G σ (state (loctype ℓ)) (hℓ) (h′ ℓ′ ) for all ℓ, ℓ′ with ℓ ∈ d om(Ch) and σ ℓ ℓ′
For other categories θ we define G σ θ as follows.
G
G
G
G
G
G
G
G
G

G

bool d d′
⇔ d = d′
unit d d′
⇔ d = d′
′
Cdd
⇔ σ d = d′ ∨ d = nil = d′
Γ η η′
⇔ ∀x ∈ d om Γ • G σ (Γx) (ηx) (η ′ x)
′
(state C) s s
⇔
C  Own ∧ ∀f ∈ d om(fields C) • G σ (type(f, C)) (s f ) (s′ f )
σ (θ⊥ ) α α′
⇔ (α = ⊥ = α′ ) ∨ (α 6= ⊥ =
6 α′ ∧ G σ θ α α′ )
σ (Heap ⊗ Γ) (h, η) (h′ , η ′ ) ⇔ G σ Heap h h′ ∧ G σ Γ η η ′
σ (Heap ⊗ T ) (h, d) (h′ , d′ ) ⇔ G σ Heap h h′ ∧ G σ T d d′
⇔ ∀σ, (h, η) ∈ [[Heap ⊗ Γ]], (h′ , η ′ ) ∈ [[Heap ⊗ Γ]]′ •
(C, x, T →T ) d d′
G σ (Heap ⊗ Γ) (h, η) (h′ , η ′ ) ∧ conf C (h, η) ∧ conf C (h′ , η ′ )
⇒ ∃σ0 ⊇ σ • G σ0 (Heap ⊗ T )⊥ (d(h, η)) (d′ (h′ , η ′ ))
where Γ = [x 7→ T , self 7→ C]
MEnv µ µ′
⇔ ∀C, m •
(¬mscope(m, C) ∨ prot(m, C)) ∧ (C is non-rep) ∧ (mtype(m, C) is defined)
⇒ G (C, pars(m, C), mtype(m, C)) (µ C m) (µ′ C m)
σ
σ
σ
σ
σ

(Recall that prot is defined in (5) of Sect. 9.3.)
As an example, the body of makeNode in ObservableAcc (Fig. 11) returns a new
rep. Consider a coupling with a version using a sentinel. Given a bijection σ
and related heaps h, h′ , the location ℓ = fresh(Node4, h) may be different from
ℓ′ = fresh(Node4, h′ ) even if fresh is parametric, because h′ has extra reps, the
sentinels. But σ can be extended with the pair (ℓ, ℓ′ ).
The following facts are straightforward consequences of the definition. The first
says that if h and h′ are related by G at σ, then σ is a bijection between the domains
of h and h′ except for reps.
Lemma 10.4 For all σ, h, h′ and all ℓ, ℓ′ not in locs(Rep↓, Rep′ ↓), if G σ Heap h h′
then σ((d om h) ⇂ (locs(Rep↓, Rep′ ↓))) = (d om h′ ) ⇂ (locs(Rep↓, Rep′ ↓)).
Lemma 10.5 If U ≤ T and G σ U d d′ then G σ T d d′ .
For equivalence of values and states, we define a family of relations indexed on
categories θ. To streamline the notation, we say “x ∼σ x′ in [[θ]]” here, and simply
use the symbol ∼σ later.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

65

Definition 10.6 (value equivalence) For any σ, we define a relation ∼σ for data
values, object states, heaps, and stores, as follows.
ℓ ∼σ ℓ′
d ∼σ d′
s ∼ σ s′
η ∼σ η ′
h ∼ σ h′
(h, η) ∼σ (h′ , η ′ )
d ∼σ d′

in
in
in
in
in
in
in

[[C]]
[[T ]]
[[state C]]
[[Γ]]
[[Heap]]
[[Heap ⊗ Γ]]
[[θ⊥ ]]

⇔
⇔
⇔
⇔
⇔
⇔
⇔

σ ℓ = ℓ′ ∨ ℓ = nil = ℓ′
d = d′ for primitive types T
∀f ∈ fields C • sf ∼σ s′ f
∀x ∈ d om Γ • η x ∼σ η ′ x
σ(d om h) = d om h′ ∧ ∀ℓ ∈ d om h • h ℓ ∼σ h′ (σ ℓ)
h ∼ σ h′ ∧ η ∼ σ η ′
d = ⊥ = d′ ∨ (d 6= ⊥ =
6 d′ ∧ d ∼σ d′ in [[θ]])

Lemma 10.7 (identity extension) Suppose G σ (Heap ⊗ Γ) (h, η) (h′ , η ′ ) and
Γ self is non-rep. Let (h, η) and (h′ , η ′ ) be confined at Γ self. If both collect(η, h)
and collect(η ′ , h′ ) are Own-free then collect(η, h) ∼σ collect(η ′ , h′ ).
The reader may care to check that in the case that σ is equality, the relations
G σ θ coincide with R θ and ∼σ is just equality.
Definition 10.8 (client program equivalence) Suppose programs CT, (Γ ⊢ S)
and CT ′ , (Γ ⊢′ S ′ ) are such that CT, CT ′ are comparable and confined, and moreover S (resp. S ′ ) occurs in CT (resp. CT ′ ). The programs are equivalent iff for all
confined, Own-free (h, η) and (h′ , η ′ ) in [[Heap ⊗ Γ]] and all σ with (h, η) ∼σ (h′ , η ′ ),
there is some σ0 ⊇ σ with
collect([[Γ ⊢ S]]µ̂(h, η)) ∼σ0 collect([[Γ ⊢′ S ′ ]]′ µ̂′ (h′ , η ′ )) ,
where µ̂ = [[CT ]] and µ̂′ = [[CT ′ ]]′ .
Lemma 10.9 Suppose C and all class names in T are non-rep, and B < C. If
G (C, x, T →T ) d d′ then G (B, x, T →T ) (restr (d, B)) (restr (d′ , B)) where restr is
the restriction to global states of B (see Def. 5.5).
As discussed in Sect. 9, the relation must be preserved not only by public methods
but also by any module scope methods that are called by methods declared in
subclasses of Own.
Definition 10.10 (simulation) A simulation is a coupling relation G such that
(1) (constructors of Own establish G) For any µ, µ′ , any ℓ, ℓ′ in locs(Own↓) with
σ ℓ = ℓ′ , and any h, h′ with G σ Heap h h′ , let
h1
h′1
h0
h′0

= [h | ℓ 7→ [fields(loctype ℓ) 7→ defaults]]
= [h′ | ℓ′ 7→ [fields′ (loctype ℓ′ ) 7→ defaults]]
= [[self : (loctype ℓ) ⊢ constr(loctype ℓ) : con]]µ̂(h1 , [self 7→ ℓ])
= [[self : (loctype ℓ′ ) ⊢′ constr(loctype ℓ′ ) : con]]′ µ̂′ (h′1 , [self 7→ ℓ′ ])

Then there is σ0 ⊇ σ such that G σ h0 h′0 .
(2) (methods of Own preserve G) Let µ ∈ N → [[MEnv ]] (resp. µ′ ∈ N → [[MEnv ]]′ )
be the approximation chain in the definition of [[CT ]] (resp. [[CT ′ ]]′ ). For every
m with mtype(m, Own) defined and ¬mscope(m, Own) or prot(m, Own), the
following implications hold for every i, where x = pars(m, Own) and T →T =
mtype(m, Own).
ACM Journal Name, Vol. V, No. N, Month 20YY.

66

·

A. Banerjee and D. Naumann

(a) G MEnv µi µ′i ⇒ G (Own, x, T →T ) ([[M ]]µi ) ([[M ′ ]]′ µ′i )
if m has declaration M in CT (Own) and M ′ in CT ′ (Own)
(b) G MEnv µi µ′i ⇒ G (Own, x, T →T ) ([[M ]]µi ) (restr ([[MB ]]′ µ′i , Own))
if m has declaration M in CT (Own) and is inherited from B in CT ′ (Own),
with MB the declaration of m in B
(c) G MEnv µi µ′i ⇒ G (Own, x, T →T ) (restr([[MB ]]µi , Own)) ([[M ′ ]]′ µ′i )
if m has declaration M ′ in CT ′ (Own) and is inherited from B in CT (Own),
with MB the declaration of m in B
Instead of Assumption 7.15 we need only the following.
Assumption 10.11 CT and CT ′ are confined class tables for which a (generalized)
simulation G is given.
Theorem 10.12 (abstraction) G MEnv [[CT ]] [[CT ′ ]]′ .
The proof is essentially the same as the proof of Theorem 7.20. The definition
of G MEnv requires the relation to be preserved by those module-scoped methods
that are called by subowners, and this is ensured by Def. 10.10(2) of simulation.
The lemmas used in the proof are as follows.
Lemma 10.13 (preservation by expressions) For any non-rep class C 6= Own
and any constituent expression Γ ⊢ e : T of a method declared in C, the following holds: For all σ and all (h, η) ∈ [[Heap ⊗ Γ]] and (h′ , η ′ ) ∈ [[Heap ⊗ Γ]]′ , if
G σ (Heap ⊗ Γ) (h, η) (h′ , η ′ ) then
G σ (T⊥ ) ([[Γ ⊢ e : T ]](h, η)) ([[Γ ⊢′ e : T ]]′ (h′ , η ′ )) .
Proof. The proof is very similar to the proof of Lemma 7.22 except in the case
of field access.
For Γ ⊢ e.f : T , the argument is as follows, for any σ. By induction on e we have
G σ C⊥ ℓ ℓ′ . In the non-⊥ case, ℓ 6= nil 6= ℓ′ hence, by definition of G, σ ℓ = ℓ′ . By
closure of the heaps, ℓ ∈ d om h and ℓ′ ∈ d om h′ .
We consider cases on whether C < Own. Consider confining partitions (Ch ∗
Oh 1 ∗ Rh 1 . . .) = h and (Ch ′ ∗ Oh ′1 ∗ Rh ′1 . . .) = h′ that have corresponding islands
as in the definition of R Heap. In the case C < Own, we have ℓ ∈ locs(Own↓) and
hence ℓ in some d om(Oh i ). From G σ Heap h h′ we have
G σ (Oh i ∗ hRepi ) (Oh ′i ∗ hRep′i )
and thus ℓ′ ∈ d om(Oh ′i ) by basic coupling Def. 10.2(1) and bijectivity of σ. Since
C 6= Own, we know by visibility that f is not in the private fields g of Own. Thus,
as type(f, loctype ℓ)) = T , we have G σ T (hℓf ) (h′ ℓ′ f ) by Def. 10.2(3).
In the case C  Own we have ℓ ∈ d om(Ch) and hence ℓ′ ∈ d om(Ch ′ ) by σ ℓ = ℓ′
and definition G Heap. Hence
G σ (state (loctype ℓ)) (hℓ) (h′ ℓ′ )
and thus G σ T (hℓf ) (h′ ℓ′ f ) by definition of G (state (loctype ℓ)). Note that
loctype ℓ = loctype ℓ′ because σ is a typed bijection.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

67

Lemma 10.14 (preservation by commands) Suppose that µ and µ′ are confined method environments and G MEnv µ µ′ . Then the following holds for any
non-rep class C 6= Own. For any constituent command Γ ⊢ S in a method declaration in CT (C), any σ, and any (h, η) ∈ [[Heap ⊗ Γ]] and (h′ , η ′ ) ∈ [[Heap ⊗ Γ]]′ , if
conf C (h, η), conf C (h′ , η ′ ), and G σ (Heap ⊗ Γ) (h, η) (h′ , η ′ ) then there is σ0 ⊇ σ
such that
G σ0 (Heap ⊗ Γ)⊥ ([[Γ ⊢ S]]µ(h, η)) ([[Γ ⊢′ S]]′ µ′ (h′ , η ′ )) .
Proof. The proof is very similar to the proof of the corresponding Lemma 7.23
except in the cases of method call, field update, and most interestingly new. We no
longer have the assumption of parametricity of the allocator, and we must consider
construction of reps in sub-owners. We also need an analog to Lemma 7.21, saying
that constructors establishes R:
Claim: For all σ and all (h, ℓ) ∈ [[Heap ⊗ C]] and (h′ , ℓ′ ) ∈ [[Heap ⊗ C]], if
G σ Heap h h′ and G σ C ℓ ℓ′ then there is σ0 ⊇ σ such that G σ0 Heap h0 h′0 where
h0 = [[self : C ⊢ constr C : con]]µ(h, [self 7→ ℓ])
h′0 = [[self : C ⊢′ constr C : con]]µ′ (h′ , [self 7→ ℓ′ ])
We omit the proof of the claim, which has the same structure as the proof of
Lemma 7.21.
Case Γ ⊢ x := e.m(e). This goes through as before except for the case where
C < Own. In that case, the called method may have module scope and this is why
such methods (designated by prot) are included in the definition of G MEnv .
Case Γ ⊢ e1 .f := e2 . By Lemma 10.13 for e1 we have G σ C ℓ ℓ′ , hence σ ℓ = ℓ′
definition of G. By Lemma 10.13 for e2 we have G σ U d d′ and hence G σ T d d′
by Lemma 10.5. To conclude the argument it suffices to show
G σ Heap [h | ℓ 7→ [hℓ | f 7→ d]] [h′ | ℓ′ 7→ [h′ ℓ′ | f 7→ d′ ]] .
′

(∗)

∗ Oh ′1 ∗ Rh ′1

Consider confining partitions (Ch ∗ Oh 1 ∗ Rh 1 . . .) = h and (Ch
. . .) = h′
′
that correspond as in the definition of G σ Heap h h . We argue by cases on C.
—C < Own: Then loctype ℓ ≤ C < Own. By σ ℓ = ℓ′ and G σ Heap h h′ , there is i
such that {ℓ} = d om(Oh i ) and {ℓ′ } = d om(Oh ′i ) and
G σ (Oh i ∗ Rh i ) (Oh ′i ∗ Rh ′i ) .
By typing and C 6= Own, field f is not in the private fields g of Own. So (∗)
follows from G σ Heap h h′ and G σ T d d′ .
—C  Own: As C is non-rep, we have ℓ ∈ d om Ch and ℓ′ ∈ d om Ch ′ . Moreover,
G σ (state (loctype ℓ)) (hℓ) (h′ ℓ′ ) and so by G σ T d d′ we get
G σ (state (loctype ℓ)) [hℓ | f 7→ d] [h′ ℓ′ | f 7→ d′ ] .
Hence (∗).
Case Γ ⊢ x := new B. By confinement of CT , this command is confined and
hence the final states are confined: conf C (h0 , η0 ) and conf C (h′0 , η0′ ). We have
C  Rep and C 6= Own. Let ℓ = fresh(B, h) and ℓ′ = fresh(B, h′ ). Define
ACM Journal Name, Vol. V, No. N, Month 20YY.

68

·

A. Banerjee and D. Naumann

σ1 = σ ∪ {(ℓ, ℓ′ )}. This makes σ1 bijective because ℓ, ℓ′ are fresh and G σ Heap h h′
implies, by definition, that d om σ ⊆ d om h and rng σ ⊆ d om h′ .
By G σ Γ η η ′ and definition of σ1 we have G σ1 Γ η0 η0′ . We proceed to show
G σ1 Heap h0 h′0 , by cases on B.
—B  Own ∧ B  Rep: We have fields B = fields′ B and thus
G σ1 (state B) [fields B 7→ defaults] [fields′ B 7→ defaults] .
So, as B is non-rep and B 6= Own, we can add ℓ to Ch and ℓ′ to Ch ′ to get
partitions that witness G σ1 Heap h1 h′1 . Now the induction hypothesis yields
some σ0 ⊇ σ1 such that G σ0 Heap h0 h′0 . We obtain G σ0 Γ η0 η0′ from
G σ1 Γ η0 η0′ because σ0 ⊇ σ1 .
—B ≤ Own: By basic coupling, Def. 10.2, we get σ0 with G σ0 h2 h′2 . Moreover,
h2 and h′2 are owner islands and the confining partitions for h, h′ extend to ones
for h ∗ h2 . and h′ ∗ h′2 with σ0 . Finally, by definition of G we get G σ0 Heap h0 h′0
as h0 = h ∗ h2 and h′0 = h′ ∗ h′2 .
—B ≤ Rep: Here, C ≤ Own or C ≤ Rep, as otherwise the command would not be
confined. Let j be such that η self ∈ d om(Oh j ∗ Rh j ). Add ℓ to Rh j and ℓ′ to
Rh ′j . This yields G σ0 Heap h0 h′0 with h0 = h ∗ h2 and h′0 = h′ ∗ h′2 .
11. STATIC ANALYSIS
This section gives a syntax directed static analysis. It checks a property called
safety. Safety is shown to imply confinement.
The input is a well formed class table and designated class names Own and Rep.
With one exception, only rep and owner code (including subclasses) is constrained.
The exception is for new: a client cannot construct a new rep. For practical
application, this can be ensured in a modular way: Rep and its subclasses would
simply be declared with module scope.
The analysis is given for the language extended in Sect. 9.3 with module-scoped
methods. For the original language, mscope(m, C) can be taken to be false for all
m and C.
Definition 11.1 (safe) Class table CT is safe iff for every C and every m with
mtype(m, C) = T →T the following hold.
(1) If m is declared in C by T m(T x){S} then x : T , self : C, result : T ✄ S where ✄
is the safety relation defined in the sequel.
(2) self : C ✄ constr C, for all C
(3) If C ≤ Own and ¬mscope(m, C) then T 6≤
> Rep.
> Rep.
(4) If m is inherited in Own from some B > Own then T 6≤
(5) No m is inherited in Rep from any B > Rep.
The safety relation ✄ is defined by the following rules. There is no restriction on
field declarations per se. A client can have a Rep type field, but can assign only
null to it.
Safety for expressions
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

Γ ✄ x : Γx

Γ ✄ null : B

·

69

Γ ✄ it : unit Γ ✄ true : bool Γ ✄ false : bool

C = (Γ self) Γ ✄ e : C (f : T ) ∈ dfields C
C = Own ∧ e 6= self ⇒ T 6≤
> Rep
C < Own ⇒ T 6≤
> Rep
Γ ✄ e.f : T
Γ ✄ e1 : T Γ ✄ e2 : T
Γ ✄ e1 = e2 : bool

Γ ✄ e:D B ≤ D
Γ ✄ (B) e : B

Γ ✄ e:D B ≤ D
Γ ✄ e is B : bool

For expressions, the analysis imposes restrictions on field accesses and nothing
else. If e.f appears in the body of an owner method, then a Rep can be accessed
only via the private fields of Own; this requires e to be self. If e.f appears in
a sub-owner, then the private fields of Own cannot be accessed, hence the result
cannot be a Rep.
For commands, the rules impose restrictions on new, field update, and method
call. The conditions on field update are analogous to those for field access. For an
object construction x := new B in the body of a client method, it cannot create a
new rep. And, if it appears in a subclass of Rep, it cannot create a new owner as
this would break confinement of the heap.
For method call x := e.m(e), the condition labelled (a) says that if m is a client
method called from a subclass of Own or Rep, then m cannot be passed reps as
parameters. Conditions (b) and (c) consider method calls from an owner class or
its subclasses: (b) says that if m’s type is comparable to Own then reps can be
passed as parameters only if e is self. Finally, (c) says that if m’s type is comparable
to Rep then no owner, other than itself, can be passed as parameter —otherwise
confinement will be violated.

Safety for commands
ACM Journal Name, Vol. V, No. N, Month 20YY.

70

·

A. Banerjee and D. Naumann

C = (Γ self)
(f : T ) ∈ dfields C
Γ ✄ e1 : C Γ ✄ e2 : U U ≤ T
C = Own ∧ e1 6= self ⇒ U 6≤
> Rep
C < Own ⇒ U 6≤
> Rep
Γ ✄ e1 .f := e2

x 6= self B ≤ Γx B 6= Object
C  Rep ∧ C  Own ⇒ B  Rep
C ≤ Rep ⇒ B  Own
Γ ✄ x := new B

Γ ✄ e : D mtype(m, D) = T →T T ≤ Γ x
Γ ✄ e : U U ≤ T x 6= self
C = (Γ self)
mscope(m, D) ⇒ C ≤ Own ∨ C ≤ Rep
(a) (C ≤ Own ∨ C ≤ Rep) ∧ D 6≤ Rep ∧ D 6≤ Own ⇒ T 6≤
> Rep
> Rep
(b) C ≤ Own ⇒ D 6≤
> Own ∨ (e = self) ∨ T 6≤
(c) C ≤ Own ⇒ D 6≤
> Rep ∨ (∀ei ∈ e • ei 6= self ⇒ Ti 6≤
> Own)
Γ ✄ x := e.m(e)
C = (Γ self) mtype(m, super C) = T →T
Γ ✄ e : U U ≤ T x 6= self T ≤ Γ x
Γ ✄ x := super.m(e)
x 6= self Γ ✄ e : T T ≤ Γ x
Γ ✄ x := e
Γ ✄ e : bool Γ ✄ S1 Γ ✄ S2
Γ ✄ if e then S1 else S2 fi

Γ ✄ S1 Γ ✄ S2
Γ ✄ S1 ; S2

Γ ✄ e : U U ≤ T (Γ, x : T ) ✄ S
Γ ✄ T x := e in S

Theorem 11.2 (soundness) If CT is safe then it is confined.
Proof. Items (3)–(5) in the definition of safety are the same as items (3)–(5) in
the definition of confinement for class tables. For items (1) and (2), the confinement
of method and constructor bodies follows from safety thereof, by Lemmas 11.3, 11.5,
and 11.6 to follow.
Lemma 11.3 (argument values confined) Suppose Γ ⊢ e : D and Γ ⊢ e : U are
confined.
(1) If Γ ✄ x := e.m(e) then Γ ⊢ x := e.m(e) has confined arguments.
(2) If Γ ✄ x := super.m(e) then Γ ⊢ x := super.m(e) has confined arguments.
Proof. We give the argument for (1); the argument for (2) is similar (see Appendix).
As in Def. 6.8, let C = (Γ self). Assume conf µ and conf C (h, η). Let ℓ =
[[Γ ⊢ e : D]]µ(h, η), let d = [[Γ ⊢ e : U ]]µ(h, η), and let η1 = [self 7→ ℓ, x 7→ d]. Finally,
let ℓ 6= nil , ℓ 6= ⊥ and d 6= ⊥.
Because Γ ✄ x := e.m(e) holds we can use conditions (a)–(c) in the analysis rule
for method call. Now the proof proceeds by cases on C with subcases on loctype ℓ.
In each case we show conf (loctype ℓ) (h, η1 ).
—C  Rep ∧ C  Own: Because e and e are confined at C, we have ℓ 6∈ locs(Rep↓)
and di 6∈ locs(Rep↓) for all di ∈ d. Thus rng η1 ∩ locs(Rep↓) = ∅ proving
conf (loctype ℓ) (h, η1 ) by Def. 6.4(1).
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

71

—C ≤ Own: Choose a confining partition and let j be such that η self ∈ d om(Oh j ).
Because e and e are confined at C, we have ℓ ∈ locs(Rep↓) ⇒ ℓ ∈ d om(Rh j )
and di ∈ locs(Rep↓) ⇒ di ∈ d om(Rh j ) for all di ∈ d. Now we go by cases on
loctype ℓ:
—loctype ℓ  Rep ∧ loctype ℓ  Own: Because loctype ℓ ≤ D we have D 
Rep ∧ D  Own. Hence by condition (a) of the analysis, T 6≤
> Rep. Thus
rng η1 ∩ locs(Rep↓) = ∅ proving conf (loctype ℓ) (h, η1 ) by Def. 6.4(1).
—loctype ℓ ≤ Own: Hence ℓ ∈ d om(Oh k ) for some k. Because loctype ℓ ≤ D
we have, D ≤ Own ∨ Own ≤ D. If e = self then ℓ = (η self) and k = j.
Then rng η1 ∩ locs(Rep↓) = d ∩ locs(Rep↓) ⊆ d om(Rh j ) = d om(Rh k ). Thus
conf (loctype ℓ) (h, η1 ) by Def. 6.4(2). If e 6= self then by condition (b) of the
> Rep. Hence rng η1 ∩locs(Rep↓) = ∅ proving conf (loctype ℓ) (h, η1 )
analysis, T 6≤
by Def. 6.4(2).
—loctype ℓ ≤ Rep: Hence ℓ ∈ d om(Rh j ) by confinement of e at C. As loctype ℓ ≤
D we have, D ≤ Rep∨Rep ≤ D. By Def. 6.4(3), to show conf (loctype ℓ) (h, η1 ),
we must show rng η1 ∩ locs(Own↓, Rep↓) ⊆ d om(Oh j ∗ Rh j ). For any di ∈
locs(Own↓), because loctype di ≤ Ti , we have Ti ≤ Own ∨ Own ≤ Ti . So by
condition (c) of the analysis, ei = self, hence di = (η self) ∈ d om(Oh j ). For
any di ∈ locs(Rep↓) we have di ∈ d om(Rh j ) by confinement of e at C.
—C ≤ Rep: Choose a confining partition and let j be such that η self ∈ d om(Rh j ).
Because e and e are confined at C, we have ℓ ∈ locs(Own↓, Rep↓) ⇒ ℓ ∈
d om(Oh j ∗ Rh j ) and di ∈ locs(Own↓, Rep↓) ⇒ di ∈ d om(Oh j ∗ Rh j ) for all
di ∈ d. Now we go by cases on loctype ℓ.
—loctype ℓ  Rep ∧ loctype ℓ  Own: Because loctype ℓ ≤ D we have D 
> Rep. Thus
Rep ∧ D  Own. Hence by condition (a) of the analysis, T 6≤
rng η1 ∩ locs(Rep↓) = ∅ proving conf (loctype ℓ) (h, η1 ) by Def. 6.4(1).
—loctype ℓ ≤ Own: Hence ℓ ∈ d om(Oh j ). Now rng η1 ∩ locs(Rep↓) ⊆ d om(Rh j )
as required for conf (loctype ℓ) (h, η1 ) by Def. 6.4(2).
—loctype ℓ ≤ Rep: Hence ℓ ∈ d om(Rh j ). Now rng η1 ∩ locs(Own↓, Rep↓) ⊆
d om(Oh j ∗ Rh j ) as required for conf (loctype ℓ) (h, η1 ), by Def. 6.4(3).
Lemma 11.4 (soundness for expressions) If Γ✄e : T then Γ ⊢ e : T is confined.
Proof. Let C = (Γ self). Now we go by induction on Γ ✄ e : T .
conf C (h, η) and d = [[Γ ⊢ e : T ]](h, η) 6= ⊥ for each case of e.

Assume

Case Γ ✄ e.f : T . Then d = hℓf . We consider cases on C.
—C  Rep ∧ C  Own: We must show d 6∈ locs(Rep↓). Because loctype ℓ ≤ C, we
have ℓ 6∈ locs(Own↓, Rep↓). So ℓ is in the client part of a confining partition and
by Def. 6.2(1) we have d 6∈ locs(Rep↓).
—C ≤ Own: Consider a confining partition and j such that η self ∈ d om(Oh j ).
We must show d ∈ locs(Rep↓) ⇒ d ∈ d om(Rh j ). Assume d ∈ locs(Rep↓). If
C = Own, we have two subcases: If e = self we get ℓ = η self, so i = j and
d ∈ d om(Rh j ); if e 6= self then by the analysis we get T 6≤
> Rep so d 6∈ locs(Rep↓),
falsifying the antecedent. This concludes the case C = Own. If C < Own then
by the analysis T 6≤
> Rep so d 6∈ locs(Rep↓), falsifying the antecedent.
ACM Journal Name, Vol. V, No. N, Month 20YY.

72

·

A. Banerjee and D. Naumann

—C ≤ Rep: Consider a confining partition and j such that η self ∈ d om(Rh j ). We
must show d ∈ locs(Own↓, Rep↓) ⇒ d ∈ d om(Oh j ∗Rh j ). Since loctype ℓ ≤ C, we
have ℓ ∈ locs(Rep↓) and by induction on e we get ℓ ∈ d om(Rh j ) via Def. 6.6(3).
Because h is confined we get d ∈ d om(Oh j ∗ Rh j ) by Def. 6.2(4).
The remaining cases are similar; see Appendix.
Lemma 11.5 (soundness for constructors) Suppose that self : C ✄ constrC for
all C and let µ be arbitrary. Then the constructor semantics is confined in the
following sense: For all (h, η) with conf C (h, η) we have conf h0 and h ✂ h0 where
h0 = [[self : C ✄ constr C : con]]µ(h, η) 6= ⊥.
Proof. By well founded induction on C using the order ≪ in an argument
similar to that for Lemma 7.21. See Appendix.
Lemma 11.6 (soundness for commands) If Γ ✄ S then Γ ⊢ S is confined.
Proof. Let C = (Γ self). Now we go by induction on Γ ✄ S and by cases
on C. Assume conf C (h, η) and conf µ and [[Γ ⊢ S]]µ(h, η) 6= ⊥. Let (h0 , η0 ) =
[[Γ ⊢ S]]µ(h, η). In each case we must show h0 is confined and conf C (h0 , η0 ).
Case Γ ✄ e1 .f := e2 . Here η0 = η and h0 = [h | ℓ 7→ [hℓ | f 7→ d]]. Because
Γ ✄ e1 : C and Γ ✄ e2 : U , by Lemma 11.4, e1 and e2 are confined at C. We must
first show that h0 is confined and then show conf C (h0 , η0 ). By conf C (h, η) we
know there is a confining partition h = Ch ∗ . . .. We partition h0 using the given
partition for h. That is, the domain for each block, say Ch 0 , is the same as the
corresponding block for h, say Ch. We claim this partition is confining for h0 . It
then follows by Def. 6.3 that h ✂ h0 . Then by Lemma 6.13, we get conf C (h0 , η),
hence conf C (h0 , η0 ). It remains to show the claim for which we need to show the
conditions in Def. 6.2. We go by cases on C.
—C  Rep ∧ C  Own: Only condition (1) in Def. 6.2 can possibly be violated.
By conf C (h, η) we obtain rng η ∩ locs(Rep↓) = ∅. Because loctype ℓ ≤ C we
have ℓ ∈ d om(Ch 0 ). By confinement of e2 , d 6∈ locs(Rep↓). Hence Ch 0 6❀ Rh 0j
for all j.
—C ≤ Own: Let η self ∈ d om(Oh 0i ) for some i. Only conditions (2) and (3) in
Def. 6.2 can possibly be violated. Because loctype ℓ ≤ C, ℓ ∈ d om(Oh 0j ) for
some j. Because e2 is confined at C we have, d ∈ locs(Rep↓) ⇒ d ∈ d om(Rh 0i ).
We consider the case C = Own and e = self. Then ℓ = η self and i = j,
establishing condition (2). By typing, f ∈ g. Hence Oh i 6❀g Rh 0i establishing
condition (3). In the case e 6= self, by the analysis we have U 6≤
> Rep thus
establishing conditions (2) and (3).
Now we consider the case C < Own. By the analysis we have U 6≤
> Rep thus
establishing conditions (2) and (3).
—C ≤ Rep: Let η self ∈ d om(Rh 0i ) for some i. Only condition (4) in Def. 6.2 can
possibly be violated. Because loctype ℓ ≤ C, ℓ ∈ locs(Rep↓). By confinement
of e1 at C, we have ℓ ∈ d om(Rh 0i ). And, by confinement of e2 at C, we have
d ∈ locs(Own↓, Rep↓) ⇒ d ∈ d om(Oh 0i ∗ Rh 0i ). This establishes condition (4).
Case Γ ✄ x := e.m(e). Here h0 = h1 and η0 = [η | x 7→ d1 ]. Because Γ ✄ e : D
and Γ ✄ e : U , by Lemma 11.4, e and e are confined at C. By the analysis and
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

73

Lemma 11.3 we have conf (loctype ℓ) (h, η1 ). Then by assumption conf µ we get
conf (loctype ℓ) (h0 , η1 ). Hence h0 is confined. To show conf C (h0 , η0 ), we go by
cases on C:
—C  Rep∧C  Own: By conf µ, d1 6∈ locs(Rep↓). Hence rng η0 ∩locs(Rep↓) = ∅
by conf C (h, η).
—C ≤ Own: Let η self ∈ d om(Oh j ) for some j in the confining partition of h. By
conf µ, d1 6∈ locs(Rep↓) and h ✂ h0 . Because x 6= self, we have η0 self = η self.
Hence rng η0 ∩ locs(Rep↓) = rng η ∩ locs(Rep↓) ⊆ d om(Rh j ) by conf C (h, η).
As h ✂ h0 , d om(Rh j ) ⊆ d om(Rh 0j ). That is, rng η0 ∩ locs(Rep↓) ⊆ d om(Rh 0j ).
—C ≤ Rep: Because loctype ℓ ≤ C, let ℓ ∈ d om(Rhj ) for some j in the confining
partition of h. By conf µ, d1 ∈ locs(Own↓, Rep↓) ⇒ d1 ∈ d om(Oh 0j ∗ Rh 0j ) and
h ✂ h0 . Hence rng η0 ∩ locs(Own↓, Rep↓) ⊆ d om(Oh 0j ∗ Rh 0j ) by conf C (h, η)
and Def. 6.3.
Case Γ ✄ x := new B. First, we claim conf B (h1 , η1 ) and h ✂ h1 . Then by
Lemma 11.5 we get conf B (h0 , η1 ) and h1 ✂ h0 . So h ✂ h0 and by Lemma 6.13
conf C (h0 , η). To conclude, we argue that conf C (h0 , [η | x 7→ ℓ]) by cases on C.
—C  Own ∧ C  Rep: then B  Rep so ℓ 6∈ locs(Rep↓) by typing and hence
conf C (h0 , [η | x 7→ ℓ]).
—C ≤ Own: Let h = Ch ∗ (Oh 1 ∗ Rh 1 ) . . . (Oh k ∗ Rh k ) be a confining partition of h,
and j such that η self be in d om(Oh j ). If B  Rep then conf C (h0 , [η | x 7→ ℓ]) by
definition. If B ≤ Rep then we must show ℓ ∈ d om(Rh 0j ) where h0 has confining
extension h0 = Ch 0 ∗ (Oh 01 ∗ Rh 01 ) . . .. This is defined just as in the proof of
Lemma 6.16, and we choose to put ℓ and the objects it constructs in Rh j to
obtain Rh 0j .
—C ≤ Rep: By the static analysis, B  Own. So Oh 0j = Oh j . Thus rng [η | x 7→
ℓ] ∩ locs(Own↓, Rep↓) ⊆ d om(Oh j ∗ Rh 0j ). We choose to put ℓ and the objects it
constructs in Rh j to obtain Rh 0j , which makes the inclusion hold.
It remains to prove the claims conf B (h1 , η1 ) and h ✂ h1 . In the semantic definition, h1 = [h | ℓ 7→ [fields B 7→ defaults]] where ℓ = fresh(B, h). Define
Bh = [ℓ 7→ [fields B 7→ defaults]] so h1 = h ∗ Bh. Let η1 = [self 7→ ℓ]. Next,
we argue that h ✂ h1 and conf B (h1 , η1 ). Because h is closed, ℓ is not in the range
of any object state in h. To construct an extending partition it suffices to deal with
the new object, as its addition cannot violate confinement of existing objects. We
define the extension and argue by cases on B.
—B  Own ∧ B  Rep. For a confining partition of h1 we extend that for h
by defining Ch 0 = Ch ∗ Bh and using the given partition of owner islands.
Because defaults contains no locations, this is a confining partition and we have
conf B (h1 , η1 ).
—B ≤ Own. We extend the partition by adding an island Oh 0k+1 ∗ Rh 0k+1 with
Oh 0k+1 = Bh and Rh 0k+1 = ∅. This is a confining partition because defaults has
no locations and we have conf B (h1 , η1 ) because rng η1 has no reps.
—B ≤ Rep. Then, by the analysis we have C ≤ Own or C ≤ Rep; moreover as
x 6= self, we have η self 6= ℓ, so η self ∈ d om(Oh j ∗ Rh j ) for some j. Then we can
ACM Journal Name, Vol. V, No. N, Month 20YY.

74

·

A. Banerjee and D. Naumann

obtain a confining extension by adding Bh to Rh j , as defaults has no locations.
As rng η1 = {ℓ}, we have conf B (h1 , η1 ) by definition.
This concludes the argument for h ✂ h1 and conf B (h1 , η1 ).
The remaining cases are similar and can be found in the appendix.
12. DISCUSSION AND RELATED WORK
Programmers draw pictures of pointers in heap-based data structures and often
manage to get things right as far as the presence of pointers goes. For example, lists
don’t get disconnected. The absence of pointers is harder to picture and many bugs
are due to unexpected aliasing. Expectations are raised through use of encapsulation constructs such as private fields and modules, but heap structure is not entirely
manifested in language constructs. Simulation relations are often used for reasoning
about abstractions and here too aliasing presents a challenge: Multiple instances
of an abstraction may reference a shared client object or be shared by multiple
clients —but client references to representation objects can violate encapsulation.
Various notions of ownership confinement have been proposed for encapsulation of
objects. We have formalized one and shown that clients are independent from confined representations. Independence is formalized by an abstraction theorem that
licenses reasoning about equivalence of class implementations using simulation relations. Confinement is formalized by drawing boundaries that signify the absence
of pointers.
12.1 Related work
Representation independence. The main proof technique for representation independence is so fundamental that it has appeared in many places, with a variety of names, e.g., simulation, logical relations, abstraction mappings, relational
parametricity (e.g., [Plotkin 1973; Reynolds 1984; Lynch and Vaandrager 1995;
de Roever and Engelhardt 1998]). Among the many uses of simulations are program transformations and justification of logics for reasoning about data abstraction
and modification of encapsulated state.
Representation independence results are known for general transition systems [Milner 1971; Lynch and Vaandrager 1995], first order imperative languages [He et al.
1986; de Roever and Engelhardt 1998], higher order functional [Reynolds 1984;
Mitchell 1986; 1991; 1996; Power and Robinson 2000] and higher order imperative
languages [O’Hearn and Tennent 1995; Naumann 2002], and sequential objectoriented programs without heap allocation ([Cavalcanti and Naumann 2002] treats
a language with class-based visibility and [Reddy 1998] treats one with instancebased visibility). As far as we know, our results are the first for shared references
to mutable state, a ubiquitous feature in object-oriented and imperative programs.
(The lacuna is mentioned in [Grossman et al. 2000].)
A widely held view seems to be that classical techniques based on denotational
semantics and logical relations are inadequate in the face of the complex language
features of interest. The combination of local state with higher order procedures
makes it difficult to prove representation independence even for Algol, where procedures can be passed as arguments but not assigned to state variables [O’Hearn
and Tennent 1995]. Objects exhibit similar features.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

75

Difficulties with denotational semantics led to considerable advances using smallstep operational semantics [Gordon and Pitts 1998]. However, to get an adequate
induction hypothesis for an abstraction theorem, parametricity needs to be imposed
on the latent effects of procedure abstractions, either as a property to be proved or
as an intrinsic feature of the semantic model [Reynolds 1981b; O’Hearn and Tennent
1995]. These conditions are most easily expressed in terms of a denotational model,
but if procedures can be stored in the heap on which they act, difficult domain
equations must be solved.22 Recursive data types also lead to nontrivial domain
equations. Even if solutions can be found, they may be quite complex structures
that are difficult to understand and work with.
One of the most relevant works using operational semantics is that of Grossman
et al. [2000] where representation independence is approached using a dynamic notion of ownership by principals as in the security literature. To prove that clients
are independent from the representation of an abstraction provided by a host program, a wrapper construct is used to tag code fragments with their owner (e.g.,
client or “host”), and to provide an opaque type for the client’s view of the abstraction. This is a promising approach, but the results so far only show “independence
of evaluation”, which is analogous to the special case of simulation used for noninterference in analysis of information flow [Volpano et al. 1996; Abadi et al. 1999].
Although Grossman et al. [2000] offer their work as a simpler alternative to domain
theoretic semantics, the technical treatment is somewhat intricate by the time the
language is extended to include references, recursive and polymorphic types.
Except for parametric polymorphism, we treat all these features, as well as others
such as subclassing, dynamic binding, type tests and casts. Although Java syntax
seems less elegant than, say, lambda calculus, it has several features that ease
the difficulties. Owing to name-based type equivalence and subtyping, and the
binding of methods to objects via their class, we can use a denotational model with
quite simple domains and fixpoint definitions in the manner of Strachey [2000] (cf.
Sect. 3.1).
For applications in security and automated static checking, it is important to devise robust, comprehensible models that support not only the idealized languages of
research studies but also the full languages used in practice. Denotational semantics has conceptual advantages, at least if the domains are simple enough to have
a clear operational significance. However, we admit that our enthusiasm for the
efficacy of denotational techniques has been tempered by the irritation of flushing
out bugs in intricate definitions and induction hypotheses.
Our abstraction theorem and identity extension lemma can be used directly to
prove equivalence of programs, where a program is a command in the context of
a class table and designated class C. It would be reasonable to use a notion of
equivalence based on field visibility: states would be equated if they are equal after
hiding all fields except those visible in C. But this would beg the question whether
hiding imposes encapsulation that is not intrinsic to the language. In this paper we
use the finer equivalence on programs: for commands to be equivalent they must
22 Recently

Levy [2002] used functor categories to give a denotational model for a higher order
language with pointers, but the model does not capture relational parametricity and the language
has neither object-oriented features nor recursive types.
ACM Journal Name, Vol. V, No. N, Month 20YY.

76

·

A. Banerjee and D. Naumann

yield outcomes that are identical after garbage collection. Thus encapsulation is
formulated in terms of private fields and confined reps but the identity extension
lemma is expressed, in effect, in terms of local variable blocks (in the style of, e.g.,
He et al. [1986]).
Besides the “client interface” provided by public methods and analogous to the
interfaces studied in previous work on representation independence, a class also has
a “protected” interface to its subclasses. The combination of protected and public
interfaces is complicated, but a thorough treatment of representation independence
for object-oriented programs must take it into account. For reasoning about the
protected interface, work on behavioral subclassing has used simulations to connect
a class with its subclass [Liskov and Wing 1994; Leavens and Dhara 2000] but
a formal connection has not been made with the use of simulations to connect
alternative representations.
Confinement. Quite a few confinement disciplines have been proposed, by Hogg
[1991], Almeida [1997],Vitek and Bokowski [2001], Clarke et al. [2001], Müller and
Poetzsch-Heffter [2000], Boyland [2001], Lea [2000], Aldrich et al. [2002], and Clarke
[2001] (the latter has a more comprehensive recent survey). Most proposals have significant shortcomings; they disallow important design patterns or are not efficiently
checkable. Although the aim is to achieve encapsulation and thereby support modular reasoning in one form or another, few proposals have been formally justified
in these terms —none in terms of representation independence.
Several works justify a syntactic discipline by proving that it ensures a confinement invariant [Müller and Poetzsch-Heffter 2000; Clarke 2001; Aldrich et al. 2002].
Others go further and show some form of modular reasoning principle, as we discuss
in detail below. Existing justifications involve disparate techniques and objectives,
so that it is quite hard to assess and compare confinement disciplines. One of our
contributions is to show how standard semantic techniques can be used for such
assessments.
The fact that type names are semantically relevant lets us use them to formulate in semantic terms a condition similar to the ownership confinement notions
of Müller [2002], Clarke et al. [2001] and their predecessors [Hogg 1991; Almeida
1997]. Whereas several papers emphasize reachability via paths, our formulation
of confinement emphasizes partitioning of heap objects and the one-step points-to
relation. In this we were inspired by the work of Reynolds [2001] that shows the
efficacy of reasoning about partition blocks that may have dangling pointers.
Reasoning on the assumption of confinement is a separate concern from enforcement or checking of confinement. Semantic considerations led us to a flexible,
syntax-directed static analysis, but other analysis techniques such as model checking or theorem proving for (an approximation of) the semantic confinement property
could be interesting.
It is interesting to note that we get a strong reasoning principle on the basis
of ownership confinement alone, in a form that can be checked without program
annotations. By contrast, other works use annotations and combine ownership with
uniqueness and effects (e.g., read-only) [Clarke and Drossopoulou 2002; Aldrich
et al. 2002; Müller 2002].
Confinement figures heavily in the verification logics of Müller and PoetzschACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

77

Heffter [2000] and in some work by the group of Nelson and Leino [Leino and Nelson
2002; Detlefs et al. 1998] where it is needed for sound reasoning about the “modifies
clause” framing the scope of effects. Subsequent to the present work, Clarke and
Drossopoulou [2002] state results on reasoning about effects, using a confinement
discipline imposed using code annotations for confinement and effects. These works
are concerned with delimiting the scope of effects, which is an important aspect of
modular reasoning, but they do not address representation independence.
There has been much work on capturing encapsulation via visibility (lexical
scope), using existential types and subsumption (see [Bruce et al. 1999; Bruce 2002;
Pierce 2002] and references therein). None of these works addresses the problem of
confinement; they are concerned with the complex typing issues for object oriented
languages.
It is interesting to note that one of the main difficulties in designing safe and
flexible type systems is due to the desire to eliminate or minimize the use of type
testing and casting which are seen as loopholes that subvert type-based encapsulation. Indeed, parametric polymorphism has been much pursued as a means to cope
with generic patterns that, in current practice, are usually coded using subsumption, casts, and type Object (a recent reference is the textbook by Bruce [2002]).
Although parametric polymorphism has obvious merit, our results show that casts
and type tests are themselves relationally parametric. It is behavioral subclassing
which is at risk in some uses of casts and tests. This does not contradict [Reynolds
1984] because our language has a nominal type system [Pierce 2002]; it is the name
of a type, not its set of values, that is involved with tests and casts.
Our aim is to deal with the rich languages currently in use, rather than to advance
language design. It is challenging to formalize the syntax precisely yet perspicuously. Rather than devising our own idiosyncratic formalization, we adapted that
of Igarashi et al. [2001]. The details differ, as our language includes imperative
constructs and non-public scoping and their main concern is type soundness.
12.2 Future challenges
The language for which our results are given encompasses many important features of object oriented languages. Two major features are missing and will require
substantial additional work: concurrency and parametric polymorphism. The interaction between parametric and subtyping polymorphism is non-trivial and there
are a number of competing type systems. Some languages, e.g., C++, have parametric polymorphism but with significant limitations; for Java, parametric types
are a late addition. We expect to extend our work to them in the future.
Ownership confinement is appropriate for reasoning about many designs in practice and we have shown through a series of examples that our notion is applicable
to widely used designs such as the observer and factory patterns. Two important
issues are beyond the reach of our work (and much of the previous work on confinement). The first is multiple ownership. A canonical example is a collection
class with iterators. The reps for the collection are nodes of a data structure. The
collection object mediates additions and deletions. To allow enumeration of elements of the collection it is common to use iterator objects which need access to
the nodes of the data structure. Static analyses have been given that allow some
form of multiple owners [Clarke 2001; Müller 2002; Aldrich et al. 2002]. Although
ACM Journal Name, Vol. V, No. N, Month 20YY.

78

·

A. Banerjee and D. Naumann

our formalization of islands can be extended easily to encompass multiple owners,
it is not as clear how to extend the notion of simulation in a useful way. Our result
formalizes the notion that an owner instance provides an abstraction and this is
easily expressed in terms of the class construct. The generalization can perhaps be
expressed by grouping the related owners (e.g., the collection class and the iterator
class) in a module, but this is left for future work.
The other challenging issue for confinement is ownership transfer. Consider a
queue that owns objects representing tasks to be performed. For load balancing,
tasks may be moved from one queue to another. In this case a task is owned by
just one queue at a time and in a given state the system is confined according
to the definition in this paper. A sequential program for transferring ownership
from one queue might look as follows: q2.task := q1.task; q1.task := null. From a
confined initial state this need not lead to a confined final state: there could be other
references to task. But it does lead to a confined final state if q2.task is initially
the only existing reference to the task. Unique references have been extensively
studied so let us assume that a static analysis is given for uniqueness. Even with
uniqueness, our theory fails to apply, for two reasons. The first reason is a small
one: in the intermediate state two different owners reference the same task. This
problem is well known and can be surmounted: It is easy to add to our language an
atomic command with the effect of the above sequence [Minsky 1996] and to show,
given uniqueness, that it is confined. For practical purposes one would use a static
analysis to check that q1.task is a dead expression [Boyland 2001].
The second reason our theory does not apply is a technical one. To show that a
method call is confined, we need that the caller’s environment is confined in the final
heap assuming it was confined in the initial one. We get this by using a condition
stronger than confinement: from a confined state, a command or method yields
a final heap that extends the initial one in the sense of Def. 6.3. All commands
of our language yield heaps extended in this sense so all method meanings have
this property. (See the proof of Theorem 6.17.) But, by definition of extension,
h ✂ h0 says that reps that exist in h have the same owners in h0 as in h, disallowing
ownership transfer.
For static analysis there are some more modest issues worthy of investigation.
The simple conditions of Def. 6.9 ensure suitable confinement of the class table
but they are unnecessarily strong. Methods inherited into rep classes are not risky
if they do not leak self; such “anonymous methods” can be statically checked as
shown by Vitek and Bokowski [2001] and Grothoff et al. [2001] in work on modulebased confinement.23 The conditions of our static analysis may also admit useful
variations.
Having shown that simulation is sound one might proceed to study completeness.
It is not the case that our confinement conditions are necessary in general for
simulations to be preserved. A trivial simulation might depend on no confinement
at all. Also, a rep could be leaked but not exploited by any client. One can see
confinement as a kind of simulation which happens to be a rectangular predicate:
h relates to h′ just if h and h′ are confined, independent of each other. This
23 In

fact the cited work is concerned with pragmatic aspects of the analysis and does not formalize
a semantic property ensured by the analysis.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

79

suggests folding the confinement condition into the simulation relation, an idea
which is currently under study by Uday Reddy and Hongseok Yang for a Pascal-like
language.24 For practical reasoning the benefits of treating confinement separately
are clear: it accords with informal design practice, is amenable to static checking,
and ensures soundness for a straightforward and modular notion of coupling.
The more practical question is how to express basic couplings and prove the
simulation property for owner methods. To formalize the couplings for the observer examples one needs a formalism for inductive predicates on recursive data
structures; separation logic appears promising for this purpose [Reynolds 2002].
As we discussed in conjunction with Example 8.6, representation independence licenses reasoning about equivalence of programs that are structurally similar [Banerjee et al. 2001; Riecke 1993]. This is quite adequate for uses of simulations such as
static analyses and relating alternative interpretations for primitives, such as the
lazy and eager access control implementations for Java [Banerjee and Naumann
2002a]. But for abstraction in program development, typically called data refinement, it is not uncommon to consider significantly different program structures and
this calls for a full program logic in which something like the abstraction theorem
appears as a proof rule. For first-order imperative languages, several proof systems have been given for reasoning about two versions of an abstraction [de Roever
and Engelhardt 1998]. Typically, relations (especially “abstraction functions”) are
used to derive from one version the specification of the other version, which is then
proved correct in a program logic. Logics for imperative object-oriented languages
are at an early stage of development [Abadi and Leino 1997; Cavalcanti and Naumann 1999; Poetzsch-Heffter and Müller 1999; Huisman and Jacobs 2000; Huisman
2002; Reynolds 2002].
APPENDIX
A. ADDITIONAL PROOFS
Proof of Lemma 6.12
By cases on C and B. It suffices to consider C < B and to deal with confinement
of η in h.
—C ≤ Rep. Then the hypothesis of the Lemma is falsified because η self ∈
locs(Rep↓).
—C  Own ∧ C  Rep. Then B  Own ∧ B  Rep, so conf Cηh ⇔ conf B (h, η)
because both C and B are subject to condition (1) in Definition 6.4.
—C < B ≤ Own. Again, both B and C are subject to the same condition, here
(2) in Definition 6.4.
24 Their

aim is to explicate the semantic structure of languages involving heap storage Their
approach should lead to a lucid account on par with parametricity models for other languages [Reynolds 1984; 1981b; Reddy 1998]. They have defined a parametricity semantics for
a Pascal-like language [Reddy and Yang 2002] in which heap cells are tuples of pointers and integers rather than objects with scoped fields. Several challenges remain to be addresssed, if this
approach is to provide a foundation for reasoning about instance-based abstractions in Java-like
languages using a practical confinement discipline. For example, nominal types and class-based
visibility (which is not modelled by naive use of existential types).
ACM Journal Name, Vol. V, No. N, Month 20YY.

80

·

A. Banerjee and D. Naumann

—C ≤ Own < B. We have conf B (h, η) ⇒ conf C (h, η) by implication between
the consequents of (1) and (2) in Definition 6.4. The converse holds owing to
hypothesis rng η ∩ locs(Rep↓) = ∅.
Proof of Lemma 6.13
By cases on C. In the case C  Own ∧ C  Rep, we have conf C (h, η) ⇔
conf C (h0 , η) because Definition 6.4(1) of conf C is independent of the heap. For
the cases C ≤ Own and C ≤ Rep, we show conf C (h0 , η) using h ✂ h0 . First, by
definition of ✂ we have conf h0 . To show that η is confined in h0 for C, suppose
h = Ch ∗ Oh 1 ∗ Rh 1 ∗ . . . ∗ Oh k ∗ Rh k
is a confining partition of h. Let j be such that rng η ∩ locs(Own↓, Rep↓) ⊆
d om(Oh j ∗ Rh j ). Suppose, by h ✂ h0 , that this partition is extended by confining
partition h0 = Ch 0 ∗ Oh 01 ∗ Rh 01 ∗ . . .. In the case C ≤ Own, we have rng η ∩
locs(Rep↓) ⊆ d om(Rh j ) ⊆ d om(Rh 0j ), using conf C (h, η) and the definition ✂.
The case C ≤ Rep is similar.
Additional cases for Lemma 6.16
Case Γ ⊢ x := e. Here the heap is unchanged: h0 = h and the result holds by
reflexivity of ✂.
Case Γ ⊢ x := super.m(e). The same argument as for method call e.m.
Case Γ ⊢ S1 ; S2 . Let (η1 , h1 ) = [[Γ ⊢ S1 ]]µ(h, η). By induction on S1 we have
h ✂ h1 . By confinement of S1 we have conf C (h1 , η1 ). So we can use induction on
S2 to obtain h1 ✂ h0 and then h ✂ h0 by transitivity of ✂.
Case Γ ⊢ if e then S1 else S2 fi. By induction on S1 and S2 , using confinement
of S1 and S2 .
Case Γ ⊢ T x := e in S. Let η1 = [η | x 7→ [[Γ ⊢ e : U ]](h, η)]. By conf C (h, η) and
confinement of e we have conf C (h, η1 ). Then by induction on S, using confinement
of S, we get h ✂ h0 .
Proof of Lemma 7.3
By induction on depth. If C  Own then the equality is direct from Definition 7.1(1). If C ≤ Own then it is possible that CT (Own) declares m but
CT ′ (Own) does not (or vice versa). But in that case, by Definition 7.1(3) we
have mtype(m, C) = mtype′ (m, C) so m must be declared in a superclass, whence
depth(m, C) = 1 + depth(m, super C) = 1 + depth′ (m, super C) = depth′ (m, C).
Proof of Lemma 7.19
Let ΓB = (x : T , self : B) and ΓC = (x : T , self : C). To show
R (B, x, T → T ) (restr (d, B)) (restr(d′ , B))

(∗)

consider (h, η) ∈ [[Heap ⊗ ΓB ]] and (h′ , η ′ ) ∈ [[Heap ⊗ ΓB ]]′ such that conf B (h, η),
conf B (h′ , η ′ ), and R (Heap ⊗ ΓB ) (h, η) (h′ , η ′ ). By definition of restr we have
restr(d, B)(h, η) = d(h, η) and restr(d′ , B)(h′ , η ′ ) = d′ (h′ , η ′ ). So for (∗) it remains
to show
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

R (Heap ⊗ T )⊥ (d(h, η)) (d′ (h′ , η ′ ))

·

81

(†)

By Lemma 5.7(1) we have (h, η) ∈ [[Heap ⊗ ΓC ]] and (h′ , η ′ ) ∈ [[Heap ⊗ ΓC ]]′ . By
hypothesis, C is non-rep so B is also non-rep. As T is non-rep, we have rng η ∩
locs(Rep↓) = ∅ and rng η ′ ∩ locs(Rep′ ↓) = ∅. Thus Lemma 6.12 is applicable to
η, η ′ and using hypothesis B < C we obtain conf C (h, η), and conf C (h′ , η ′ ). Thus
we have established the antecedents needed to use hypothesis R (C, x, T → T ) d d′
to obtain (†).
Proof of Lemma 7.22
Case Γ ⊢ x : T . Then R T⊥ (ηx) (η ′ x) by R Γ η η ′ , so the result follows by
semantics of x : T .
Case Γ ⊢ null : B. Then semantics is nil and R B⊥ nil nil by definition of R.
Case Γ ⊢ it : unit. Similar to null, as are the cases true and false.
Case Γ ⊢ e1 = e2 : bool. Then, using identifiers from the semantic definition as
usual, we consider cases on d1 . If d1 = ⊥ then d′1 = ⊥ = d1 by induction on e1
and definition of R T . Hence, by semantics of e1 = e2 , [[Γ ⊢ e1 = e2 : bool]](h, η) =
[[Γ ⊢ e1 = e2 : bool]]′ (h′ , η ′ ) and thus
R bool⊥ ([[Γ ⊢ e1 = e2 : bool]](h, η)) ([[Γ ⊢ e1 = e2 : bool]]′ (h′ , η ′ ))

(∗)

The argument is symmetric for d2 = ⊥.
If none of d1 , d′1 , d2 , d′2 are ⊥ then, by induction on e1 we have R (T1 )⊥ d1 d′1 .
Thus, by Lemma 7.12, d1 = d′1 . Similarly, d2 = d′2 . Hence d1 = d2 iff d′1 = d′2 ,
whence the result (∗) holds by semantics.
Additional cases for Lemma 7.23
Case Γ ⊢ x := super.m(e).
By R Γ η η ′ we have R C ℓ ℓ′ , hence ℓ = ℓ′ by Lemma 7.12. By conf C (h, η) and
conf C (h′ , η ′ ) we have ℓ 6∈ locs(Rep↓) and ℓ 6∈ locs(Rep′ ↓). Let η1 = [self 7→ ℓ, x 7→
′
d] and η1′ = [self 7→ ℓ, x 7→ d ]. By confinement of x := super.m(e) (Definition 6.7)
we have confined arguments, i.e., conf (super C) (h, η1 ) and conf (super C) (h′ , η1′ )
′
By Lemma 7.22 for e, and considering the non-⊥ case, we have R U d d , whence,
′
by Lemma 7.13, R T d d . From R C ℓ ℓ′ we get R (super C) ℓ ℓ′ by Lemma 7.13,
and thus R [x : T , this : super C] η1 η1′ . From R MEnv µ µ′ we get
R (super C, mtype(m, super C)) (µ(super C)m) (µ′ (super C)m)
hence, as h, h′ , η1 , η1′ are confined and related, R (Heap ⊗ T ) (h1 , d1 ) (h′1 , d′1 ) where
(h1 , d1 ) = µ(super C)m(h, η) and (h′1 , d′1 ) = µ′ (super C)m(h′ , η ′ ). Thus R T d1 d′1
and R Heap h1 h′1 . It remains to show that the updated stores [η | x 7→ d1 ]
and [η ′ | x 7→ d′1 ] are related. This follows from R T d1 d′1 and T ≤ Γ x using
Lemma 7.13.
Case Γ ⊢ S1 ; S2 .
As usual, we consider the non-⊥ case. By induction on S1 we have R (Heap ⊗
Γ)⊥ (h1 , η1 ) (h′1 , η1′ ). Moreover, as S1 is a constituent of a method in CT and CT ′ ,
ACM Journal Name, Vol. V, No. N, Month 20YY.

82

·

A. Banerjee and D. Naumann

by confinement of S1 we have conf C (h1 , η1 ) and conf C (h′1 , η1′ ), so we can use
induction on S2 to obtain the result.
Case Γ ⊢ if e then S1 else S2 fi. Similar to case of sequence, but also using
Lemma 7.22 for e.
Case Γ ⊢ T x := e in S.
By Lemma 7.22 for e we have R U⊥ d d′ . If d = ⊥, then d′ = ⊥ and both
semantics yield ⊥. Otherwise, we have R T d d′ by the corollary to Lemma 7.12.
Thus, from R Γ η η ′ we obtain R (Γ, x : T ) η1 η1′ where η1 = [η | x 7→ d] and
η1′ = [η ′ | x 7→ d′ ] as in the semantic definition. In order to use induction on S, we
need to show conf C (h, η1 ) and conf C (h′ , η1′ ). From condition (1) in Definition 6.9
of confinement for CT , e is confined. In the case C  Own, confinement of e yields
d 6∈ locs(Rep↓). and thus conf C (h, η1 ). In the case C < Own, confinement of
e yields d ∈ locs(Rep↓) ⇒ d ∈ d om(Rh j ) for some partition and j with η self ∈
d om(Oh j ). This is the condition required for conf C (h, η1 ) in this case. Similarly,
we get conf C (h′ , η1′ ). Now, by induction on S we get that both semantics are ⊥
or else the result states from S satisfy R (Heap ⊗ Γ, x : T )⊥ (h1 , η2 ) (h′1 , η2′ ). In the
latter case, R (Heap ⊗ Γ) (h1 , (η2 ⇂ x)) (h′1 , (η2′ ⇂ x)) as required.
Proof of Lemma 11.3(2)
Again the proof proceeds by cases on C. In each case we show conf (super C) (h, η1 ),
noting that ℓ = (η self).
—C  Rep ∧ C  Own: By confinement of η at C, we have ℓ 6∈ locs(Rep↓).
Because e is confined at C, we have di 6∈ locs(Rep↓) for all di ∈ d. Thus
rng η1 ∩ locs(Rep↓) = ∅. And, since C < super C, we have conf (super C) (h, η1 )
by Lemma 6.12 and Definition 6.4(1).
—C ≤ Own: Choose a confining partition and let j be such that ℓ = (η self) ∈
d om(Oh j ). Since C < super C we have super C ≤ Own (Own < super C
is impossible by definition of super C). Because e is confined at C, we have
di ∈ locs(Rep↓) ⇒ di ∈ d om(Rh j ) for all di ∈ d. Thus rng η1 ∩ locs(Rep↓) ⊆
d om(Rh j ) proving conf (super C) (h, η1 ) by Definition 6.4(2).
—C ≤ Rep: Choose a confining partition and let j be such that ℓ = (η self) ∈
d om(Rh j ). Since C < super C we have super C ≤ Rep (Rep < super C is impossible by definition of super C). Because e is confined at C, we have di ∈
locs(Own↓, Rep↓) ⇒ di ∈ d om(Oh j ∗ Rh j ) for all di ∈ d. Thus rng η1 ∩
locs(Own↓, Rep↓) ⊆ d om(Oh j ∗ Rh j ) proving conf (super C) (h, η1 ) by Definition 6.4(3).
Additional cases for Lemma 11.4
Case Γ ✄ x : Γ x. Then d = η x. Confinement of x follows because the conditions
for d are exactly the same as the conditions for η and η is confined.
Cases Γ✄null : B, Γ✄true : bool, Γ✄false : bool, Γ✄it : unit, Γ✄e is B : bool.
For null the result holds since nil 6∈ Loc and for true, false, it, e is B the result
holds by Lemma 6.11.
Case Γ ✄ (B)e : B. Then d = ℓ and the result follows by induction on e for each
subcase of C.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

83

Proof of Lemma 11.5
First we show that h1 is confined, where we have the following cases on super C:
—super C = Object: then h1 = h. So conf h by hypothesis and h ✂ h1 by
reflexivity of ✂.
—super C < Object: as super C ≪ C, we can appeal to induction for super C to
obtain conf h1 and h ✂ h1 . Now by Lemma 6.13 we have conf C (h1 , η).
It remains to show conf h0 and h ✂ h0 . This is a consequence of a more general
Claim: For the given C, suppose self : C ⊢ S is a command with no method calls
and self : C ✄ S. Moreover, suppose that for any new B that occurs in S we have
B ⊏ C. Then self : C ⊢ S is confined.
Applying the claim to constr C, we get conf h0 . Then Lemma 6.14 applies, to
yield h1 ✂ h0 . So finally h ✂ h0 by transitivity.
The proof of the claim is by structural induction on S. The argument is the same
as the proof of Lemma 11.6, except that in the case of new that proof appeals to
Lemma 11.5 whereas here we appeal to the induction hypothesis. This use of
induction is sound because for any new B in the constructor, B ⊏ C and hence
B ≪ C.
Additional cases for Lemma 11.6
Case Γ✄x := e. Here h0 = h, hence confinement of h0 follows because conf C (h, η).
To show conf C (h0 , η0 ), we go by cases on C. First, as Γ ✄ e : T , by Lemma 11.4
we have e is confined. Choose a confining partition of h and let j be such that
η self ∈ d om(Oh j ). As x 6= self we have η self = η0 self.
—C  Rep ∧ C  Own: We must show rng η0 ∩ locs(Rep↓) = ∅, which follows
because d 6∈ locs(Rep↓) and because rng η ∩ locs(Rep↓) = ∅ by conf C (h, η).
—C ≤ Own: We must show rng η0 ∩locs(Rep↓) ⊆ d om(Rh j ), which follows because
{d} ∩ locs(Rep↓) ⊆ d om(Rh j ) by confinement of e at C and because rng η ∩
locs(Rep↓) ⊆ d om(Rh j ) by conf C (h, η).
—C ≤ Rep: We must show rng η0 ∩ locs(Own↓, Rep↓) ⊆ d om(Oh j ∗ Rh j ), which
follows because {d} ∩ locs(Own↓, Rep↓) ⊆ d om(Oh j ∗ Rh j ) by confinement of e
at C and because rng η ∩ locs(Own↓, Rep↓) ⊆ d om(Oh j ∗ Rh j ) by conf C (h, η).
Case Γ✄x := super.m(e). Here h0 = h1 and η0 = [η | x 7→ d1 ]. Because Γ✄e : U ,
by Lemma 11.4, e is confined at C. By Lemma 11.3 we have conf (super C) (h, η1 ).
Then by assumption conf µ we get conf (super C) (h0 , η1 ). Hence h0 is confined. To
show conf C (h0 , η0 ), we go by cases on C. Recall that ℓ = η self, and, as x 6= self,
ℓ = η0 self.
—C  Rep ∧ C  Own: As C < super C we have super C  Rep ∧ super C  Own.
By conf µ, d1 6∈ locs(Rep↓). Hence rng η0 ∩ locs(Rep↓) = ∅ by conf C (h, η).
—C ≤ Own: Let η self ∈ d om(Oh j ) for some j in the confining partition of h. As
C < super C we have either super C ≤ Own (Own < super C is impossible by
definition of super). By conf µ, d1 6∈ locs(Rep↓) and h ✂ h0 . Hence rng η0 ∩
locs(Rep↓) = rng η ∩ locs(Rep↓) ⊆ d om(Rh j ) by conf C (h, η). As h ✂ h0 ,
d om(Rh j ) ⊆ d om(Rh 0j ). That is, rng η0 ∩ locs(Rep↓) ⊆ d om(Rh 0j ).
ACM Journal Name, Vol. V, No. N, Month 20YY.

84

·

A. Banerjee and D. Naumann

—C ≤ Rep: Because loctype ℓ ≤ C, let ℓ ∈ d om(Rhj ) for some j in the confining
partition of h. As C < super C we have either super C ≤ Rep (Rep < super C
is impossible by definition of super). By conf µ, d1 ∈ locs(Own↓, Rep↓) ⇒ d1 ∈
d om(Oh 0j ∗ Rh 0j ) and h ✂ h0 . Hence rng η0 ∩ locs(Own↓, Rep↓) ⊆ d om(Oh 0j ∗
Rh 0j ) by conf C (h, η) and Definition 6.3.
Case Γ ✄ S1 ; S2 . By induction on S1 , h1 is confined and conf C (h1 , η1 ). Moreover, if S1 is a method call, it has confined argument values. Now by induction on
S2 , h2 is confined and conf C (h2 , η2 ). And, if S2 is a method call, it has confined
argument values. Hence all method calls in S1 ; S2 have confined argument values.
Case Γ✄if e then S1 else S2 fi. By Lemma 6.11, e is confined at C. If b = true,
result follows by induction on S1 and if b = false, result follows by induction on S2 .
Case Γ ✄ T x := e in S. Because Γ ✄ e : U we have by Lemma 11.4 that e is
confined at C. And, because x 6= self and conf C (h, η), we get conf C (h, η1 ). Since
Γ, x : T ✄ S, by induction on S we have conf C (h1 , η2 ) and all method calls in S
have confined argument values. Hence h1 is confined and conf C (h1 , η2 ⇂ x) and
all method calls in T x := e in S have confined argument values.
ACKNOWLEDGMENTS

Our work benefitted from discussions with a number of people as well as from
helpful feedback from the POPL referees. For particularly useful technical help
and encouragement we thank Torben Amtoft, Steve Bloom, Paulo Borba, Sophia
Drossopoulou, Nevin Heintze, Doug Lea, Peter Müller, Peter O’Hearn, Uday Reddy,
David Schmidt, and Hongseok Yang.
REFERENCES
Abadi, M., Banerjee, A., Heintze, N., and Riecke, J. G. 1999. A core calculus of dependency.
In ACM Symposium on Principles of Programming Languages (POPL). ACM Press, 147–160.
Abadi, M. and Cardelli, L. 1996. A Theory of Objects. Springer-Verlag.
Abadi, M. and Leino, K. R. M. 1997. A logic of object-oriented programs. In Theory and Practice
of Software Development (TAPSOFT). Springer-Verlag. Expanded in DEC SRC report 161.
Aldrich, J., Kostadinov, V., and Chambers, C. 2002. Alias annotations for program understanding. In ACM Symposium on Object Oriented Programming: Systems, Languages, and
Applications (OOPSLA). ACM Press.
Almeida, P. S. 1997. Balloon types: Controlling sharing of state in data types. In European
Conference on Object Oriented Programming (ECOOP). Lecture Notes in Computer Science.
Springer-Verlag, 32–59.
Arnold, K. and Gosling, J. 1998. The Java Programming Language, second edition. AddisonWesley.
Banerjee, A., Heintze, N., and Riecke, J. G. 2001. Design and correctness of program transformations based on control-flow analysis. In Intl. Symp. on Theoretical Aspects of Computer
Software (TACS). Lecture Notes in Computer Science. Springer-Verlag, 420–447.
Banerjee, A. and Naumann, D. A. 2002a. Representation independence, confinement and access
control. In ACM Symposium on Principles of Programming Languages (POPL). ACM Press,
166–177.
Banerjee, A. and Naumann, D. A. 2002b. Secure information flow and pointer confinement
in a Java-like language. In IEEE Computer Security Foundations Workshop (CSFW). IEEE
Computer Society Press, 253–270.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

85

Boyland, J. 2001. Alias burying: Unique variables without destructive reads. Software Practice
and Experience 31, 6.
Bruce, K. B. 2002. Foundations of Object-Oriented Programming Languages: Types and Semantics. MIT Press.
Bruce, K. B., Cardelli, L., and Pierce, B. C. 1999. Comparing object encodings. Information
and Computation 155, 1/2, 108–133.
Cavalcanti, A. L. C. and Naumann, D. A. 1999. A weakest precondition semantics for an
object-oriented language of refinement. In FM’99 - Formal Methods, Volume II. Number 1709
in Lecture Notes in Computer Science. Springer-Verlag, 1439–1459.
Cavalcanti, A. L. C. and Naumann, D. A. 2002. Forward simulation for data refinement of
classes. In Formal Methods Europe. Lecture Notes in Computer Science, vol. 2391. SpringerVerlag, 471–490.
Clarke, D. 2001. Object ownership and containment. Ph.D. thesis, University of New South
Wales, Australia.
Clarke, D. and Drossopoulou, S. 2002. Ownership, encapsulation and the disjointness of type
and effect. In ACM Symposium on Object Oriented Programming: Systems, Languages, and
Applications (OOPSLA). ACM Press.
Clarke, D. G., Noble, J., and Potter, J. M. 2001. Simple ownership types for object containment. In European Conference on Object Oriented Programming (ECOOP). Lecture Notes in
Computer Science. Springer-Verlag.
Cormen, T. H., Leiserson, C. E., and Rivest, R. L. 1990. Introduction to Algorithms. MIT
Press.
Cousot, P. and Cousot, R. 1977. Automatic synthesis of optimal invariant assertions: mathematical foundations. In Proceedings of the ACM Symposium on Artificial Intelligence and
Programming Languages, SIGPLAN Notices. Vol. 12. ACM Press, 1–12.
Dahl, O.-J. and Nygaard, K. 1966. Simula: an algol-based simulation language. Communications of the ACM 9, 9, 671–678.
Davey, B. and Priestley, H. 1990. Introduction to Lattices and Order. Cambridge University
Press.
de Roever, W.-P. and Engelhardt, K. 1998. Data Refinement: Model-Oriented Proof Methods
and their Comparison. Cambridge University Press.
Detlefs, D., Leino, K. R. M., and Nelson, G. 1998. Wrestling with rep exposure. Tech. Rep.
156, COMPAQ Systems Research Center. July.
Dhara, K. K. and Leavens, G. T. 1996. Forcing behavioral subtyping through specification
inheritance. In Proceedings of the 18th International Conference on Software Engineering.
IEEE Computer Society Press, 258–267.
Donahue, J. E. 1979. On the semantics of ”data type”. SIAM Journal of Computing 8, 4,
546–560.
Gamma, E., Helm, R., Johnson, R., and Vlissides, J. 1995. Design Patterns: Elements of
Reusable Object-Oriented Software. Addison-Wesley.
German, S. M., Clarke, E. M., and Halpern, J. Y. 1989. Reasoning about procedures as
parameters in the language L4. Information and Computation 83, 265–359.
Gong, L. 1999. Inside Java 2 Platform Security. Addison-Wesley.
Gordon, A. D. and Pitts, A. M., Eds. 1998. Higher Order Operational Techniques in Semantics.
Cambridge University Press.
Grossman, D., Morrisett, G., and Zdancewic, S. 2000. Syntactic type abstraction. ACM
Trans. Program. Lang. Syst. 22, 6.
Grothoff, C., Palsberg, J., and Vitek, J. 2001. Encapsulating objects with confined types.
In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications
(OOPSLA). ACM Press.
Haynes, C. T. 1984. A theory of data type representation independence. In International
Symposium on Semantics of Data Types, G. Kahn, D. B. MacQueen, and G. Plotkin, Eds.
Lecture Notes in Computer Science, vol. 173. Springer-Verlag, 157–175.
ACM Journal Name, Vol. V, No. N, Month 20YY.

86

·

A. Banerjee and D. Naumann

He, J., Hoare, C. A. R., and Sanders, J. 1986. Data refinement refined (resumé). In European
Symposium on Programming. Lecture Notes in Computer Science, vol. 213. Springer-Verlag.
Hoare, C. A. R. 1972. Proofs of correctness of data representations. Acta Inf. 1, 271–281.
Hogg, J. 1991. Islands: Aliasing protection in object-oriented languages. In ACM Symposium on
Object Oriented Programming: Systems, Languages, and Applications (OOPSLA). SIGPLAN
Notices, vol. 26. ACM Press.
Hogg, J., Lea, D., Wills, A., deChampeaux, D., and Holt, R. 1992. The Geneva Convention
on the treatment of object aliasing. OOPS Messenger 3, 2, 11–16.
Huisman, M. 2002. Verification of Java’s AbstractCollection class: A case study. Lecture Notes
in Computer Science, vol. 2386. Springer-Verlag, 175–194.
Huisman, M. and Jacobs, B. 2000. Java program verification via a Hoare logic with abrupt
termination. In FASE 2000. Lecture Notes in Computer Science. Springer-Verlag.
Igarashi, A., Pierce, B., and Wadler, P. 2001. Featherweight Java: A minimal core calculus
for Java and GJ. ACM Trans. Program. Lang. Syst. 23, 3 (May), 396–459.
Jones, C. B. 1986. Systematic software development using VDM. International Series in Computer Science. Prentice-Hall.
Lea, D. 2000. Concurrent Programming in Java, Second ed. Addison-Wesley.
Leavens, G. T. and Dhara, K. K. 2000. Concepts of behavioral subtyping and a sketch of their
extension to component-based systems. In Foundations of Component-Based Systems, G. T.
Leavens and M. Sitaraman, Eds. Cambridge University Press, Chapter 6, 113–135.
Leino, K. R. M. and Nelson, G. 2002. Data abstraction and information hiding. ACM Trans.
Program. Lang. Syst. 24, 5.
Levy, P. 2002. Possible world semantics for general storage in call-by-value. In Computer Science
Logic. Number 2471 in Lecture Notes in Computer Science. Springer-Verlag.
Liskov, B. and Guttag, J. 1986. Abstraction and Specification in Program Development. MIT
Press.
Liskov, B. H. and Wing, J. M. 1994. A behavioral notion of subtyping. ACM Trans. Program.
Lang. Syst. 16, 6.
Lynch, N. and Vaandrager, F. 1995. Forward and backward simulations part I: Untimed
systems. Information and Computation 121, 2.
Meyer, A. R. and Sieber, K. 1988. Towards fully abstract semantics for local variables: Preliminary report. In ACM Symposium on Principles of Programming Languages (POPL). ACM
Press, 191–203.
Milner, R. 1971. An algebraic definition of simulation between programs. In Proceedings of
Second Intl. Joint Conf. on Artificial Intelligence. 481–489.
Minsky, N. H. 1996. Towards alias-free pointers. In European Conference on Object Oriented
Programming (ECOOP). Lecture Notes in Computer Science, vol. 1098. 189–??
Mitchell, J. C. 1986. Representation independence and data abstraction. In ACM Symposium
on Principles of Programming Languages (POPL). ACM Press, 263–276.
Mitchell, J. C. 1991. On the equivalence of data representations. In Artificial Intelligence and
Mathematical Theory of Computation: Papers in Honor of John McCarthy, V. Lifschitz, Ed.
305–330.
Mitchell, J. C. 1996. Foundations for Programming Languages. MIT Press.
Moggi, E. 1991. Notions of computation and monads. Information and Computation 93, 55–92.
Morgan, C. and Gardiner, P. 1990. Data refinement by calculation. Acta Inf. 27, 481–503.
Müller, P. 2002. Modular Specification and Verification of Object-Oriented programs. Lecture
Notes in Computer Science, vol. 2262. Springer-Verlag.
Müller, P. and Poetzsch-Heffter, A. 2000. Modular specification and verification techniques
for object-oriented software components. In Foundations of Component-Based Systems, G. T.
Leavens and M. Sitaraman, Eds. Cambridge University Press.
Müller, P. and Poetzsch-Heffter, A. 2000. A type system for controlling representation
exposure in Java. In ECOOP Workshop on Formal Techniques for Java Programs. Technical
Report 269, Fernuniversität Hagen.
ACM Journal Name, Vol. V, No. N, Month 20YY.

March 26, 2018

·

87

Naumann, D. A. 2001. Predicate transformer semantics of a higher order imperative language
with record subtyping. Sci. Comput. Program. 41, 1, 1–51.
Naumann, D. A. 2002. Soundness of data refinement for a higher order imperative language.
Theor. Comput. Sci. 278, 1–2, 271–301.
O’Hearn, P. W. and Tennent, R. D. 1995. Parametricity and local variables. Journal of the
ACM 42, 3, 658–709.
O’Hearn, P. W. and Tennent, R. D. 1997. Algol-like Languages (Two volumes). Birkhäuser,
Boston.
Olderog, E.-R. 1983. Hoare’s logic for programs with procedures — what has been achieved? In
Proceedings, Logics of Programs, E. Clarke and D. Kozen, Eds. Number 164 in Lecture Notes
in Computer Science. Springer-Verlag.
Pierce, B. C. 2002. Types and Programming Languages. MIT Press.
Plotkin, G. 1973. Lambda definability and logical relations. Tech. Rep. SAI-RM-4, University
of Edinburgh, School of Artificial Intelligence.
Poetzsch-Heffter, A. and Müller, P. 1999. A programming logic for sequential Java. In
Programming Languages and Systems (ESOP), S. D. Swierstra, Ed. Lecture Notes in Computer
Science, vol. 1576. Springer-Verlag, 162–176.
Power, A. J. and Robinson, E. P. 2000. Logical relations and data abstraction. In Proceedings
of Computer Science Logic (CSL), P. Clote and H. Schwichtenberg, Eds. Lecture Notes in
Computer Science. Springer-Verlag, 497–511.
Reddy, U. S. 1998. Objects and classes in Algol-like languages. In Fifth Intern. Workshop on
Foundations of Object-oriented Languages. Full version to appear in Information and Computation.
Reddy, U. S. and Yang, H. 2002. Correctness of data representations involving heap data
structures. Presented at Pointerfest workshop, August, Queen Mary University of London.
Reynolds, J. C. 1972. Definitional interpreters for higher-order programming languages. In
Proceedings of 25th ACM National Conference. ACM Press, 717–740.
Reynolds, J. C. 1974. Towards a theory of type structure. In Colloques sur la Programmation,
LNCS 19. 408–425.
Reynolds, J. C. 1978. User-defined types and procedural data structures as complementary
approaches to data abstraction. In Programming Methodology, D. Gries, Ed. Springer-Verlag,
309–317.
Reynolds, J. C. 1981a. The Craft of Programming. Prentice-Hall.
Reynolds, J. C. 1981b. The essence of Algol. In Algorithmic Languages, J. W. de Bakker and
J. C. van Vliet, Eds. North-Holland.
Reynolds, J. C. 1984. Types, abstraction, and parametric polymorphism. In Information Processing ’83, R. Mason, Ed. North-Holland, 513–523.
Reynolds, J. C. 2001. Intuitionistic reasoning about shared mutable data structure. In Millenial
Perspectives in Computer Science. Palgrave.
Reynolds, J. C. 2002. Separation logic: a logic for shared mutable data structures. In IEEE
Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press.
Riecke, J. G. 1993. Fully abstract translations between functional languages. Mathematical
Structures in Computer Science 3, 4, 387–415.
Strachey, C. 2000. Fundamental concepts in programming languages. Higher Order and Symbolic Computation 13, 1. Originally appeared in 1967 Lecture notes, International Summer
School in Computer Programming, Copenhagen.
Vitek, J. and Bokowski, B. 2001. Confined types in Java. Software Practice and Experience 31, 6, 507–532.
Volpano, D., Smith, G., and Irvine, C. 1996. A sound type system for secure flow analysis.
Journal of Computer Security 4, 3, 167–187.
Wallach, D., Appel, A., and Felten, E. 2000. SAFKASI: a security mechanism for languagebased systems. ACM Transactions on Software Engineering and Methodology 9, 4.
ACM Journal Name, Vol. V, No. N, Month 20YY.

88

·

A. Banerjee and D. Naumann

Received Month Year; revised Month Year; accepted Month Year

ACM Journal Name, Vol. V, No. N, Month 20YY.

