Ownership types for object encapsulation.
Ownership types provide a statically enforceable way of specifying object encapsulation and enable local reasoning about program correctness in object-oriented languages. However, a type system that enforces strict object encapsulation is too constraining: it does not allow efficient implementation of important constructs like iterators. This paper argues that the right way to solve the problem is to allow objects of classes defined in the same module to have privileged access to each other's representations; we show how to do this for inner classes. This approach allows programmers to express constructs like iterators and yet supports local reasoning about the correctness of the classes, because a class and its inner classes together can be reasoned about as a module. The paper also sketches how we use our variant of ownership types to enable efficient software upgrades in persistent object stores.
Introduction
The ability to reason locally about program correctness is
crucial when dealing with large programs. Local reasoning
allows correctness to be dealt with one module at a time.
Each module has a specication that describes its expected
behavior. The goal is to prove that each module satises its
The research was supported in part by DARPA Contract
F30602-98-1-0237, NSF Grant IIS-98-02066, and NTT.
Permission to make digital or hard copies of all or part of this work for
personal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, to
republish, to post on servers or to redistribute to lists, requires prior specific
permission and/or a fee.
POPL'03, January 15-17, 2003, New Orleans, Louisiana, USA.
ACM 1-58113-628-5/03/0001 .$5.00
specication, using only the specications but not code of
other modules. This way the complexity of the proof eort
(formal or informal) can be kept under control.
This local reasoning approach is sound if separate verica-
tion of individual modules su-ces to ensure the correctness
of the composite program [43, 28]. The key to sound local
reasoning in object-oriented languages is object encap-
sulation. Consider, for example, a Stack object s that is
implemented using a linked list. Local reasoning about the
correctness of the Stack implementation is possible if objects
outside s do not directly access the list nodes, i.e., the list
nodes are encapsulated within the s.
This paper presents a variant of ownership types for specifying
and statically enforcing object encapsulation. With
ownership types, a program can declare that s owns all the
list nodes. The type system then statically ensures that the
list nodes are encapsulated within s.
A type system that enforces strict object encapsulation, how-
ever, is too constraining [55]: it does not allow e-cient implementation
of important constructs like iterators [48, 32].
Consider, for example, an iterator over the above-mentioned
Stack object s. If the iterator is encapsulated within s, it
cannot be used outside s. If the iterator is not encapsulated
within s, it cannot directly access the list nodes in s, and
hence cannot run e-ciently.
Previous ownership type systems were either too constraining
to support constructs like iterators [22, 21], or too permissive
to support local reasoning [20, 14, 11]; for example
they allowed objects outside the above-mentioned Stack object
s to temporarily get direct access to the list nodes.
This paper argues that the right way to solve the problem
is to provide special access privileges to objects belonging to
classes in the same module; we show how to do this for inner
classes [50, 38]. Our variant of ownership types allows inner
class objects to have privileged access to the representations
of the corresponding outer class objects. This principled violation
of encapsulation allows programmers to express constructs
like iterators using inner classes, yet supports local
reasoning about the correctness of the classes. Our system
supports local reasoning because a class and its inner classes
can be reasoned about together as a module.
The paper also describes how our variant of ownership types
enables e-cient software upgrades in persistent object stores.
Our interest in software upgrades led us to work on ownership
types. The paper shows how our ownership types can
be used to ensure that code for upgrading objects does not
observe broken invariants or interfaces unknown at the time
it was written; this makes it possible for programmers to
reason about the correctness of their upgrades.
This paper is organized as follows. Section 2 discusses object
encapsulation. Section 3 describes our variant of ownership
types for enforcing object encapsulation. Section 4 presents
a formal description of the type system. Section 5 shows how
ownership types can be used to enable modular upgrades.
Section 6 discusses related work and Section 7 concludes.
Object Encapsulation
Object encapsulation is important because it provides the
ability to reason locally about program correctness. Reasoning
about a class in an object-oriented program involves
reasoning about the behavior of objects belonging to the
class. Typically objects point to other subobjects, which are
used to represent the containing object.
Local reasoning about class correctness is possible if the sub-objects
are fully encapsulated, that is, if all subobjects are
accessible only within the containing object. This condition
supports local reasoning because it ensures that outside
objects cannot interact with the subobjects without calling
methods of the containing object. And therefore the containing
object is in control of its subobjects.
However, full encapsulation is often more than is needed.
Encapsulation is only required for subobjects that the containing
object depends on [43, 28]:
D1. An object x depends on subobject y if x calls methods
of y and furthermore these calls expose mutable
behavior of y in a way that aects the invariants of x.
Thus, a Stack object s implemented using a linked list depends
on the list but not on the items contained in the list.
If code outside could manipulate the list, it could invalidate
the correctness of the Stack implementation. But code outside
can safely use the items contained in s because s doesn't
call their methods; it only depends on the identities of the
items and the identities never change. Similarly, a Set of
immutable elements does not depend on the elements even
if it invokes a.equals(b) to ensure that no two elements a and
b in the Set are equal, because the elements are immutable.
Local reasoning about a class is possible if objects of that
class encapsulate every object they depend on. But strict
object encapsulation is too constraining [55]: it prevents efcient
implementation of important constructs like iterators.
For example, to run e-ciently, an iterator over the above-mentioned
Stack object s needs access to the list nodes in s.
To provide this access, we have to allow objects like iterators
to violate encapsulation.
Local reasoning is still possible provided all violations of encapsulation
are limited to code contained in the same mod-
ule. For example, if both the Stack and its iterator are imple-
O1. Every object has an owner.
O2. The owner can either be another object or world.
O3. The owner of an object does not change over time.
O4. The ownership relation forms a tree rooted at world.

Figure

1: Ownership Properties
world

Figure

2: An Ownership Relation
mented in the same module, we can still reason about their
correctness locally, by examining the code of that module.
3 Ownership Types for Encapsulation
Ownership types [22, 20, 14, 11] provide a statically enforceable
way of specifying object encapsulation. The idea is
that an object can own subobjects it depends on, thus preventing
them from being accessible outside. This section
presents our ownership type system. This system is similar
to the one described in [20]|the main dierence is that
to support constructs like iterators, the type system in [20]
allows temporary violations of encapsulation. We disallow
this violation. Instead, we support constructs like iterators
using inner classes.
The key to the type system is the concept of object owner-
ship. Every object has an owner. The owner can either be
another object or a special owner called world. Our type system
statically guarantees the ownership properties shown in

Figure

1. Figure 2 presents an example ownership relation.
We draw an arrow from x to y if x owns y. In the gure, the
special owner world owns objects o1, o5, and o6; o1 owns o2
and o4; o2 owns o3; and o6 owns o7.
Ownership allows a program to statically declare encapsulation
boundaries that capture dependencies:
D2. An object should own all the objects it depends on.
The system then enforces encapsulation: if y is inside the
encapsulation boundary of z and x is outside, then x cannot
access y. (An object x accesses an object y if x has a pointer
to y, or methods of x obtain a pointer to y.) In Figure 2, o7
is inside the encapsulation boundary of o6 and o1 is outside,
so o1 cannot access o7. An object is only allowed to access:
itself and objects it owns, 2) its ancestors in the ownership
tree and objects they own, and globally accessible objects,
namely objects owned by world. 1 Thus, o1 can access all
objects in the gure except for o3 and o7.
1 Note the analogy with nested procedures: proc P1 fvar x2 ;
class TStack<stackOwner, TOwner> {
{
6 new TNode<this, TOwner>(value, head);
9 T  pop() {
return value;
14 }16 class TNode<nodeOwner, TOwner> {
TNode<nodeOwner, TOwner> next; T  value;19 TNode(T  v, TNode<nodeOwner, TOwner> n) {
22 T  value() { return value; }
TNode<nodeOwner, TOwner> next() { return next; }
class T  { }28 class TStackClient  {
29 void test() {
new TStack<this, this> ();
new TStack<this, world>();
new TStack<world, world>();
new TStack<world, this> (); */
34 }}

Figure

3: Stack of T Objects
s1.head
s1.head.next
s2.head
s2.head.next
s3.head
s3.head.next
s1.head.value
s2.head.value
s1.head.next.value
s2.head.next.value
s3.head.next.value
s3.head.value
world

Figure

4: Ownership Relation for TStacks s1, s2, s3
3.1 Owner Polymorphism
We present our type system in the context of a Java-like
language augmented with ownership types. Every class definition
is parameterized with one or more owners. The rst
owner parameter is special: it identies the owner of the
corresponding object. The other owner parameters are used
to propagate ownership information. Parameterization allows
programmers to implement a generic class whose objects
have dierent owners. This parameterization is similar
to parametric polymorphism [54, 16, 1, 61] except that our
parameters are owners, not types.
An owner can be instantiated with this, with world, or with
another owner parameter. Objects owned by this are encapsulated
objects that cannot be accessed from outside.
Objects owned by world can be accessed from anywhere.
proc P2 fvar x3 ; proc P3 f.ggg. Say xn+1 and Pn+1 are
children of Pn . Pn can only access: 1) Pn and its children, 2)
the ancestors of Pn and their children, and global variables
and procedures.
class C<cOwner, sOwner, tOwner> where (sOwner <= tOwner) {
.
3 TStack<sOwner, tOwner> s;

Figure

5: Using Where Clauses to Constrain Owners

Figure

3 shows an example. 2 A TStack is a stack of T ob-
jects. It is implemented using a linked list. The TStack
class is parameterized by stackOwner and TOwner. stack-
Owner owns the TStack object; TOwner owns the T objects
contained in the TStack. The code species that the TStack
object owns the nodes in the list; therefore the list nodes
cannot be accessed from outside the TStack object.
The type of TStack s1 is instantiated using this for both
the owner parameters. This means that TStack s1 is owned
by the TStackClient object that created it and so are the T
objects in s1. TStack s2 is owned by the TStackClient object,
but the T objects in s2 are owned by world. TStack s3 is
owned by world and so are the T objects in s3. The ownership
relation for s1, s2, and s3 is depicted in Figure 4 (assuming
the stacks contain two elements dotted line
indicates that every object is directly or indirectly owned
by world.)
3.2 Constraints on Owners
For every type T hx1 ; :::; xni with multiple owners, our type
system statically enforces the constraint that (x1  x i ) for
f1::ng. Recall from Figure 1 that the ownership
relation forms a tree rooted at world. The notation (y  z)
means that y is a descendant of z in the ownership tree. The
notation (y  z) means that y is either the same as z, or y
is a descendant of z in the ownership tree. Thus, the type
of TStack s4 in Figure 3 is illegal because (world 6 this).
The above constraint is the same as in [20]. However, we
extend it to parameterized methods as well. For a method
of an object of type T hx1 ; :::; xni, the
restriction is that (x1  x i ) for all i 2 f1::kg. (These constraints
are needed to provide encapsulation in the presence
of subtyping. [11] illustrates this point with an example.)
To check ownership constraints modularly, it is sometimes
necessary for programmers to specify additional constraints
on class and method parameters. For example, in Figure 5,
the type of s is legal only if (sOwner  tOwner). We allow
programmers to specify such additional constraints using
where clauses [25, 54], and our type system enforces the
constraints. For example, in Figure 5, class C species that
(sOwner  tOwner). An instantiation of C that does not
satisfy the constraint is illegal.
3.3 Subtyping
The rule for declaring a subtype is that the rst owner parameter
of the supertype must be the same as that of the
subtype; in addition, of course, the supertype must satisfy
the constraints on owners. The rst owners have to match
2 The example shows type annotations written explicitly.
However, many of them can be automatically inferred. See
Section 4.3 for details.
class TStack<stackOwner, TOwner> {
3 .
4 TStackEnum<enumOwner, TOwner> elements
5 where (enumOwner <= TOwner) {
6 return new TStackEnum<enumOwner, TOwner>();
8 class TStackEnum<enumOwner, TOwner>
9 implements TEnumeration<enumOwner, TOwner> {11 TNode<TStack.this, TOwner> current;13 TStackEnum() { current = TStack.this.head; }15 T  getNext() {
(current == null) return null;
19 return t;
{
22 return (current != null);
class TStackClient  {
28 void test() {
29 TStack<this, world> new TStack<this, world>();
interface TEnumeration<enumOwner, TOwner> {
36 boolean hasMoreElements();

Figure

TStack With Iterator
because they are special, in that they own the corresponding
objects. Thus, TStackhstackOwner, TOwneri is a subtype
of ObjecthstackOwneri. But ThTOwneri is not a subtype of
Objecthworldi because the rst owners do not match.
3.4 Inner Classes
Our inner classes are similar to the member inner classes in
Java. Inner class denitions are nested inside other classes.

Figure

6 shows an example. The inner class TStackEnum
implements an iterator for TStack; the elements method of
TStack provides a way to create an iterator over the TStack.
The TStack code is otherwise similar to that in Figure 3.
Recall from before that an owner can be instantiated with
this, with world, or with another owner parameter. Within
an inner class, an owner can also be instantiated with C.this,
where C is an outer class. This feature allows an inner object
to access the objects encapsulated within its outer objects.
In

Figure

6, the owner of the current eld inTStackEnum is
instantiated with TStack.this. The current eld accesses list
nodes encapsulated within its outer TStack object.
An inner class is parameterized with owners just like a regular
class. In our system, the outer class parameters are
not automatically visible inside an inner class. If an inner
class uses an outer class parameter, it must explicitly include
the outer class parameter in its declaration. In Figure 6,
the TStackEnum declaration includes the owner parameter
TOwner from its outer class. TOwner is therefore visible
inside TStackEnum. But the TStackEnum declaration does
class TStack<stackOwner, TOwner> {
3 .
4 class TStackEnum<enumOwner, TOwner>
5 implements TEnumeration<enumOwner, TOwner> {7 TNode<TStack.this, TOwner> current;
8 .
9 T  getNext() writes(this) reads(TStack.this){.}
12 }14 interface TEnumeration<enumOwner, TOwner> {
boolean hasMoreElements() reads(this);

Figure

7: TStack Iterator With Eects
not include stackOwner. Therefore, stackOwner is not visible
inside TStackEnum.
Note that in this example, the elements method is parameterized
by enumOwner. This allows a program to create different
iterators that have dierent owners. elements returns
an iterator of type TStackEnumhenumOwner, TOwneri. For
this type to be legal, it must be the case that (enumOwner
TOwner). This requirement is captured in the where clause.
Note also that TStackhstackOwner, TOwneri.TStackEnum-
henumOwner, TOwneri is declared to be a subtype of TEnu-
merationhenumOwner, TOwneri. This allows TStackClient to
create an unencapsulated iterator e2 over an encapsulated
TStack s; the program can then pass e2 to objects outside
the TStackClient. In general, inner classes can be used to implement
wrappers [32] that expose a limited interface to an
outer object. A program can then create a wrapper around
an encapsulated subobject, and pass the wrapper object outside
the encapsulation boundary.
3.5 Encapsulation Theorem
Our system provides the following encapsulation property:
Theorem 1. x can access an object owned by
1.
2. x is an inner class object of o.
Proof. Consider the code: class Chf; :::if::: T ho; :::i y :::g.
Variable y of type T ho; :::i is declared within the static scope
of class C. Owner can therefore be either 1) this, or 2)
world, or 3) a formal class parameter, or 4) a formal method
parameter, or 5) C 0 .this, where C 0 is an outer class. We will
show that in the rst four cases, the constraint (this  o)
holds. In the rst two cases, the constraint holds trivially.
In the last two cases, (f  o) and (this  f ), so the constraint
holds. In the fth case, (C 0 Therefore an object x
of a class C can access an object y owned by
as in the rst four cases, or 2) x is an inner object
of o, as in the fth case.
class IntVector  {
3 int size() reads (this) { return elementCount; }
4 void add(int x) writes(this) { elementCount++; . }
5 .
6 }8 class IntStack  {
9 IntVector  new IntVector ();
{ vec.add(x); }
11 .

Figure

8: Reasoning About Aliasing and Side Eects
3.6 Discussion
Our variant of ownership types supports local reasoning provided
the programmer declares that all depended-on objects
are owned. The above theorem implies that owned objects
can only be accessed from inside the owner, and by inner ob-
jects. Therefore if ownership captures the depends relation
described in Section 2, local reasoning about the correctness
of a class is possible, because the class and its inner classes
together can be reasoned about as a module.
Our ownership types are also expressive. They allow ecient
implementation of constructs like iterators and wrappers
[32]. Furthermore, they also allow programs to create
wrappers that can be used in contexts where the underlying
object is inaccessible. This ability was illustrated in Figure 6;
iterator e2 can be used globally even though the TStack it
is iterating over can only be used in TStackClient.
Ours is the rst ownership type system to support constructs
like iterators and generally accessible wrappers while also ensuring
local reasoning. We discuss this further in Section 6.
3.7 Eects Clauses
Our system also contains eects clauses [49] because they
are useful for specifying assumptions that hold at method
boundaries and enable modular reasoning and checking of
programs. We use eects with ownership types to enable
modular upgrades; we describe this in Section 5.
Our system allows programmers to specify reads and writes
clauses. Consider a method that species that it writes
wn ) and reads (r1 ; :::; rm ). The method can write
an object x (or call methods that write x) only if
for some i 2 f1::ng. The method can read an object y (or
call methods that read y) only if (y  w i ) or (y  r j ), for
some f1::mg. We thus allow a method to
both read and write objects named in its writes clause.

Figure

7 shows a TStack iterator that uses eects, but is
otherwise similar to the TStack iterator in Figure 6. In the
example, the hasMoreElements method reads the this object.
The getNext method reads objects owned by TStack.this and
writes (and reads) the this object.
defn ::= class cnhformal+i extends c where constr* body
body ::= finnerclass* eld* meth*g
owner ::= formal j world j cn.this
constr ::= (owner  owner) j (owner 6 owner)
innerclass ::= defn
meth ::= t mnhformal*i(arg* ) eects where constr* feg
eects ::= reads (owner* ) writes (owner* )
eld ::= t fd
formal ::= f
e ::= new c j x.new c j x j let (arg=e) in feg j
class names
eld names
method names
x,y 2 variable names

Figure

9: Grammar
When eects clauses are used in conjunction with subtyping,
the eects of an overridden method must subsume the eects
of the overriding method. This sometimes makes it di-cult
to specify precisely all the eects of a method. For example,
it is di-cult to specify precisely all the read eects in the
getNext method of the TEnumeration class because TEnumer-
ation is expected to be a supertype of subtypes like TStack-
Enum and TEnumeration cannot name the specic objects
used in the getNext methods of these subtypes. To accommodate
such cases, we allow an escape mechanism, where a
method can include world in its eects clauses.
Ownership types and eects can be used to locally reason
about the side eects of method calls. Consider, for example,
the code in Figure 8, which shows an IntStack implemented
using an IntVector vec. (We adopted this example from [44].)
The example has a method m that receives two arguments:
an IntStack s and an IntVector v. The condition in the assert
statement in m can be true only if v is not aliased to s.vec.
In the example, the method m uses a where clause to specify
that (v 6 s) and (s 6 v). Since the ownership relation forms
a tree (see Figure 1), this constraint implies that v cannot be
aliased to s.vec. Furthermore, IntVector.size declares that it
only reads objects owned by the IntVector, and IntStack.push
declares that it only writes (and reads) objects owned by
the IntStack. Therefore, it is possible to reason locally that
v.size and s.push cannot interfere, and thus the condition in
the assert statement in m must be true.
4 The Type System
This section presents a formal description of our type system.
To simplify the presentation of key ideas, we describe our
type system in the context of a core subset of Java [33] known
as Classic Java [31]. We add inner classes to Classic Java
and augment its type system with ownership types. Our
approach, however, extends to the whole of Java and other
similar languages.
4.1 Type Checking

Figure

9 presents our grammar. The core of our type system
is a set of rules for reasoning about the typing judgment:
FieldsOnce(P)
class cnhf1::n i extends c 0 where constr ficlass eld methg 2 c
[CONSTR ENV]
[OWNER WORLD]
world
[OWNER FORMAL]
[OWNER THIS]
class cnhf1::n i. where constr . 2 cnhfi
6 9x;y
[METHOD DECLARED]
class cnhf1::n i. f. meth .g 2 c
[METHOD INHERITED]
[FIELD DECLARED]
class cnhf1::n i. f. eld .g 2 c
[FIELD INHERITED]
eld
world
[EXP REF ASSIGN]

Figure

10: Type Checking Rules
Judgment Meaning
defn is a well-formed class in class c
is an owner
constraint constr is satised
eect X is subsumed by eect Y
is a well-formed type
a subtype of t 2
typing environment E is well-formed
class c declares/inherits eld
class c declares/inherits meth
eld eld is a well-formed eld
meth meth is a well-formed method
eects of e are subsumed by R/W

Figure

Typing Judgments
t. P , the program being checked, is included
here to provide information about class denitions.
E is an environment providing types for the free variables
of e. R and W must subsume the read and write eects
of e. t is the type of e. We dene a typing environment
as
as R, W ::= o1::n . We dene the type system using the
judgments in Figure 11. We present the rules for these judgments
in Figure 10. The rules use a number of predicates
that are shown in Figure 12. These predicates are based on
similar predicates from [31]. For simplicity, we sometimes
treat outermost classes in our rules as if they were inner
classes of class ;. We also sometime use cnhfi to denote
4.2 Soundness of the Type System
Our type checking rules ensure that for a program to be
well-typed, the program respects the properties described in

Figure

1. A complete syntactic proof [63] of type soundness
can be constructed by dening an operational semantics (by
extending the operational semantics of Classic Java [31]) and
then proving that well-typed programs do not reach an error
state and that the generalized subject reduction theorem
holds for well-typed programs. The subject reduction theorem
states that the semantic interpretation of a term's type
is invariant under reduction. The proof is straightforward
but tedious, so it is omitted here.
4.3 Type Inference
Although our type system is explicitly typed in principle, it
would be onerous to fully annotate every method with the
extra type information. Instead, we can use a combination
of inference and well-chosen defaults to signicantly reduce
the number of annotations needed in practice. [14, 11] describe
an intraprocedural type inference algorithm and some
default types; we can use a similar approach. (In [14, 11],
about one in thirty lines of code had to be changed to express
Java programs in an ownership type system.) We emphasize
that this approach to inference is purely intraprocedural and
does not infer method signatures or types of instance vari-
ables. Rather, it uses a default completion of partial type
specications in those cases to minimize the required anno-
tations. This approach permits separate compilation.
Meaning
WFClasses(P) There are no cycles in the class hierarchy
declared twice in P
contains two inner classes with
same name, either declared or inherited
FieldsOnce(P) No class contains two elds with same
name, either declared or inherited
contains two methods with
same name
Overriding methods have the same return
type and parameter types as the methods
being overridden. The read and write
eects of an overriding method must be
superseded by those of the overridden
methods

Figure

12: Predicates Used in Type Checking Rules
4.4 Runtime Overhead
The system we described is a purely static type system.
The ownership relations are used only for compile-time type
checking and are not preserved at runtime. Consequently,
our programs have no runtime overhead compared to regular
(Java) programs. In fact, one way to compile and run a program
in our system is to convert it into a regular program
after type checking, by removing the owner parameters, the
constraints on owners, and the eects clauses.
A language like Java, however, is not purely statically-typed.
Java allows downcasts that are checked at runtime. Suppose
an object with declared type Objecthoi is downcast to
Vectorho,ei. Since the result of this operation depends on information
that is only available at runtime, our type checker
cannot verify at compile-time that e is the right owner parameter
even if we assume that the object is indeed a Vec-
tor. To safely support downcasts, a system has to keep some
ownership information at runtime. This is similar to keeping
runtime information with parameterized types [54, 61]. [10]
describes how to do this e-ciently for ownership by keeping
runtime information only for objects that can be potentially
involved in downcasts into types with multiple parameters.
5 Upgrades in Persistent Object Stores
This section shows how ownership types and eects clauses
can be used to enable modular reasoning about the correctness
of upgrades in a persistent object store. The desire to
achieve such reasoning was the motivation for our work on
ownership types for encapsulation.
A persistent object store [46, 5, 9, 17, 18, 29, 56] contains
conventional objects similar to what one might nd in an
object-oriented language such as Java. Applications access
persistent objects within atomic transactions, since this is
necessary to ensure consistency for the stored objects; transactions
allow for concurrent access and they mask failures.
Upgrades are needed in such a system to improve object
implementations, to correct errors, or even to change interfaces
in the face of changing application requirements; this
includes incompatible changes to interfaces where the new
interface does not support the same methods as the old one.
Providing a satisfactory solution for upgrades in persistent
object stores has been a long-standing challenge.
An upgrade for a persistent object store is dened as a set
of class-upgrades, one for each class whose objects need to
change. A class-upgrade is a triple: hold-class, new-class,
TFi. It indicates that all objects belonging to old-class
should be transformed, through the use of the transform
function TF provided by the programmer, into objects of
new-class. TF takes an old-class object and a newly allocated
new-class object and initializes the new-class object
from the old-class object. The upgrade infrastructure causes
the new-class object to take over the identity of the old-class
object, so that all objects that used to point to the old-class
object now point to the new-class object.
An upgrade is executed by transforming all objects whose
classes are being replaced. However, transforms must not
interfere with application access to the store, and must be
performed e-ciently in both space and time. In addition,
they must be done safely so that important persistent state
is not corrupted. Previous approaches [4, 7, 29, 45, 56, 57]
do not provide a satisfactory solution to these challenges;
they either stop application access to the database while
running the upgrade, or they keep copies of the database, or
they limit the expressive power of transforms (e.g., transform
functions are not allowed to make method calls).
Our system provides an e-cient solution. It performs upgrades
lazily. An object is transformed just before an application
accesses it: the application transaction is interrupted
to run the transform function. The transform runs in its
own transaction; when this transaction commits, the application
transaction is resumed. Our system also allows later
upgrades to run in parallel with earlier ones. If an object has
several pending transforms, they are run one after another,
in upgrade order. Furthermore, if a transform transaction
T encounters an object with a pending transform from an
upgrade, T is interrupted (just like an application
to run the pending transform, and continues execution
after the pending transform commits.
More details can be found in [13, 12, 47].
5.1 Ownership Types for Safe Upgrades
Our upgrade system is e-cient and expressive: it does not
delay application transactions, avoids the use of versions
(copies of objects), and does not limit the expressive power
of transform functions. But it also needs to support modular
reasoning about the correctness of transform functions.
This is possible if each transform function encounters only
object interfaces and invariants that existed when its upgrade
started, even though in reality the transform function
might run much later, after application transactions
and other transform transactions.
We use our variant of ownership types to enable modular
reasoning about the correctness of transform functions. Our
system checks statically whether transform functions satisfy
the following constraint, using ownership and eects declarations
(eects clauses state what objects TFs access):
S1. TF(x) only accesses objects that x owns (directly or
transitively).
Transform functions often satisfy S1 because ownership frequently
captures the depends relation discussed in Section 2,
and typically transform functions only access the depended-
on objects. (We discuss in [13] how we support modular
reasoning of transform functions when S1 does not hold.)
Our implementation also ensures the following:
S2. For any object x aected by an upgrade, x is accessed
before any object owned by x.
We ensure S2 using two mechanisms. If the owned object is
encapsulated within x, the type system guarantees that x is
accessed rst. If the owned object is shared with an inner
class object of x, our system causes x to be accessed just
before the inner class object is rst used after the upgrade.
This latter mechanism is described in more detail in [13].
When S1 holds, we can prove that out-or-order processing
of transforms does not cause problems. In particular, we
can show that: applications do not interfere with transform
functions, transform functions of unrelated objects do not
interfere with each other, and transform functions of related
objects run in a pre-determined order (namely an object is
transformed before its owned subobjects). (The proofs are
given in [13]).
Thus when S1 holds, we can ensure that transform functions
encounter the expected interfaces and invariants. This supports
modular reasoning: each transform function can be
reasoned about as extra method of its old class.
6 Related Work
Euclid [41] is one of the rst languages that considered the
problem of aliasing. [37] stressed the need for better treatment
of aliasing in object-oriented programs. Early work on
Islands [36] and Balloons [3] focused on fully encapsulated
objects where all subobjects an object can access are not accessible
outside the object. Universes [53] also enforces full
encapsulation, except for read-only references. However, full
encapsulation signicantly limits expressiveness, and is often
more than is needed. The work on ESC/Java pointed out
that encapsulation is required only for subobjects that the
containing object depends on [43, 28], but ESC/Java was
unable to always enforce encapsulation.
6.1 Ownership Types and Encapsulation
Ownership types provide a statically enforceable way of specifying
object encapsulation. They were proposed in [22] and
formalized in [21]. These systems enforce strict object en-
capsulation, but do so by signicantly limiting expressive-
ness. They require that a subtype have the same owners
as a supertype. So TStackhstackOwner, TOwneri cannot be
a subtype of ObjecthstackOwneri. Moreover, they do not
support iterators.
PRFJ [14], SCJ [11], and JOE [20] extended ownership types
to support a natural form of subtyping. To do so without
violating encapsulation, JOE introduces the constraint that
in every type with multiple owners, the rst owner  all
other owners. As a result, in JOE, a program can create a
pointer from object x to an object owned by
o). PRFJ and SCJ allow an object to contain pointers to
subobjects owned by a dierent object, but they have eects
clauses that prevent a program from following such point-
ers. The above systems eectively enforce encapsulation for
object elds. However, to support constructs like iterators,
they allow method local variables to violate encapsulation.
Therefore they do not support local reasoning.
AliasJava [2] uses ownership types to aid program under-
standing. Like other ownership type systems, AliasJava allows
programmers to use ownership information to reason
about aliasing. AliasJava is also more
exible than other
ownership type systems. However, unlike other ownership
type systems, AliasJava does not enforce any encapsulation
properties. (This is illustrated with an example in [11].)
Ownership types have been extended to inner classes in [19,
2]. However, these systems do not enforce the property
stated in Section 3.5, and do not support local reasoning.
Ownership types have also been used to enforce other prop-
erties. Parameterized Race-Free Java (PRFJ) [14] uses an
based type system to prevent data races in multi-threaded
programs. Safe Concurrent Java (SCJ) [11] extends
this to prevent both data races and deadlocks. These systems
can be combined with our approach to enforce object
encapsulation as well as prevent data races and deadlocks.
[11] sketches a way of doing this.
Recent work [15, 59] combines region types [60, 24, 35] with
our type system to statically ensure both object encapsulation
and safe region-based memory management.
6.2 Related Type Systems
Linear types [62] and unique pointers [51] can also be used
to control object aliasing. Linear types have been used in
low level languages to support safe explicit memory deallocation
[24] and to track resource usage [26, 27]. Linear types
and unique pointers are orthogonal to ownership types, but
the two can be used in conjunction to provide more expressive
systems. PRFJ [14] is the rst system that combines
ownership types with conventional unique pointers. Recent
work [23] proposes a better approach that allows a program
to specify a unique external pointer to an object; there can
be other internal pointers to the object from its subobjects.
Eects clauses [49] are useful for specifying assumptions that
must hold at method boundaries. Eects enable modular
checking of programs. PRFJ [14] is the rst system to combine
eects with ownership types to statically prevent data
races. [11] and [20] also combine eects with ownership for
preventing deadlocks and for program understanding. This
paper uses eects with ownership to enable lazy upgrades.
Data groups [42, 44] can be used to name groups of objects in
an eects clause to write modular specications in the presence
of subtyping. Ownership types provide an alternate
way of writing modular specications. Ownership types can
also be used to name groups of objects in an eects clause|
the name of an owner can be used to name all the objects
transitively owned by the owner. Figure 8 presents an example
from [44] expressed using ownership types. Data groups
are implemented using a theorem prover, and in principle,
they can be very
exible. However, pivot uniqueness in [44]
imposes drastic restrictions on pivot elds. Ownership types
do not impose such restrictions; they only require that the
owner of an object be unique. In [44], the owner exclusion
constraint is hard coded. In our system, programmers can
specify arbitrary constraints on owners using where clauses;
owner exclusion can be used as a default.
Systems such as TVLA [58], PALE [52], and Roles [40] specify
the shape of a local object graph in more detail than
ownership types. TVLA can verify properties such as when
the input to the program is a tree, the output is also a
tree. PALE can verify all the data structures that can be
expressed as graph types [39]. Roles can verify global properties
such as the participation of objects in multiple data
structures. Roles also support compositional interprocedural
analysis. In contrast to these systems that take exponential
time for verication, ownership types provide a lightweight
and practical way to constrain aliasing.
Conclusions
Object encapsulation enables sound local reasoning about
program correctness in object-oriented languages. Ownership
types provide a way of specifying and statically enforcing
object encapsulation. However, a type system that
enforces strict object encapsulation is too constraining: it
does not allow e-cient implementation of important constructs
like iterators.
This paper argues that the right way to solve the problem
is to allow objects of classes dened in the same module to
have privileged access to each other's representations. We
show how to do this for inner classes. Our variant of ownership
types allows objects of inner classes to have privileged
access to the representations of the corresponding objects
of outer classes. This principled violation of encapsulation
allows programmers to express constructs like iterators and
wrappers using inner classes. Our system also allows wrappers
to be used in more global contexts than the objects
they wrap. Yet our system supports local reasoning about
the correctness of classes, because a class and its inner classes
can be reasoned about together as a module.
Thus the paper describes the rst ownership type system
that is expressive enough to support iterators and wrappers,
while also supporting local reasoning. In addition, the paper
describes an application of the technique to enable modular
reasoning about upgrades in persistent object stores.
Ownership types have been used for other purposes as well,
such as for preventing data races and deadlocks, and for safe
region-based memory management. Since ownership types
require little programming overhead, their type checking is
fast and scalable, and they provide several benets, they
oer a promising approach to making object-oriented programs
more reliable.

Acknowledgments

We thank Daniel Jackson, Viktor Kuncak, Greg Nelson,
Martin Rinard, and Alexandru Salcianu for useful discussions
and comments on earlier drafts of this paper.



--R

Adding type parameterization to the Java language.
Alias annotations for program understanding.
Balloon types: Controlling sharing of state in data types.
Scalable and recoverable implementation of object evolution for the PJama 1 platform.
Design issues for persistent Java: A type-safe
Representation independence
Semantics and implementation of schema evolution in object-oriented databases

JPS: A distributed persistent Java system.
Safe runtime downcasts with ownership types.
Ownership types for safe programming: Preventing data races and deadlocks.
Ownership types and safe lazy upgrades in object-oriented databases
Lazy modular upgrades in persistent object stores.
A parameterized type system for race-free Java programs

Making the future safe for the past: Adding genericity to the Java programming language.
The GemStone data management system.
Shoring up persistent applications.
Object ownership and containment.
Ownership, encapsulation and disjointness of type and e
Simple ownership types for object containment.
Ownership types for exible alias protection.
External uniqueness.
Typed memory management in a calculus of capabilities.
Subtypes vs. where clauses: Constraining parametric polymorphism.
Enforcing high-level protocols in low-level software
Adoption and focus: Practical linear types for imperative programming.
Wrestling with rep exposure.
The story of O2.

Classes and mixins.
Design Patterns: Elements of Reusable Object-Oriented Software
The Java Language Speci
An object-oriented eects system

Islands: Aliasing protection in object-oriented languages
The Geneva convention on the treatment of object aliasing.

Graph types.
Role analysis.
Report on the programming language Euclid.
Data groups: Specifying the modi
Data abstraction and information hiding.

Beyond schema evolution to database reorganization.
Providing persistent objects in distributed systems.
Safe lazy software upgrades in object-oriented databases



Towards alias-free pointers
The pointer assertion logic engine.

Parameterized types for Java.
Iterators and encapsulation.
Object Design Inc.
Class modi
Solving shape-analysis problems in languages with destructive updating


Parametric polymorphism in Java: An approach to translation based on re ective features.
Linear types can change the world.
A syntactic approach to type soundness.
--TR
Semantics and implementation of schema evolution in object-oriented databases
Class modification in the GemStone object-oriented DBMS
The GemMYAMPERSANDndash;Stone data management system
Polymorphic effect systems
Beyond schema evolution to database reorganization
Islands
Graph types
Design patterns
A syntactic approach to type soundness
Shoring up persistent applications
Subtypes vs. where clauses
Region-based memory management
Parameterized types for Java
Adding type parameterization to the Java language
Classes and mixins
Solving shape-analysis problems in languages with destructive updating
Ownership types for flexible alias protection
Data groups
Making the future safe for the past
Typed memory management in a calculus of capabilities
Confined types
Type-based race detection for Java
Parametric polymorphism in Java
Abstraction mechanisms in CLU
Enforcing high-level protocols in low-level software
The pointer assertion logic engine
Role analysis
Representation independence, confinement and access control [extended abstract]
A parameterized type system for race-free Java programs
Adoption and focus
Using data groups to specify and check side effects
Region-based memory management in cyclone
The Java Language Specification
Ownership types for safe programming
Ownership, encapsulation and the disjointness of type and effect
Alias annotations for program understanding
The Story of O2
An Object-Oriented Effects System
Providing Persistent Objects in Distributed Systems
Simple Ownership Types for Object Containment
Scalable and Recoverable Implementation of Object Evolution for the PJama1 Platform
Towards Alias-Free Pointers
Iterators and Encapsulation

--CTR
Pradeep Kumar, Modal logic & ownership types: uniting three worlds, Companion to the 21st ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
David L. Heine , Monica S. Lam, A practical flow-sensitive and context-sensitive C and C++ memory leak detector, ACM SIGPLAN Notices, v.38 n.5, May
Ana Milanova, Precise identification of composition relationships for UML class diagrams, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
Alex Potanin , James Noble , Robert Biddle, Generic ownership: practical ownership control in programming languages, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA
Yin Liu , Ana Milanova, Ownership and Immutability Inference for UML-Based Object Access Control, Proceedings of the 29th International Conference on Software Engineering, p.323-332, May 20-26, 2007
Alex Potanin , James Noble , Dave Clarke , Robert Biddle, Featherweight generic confinement, Journal of Functional Programming, v.16 n.6, p.793-811, November 2006
Adrian Birka , Michael D. Ernst, A practical type system and language for reference immutability, ACM SIGPLAN Notices, v.39 n.10, October 2004
Protecting representation with effect encapsulation, ACM SIGPLAN Notices, v.41 n.1, p.359-371, January 2006
Ana Milanova, Composition inference for UML class diagrams, Automated Software Engineering, v.14 n.2, p.179-213, June      2007
Matthew S. Tschantz , Michael D. Ernst, Javari: adding reference immutability to Java, ACM SIGPLAN Notices, v.40 n.10, October 2005
Pratibha Permandla , Michael Roberson , Chandrasekhar Boyapati, A type system for preventing data races and deadlocks in the java virtual machine language: 1, ACM SIGPLAN Notices, v.42 n.7, July 2007
Yu David Liu , Scott F. Smith, Interaction-based programming with classages, ACM SIGPLAN Notices, v.40 n.10, October 2005
Wei-Ngan Chin , Florin Craciun , Shengchao Qin , Martin Rinard, Region inference for an object-oriented language, ACM SIGPLAN Notices, v.39 n.6, May 2004
Nathanael Schrli , Andrew P. Black , Stphane Ducasse, Object-oriented encapsulation for dynamically typed languages, ACM SIGPLAN Notices, v.39 n.10, October 2004
Derek Rayside , Lucy Mendel , Daniel Jackson, A dynamic analysis for revealing object ownership and sharing, Proceedings of the 2006 international workshop on Dynamic systems analysis, May 23-23, 2006, Shanghai, China
Tian Zhao , Jens Palsberg , Jan Vitek, Type-based confinement, Journal of Functional Programming, v.16 n.1, p.83-128, January 2006
Alex Potanin , James Noble , Dave Clarke , Robert Biddle, Generic ownership for generic Java, ACM SIGPLAN Notices, v.41 n.10, October 2006
Chandrasekhar Boyapati , Alexandru Salcianu , William Beebee, Jr. , Martin Rinard, Ownership types for safe region-based memory management in real-time Java, ACM SIGPLAN Notices, v.38 n.5, May
David A. Naumann, Observational purity and encapsulation, Theoretical Computer Science, v.376 n.3, p.205-224, May, 2007
Chandrasekhar Boyapati , Barbara Liskov , Liuba Shrira , Chuang-Hue Moh , Steven Richman, Lazy modular upgrades in persistent object stores, ACM SIGPLAN Notices, v.38 n.11, November
David A. Naumann , Mike Barnett, Towards imperative modules: reasoning about invariants and sharing of mutable state, Theoretical Computer Science, v.365 n.1, p.143-168, 10 November 2006
Peter Mller , Arnd Poetzsch-Heffter , Gary T. Leavens, Modular invariants for layered object structures, Science of Computer Programming, v.62 n.3, p.253-286, 15 October 2006
software upgrades;ownership types;object encapsulation