Behavioral Subtyping Using Invariants and ConstraintsaBarbara H. Liskov

Jeannette M. Wing

July 1999
CMU-CS-99-156

a MIT Lab. for Computer Science, 545 Technology Square, Cambridge, MA 02139

School of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213
The work described in this paper is based on a November 1994 ACM TOPLAS paper, \A Behavioral
Notion of Subtyping, by the same authors. This paper's version has been submitted to the volume
Formal Methods For Distributed Processing: An Object-Oriented Approach, edited by Howard Bowman
and John Derrick.

Abstract
We present a way of de ning the subtype relation that ensures that subtype objects preserve behavioral
properties of their supertypes. The subtype relation is based on the speci cations of the sub- and supertypes.
Our approach handles mutable types and allows subtypes to have more methods than their supertypes.
Dealing with mutable types and subtypes that extend their supertypes has surprising consequences on how
to specify and reason about objects. In our approach, we discard the standard data type induction rule,
we prohibit the use of an analogous \history" rule, and we make up for both losses by adding explicit
predicates|invariants and constraints{to our type speci cations. We also discuss the rami cations of ourapproach of subtyping the design of type families.
This research was supported for Liskov in part by the Advanced Research Projects Agency of the Departmentof Defense, monitored by the Oce of Naval Research under contract N00014-91-J-4136 and in part by the National
Science Foundation under Grant CCR-8822158; for Wing, by the Avionics Lab, Wright Research and Development
Center, Aeronautical Systems Division (AFSC), U. S. Air Force, Wright-Patterson AFB, OH 45433-6543 underContract F33615-90-C-1465, ARPA Order No. 7597.

Keywords: subtype, object-oriented design, abstraction function, mutable types, invariants, constraints,
speci cations

1 Introduction
What does it mean for one type to be a subtype of another? We argue that this is a semantic question
having to do with the behavior of the objects of the two types: the objects of the subtype ought to behave
the same as those of the supertype as far as anyone or any program using supertype objects can tell.
For example, in strongly typed object-oriented languages such as Simula 67[DMN70], C++[Str86],
Modula-3[Nel91], and Trellis/Owl[SCB+86], subtypes are used to broaden the assignment statement. An
assignment
x: T := E
is legal provided the type of expression E is a subtype of the declared type T of variable x. Once theassignment has occurred, x will be used according to its \apparent" type T, with the expectation that if the
program performs correctly when the actual type of x's object is T, it will also work correctly if the actual
type of the object denoted by x is a subtype of T.
Clearly subtypes must provide the expected methods with compatible signatures. This consideration has
led to the formulation of the contra/covariance rules[BHJ+ 87, SCB+ 86, Car88]. However, these rules are
not strong enough to ensure that the program containing the above assignment will work correctly for any
subtype of T, since all they do is ensure that no type errors will occur. It is well known that type checking,while very useful, captures only a small part of what it means for a program to be correct; the same istrue for the contra/covariance rules. For example, stacks and queues might both have a put method to add
an element and a get method to remove one. According to the contravariance rule, either could be a legal
subtype of the other. However, a program written in the expectation that x is a stack is unlikely to work
correctly if x actually denotes a queue, and vice versa.
What is needed is a stronger requirement that constrains the behavior of subtypes: properties that canbe proved using the speci cation of an object's presumed type should hold even though the object is actuallya member of a subtype of that type:
Subtype Requirement: Let (x) be a property provable about objects x of type T. Then (y)should be true for objects y of type S where S is a subtype of T.
A type's speci cation determines what properties we can prove about objects.
We are interested only in safety properties (\nothing bad happens"). First, properties of an object's
behavior in a particular program must be preserved: to ensure that a program continues to work as expected,
calls of methods made in the program that assume the object belongs to a supertype must have the same
behavior when the object actually belongs to a subtype. In addition, however, properties independentof particular programs must be preserved because these are important when independent programs shareobjects. We focus on two kinds of such properties: invariants, which are properties true of all states, andhistory properties, which are properties true of all sequences of states. We formulate invariants as predicatesover single states and history properties, over pairs of states. For example, an invariant property of a bag isthat its size is always less than its bound; a history property is that the bag's bound does not change. We
do not address other kinds of safety properties of computations, e.g., the existence of an object in a state,
the number of objects in a state, or the relationship between objects in a state, since these do not haveto do with the meanings of types. We also do not address liveness properties (\something good eventually
happens"), e.g., the size of a bag will eventually reach the bound.
This chapter provides a general, yet easy to use, de nition of the subtype relation that satis es the
Subtype Requirement. Our approach handles mutable types and allows subtypes to have more methods
than their supertypes. Dealing with mutable types and subtypes that extend their supertypes has surprisingconsequences on how to specify and reason about objects. In our approach, we discard the standard data
type induction rule, we prohibit the use of an analogous \history" rule, and we make up for both losses byadding explicit predicates to our type speci cations. Our speci cations are formal, which means that they
have a precise mathematical meaning that serves as a rm foundation for reasoning. Our speci cations canalso be used informally as described in [LG85].
Our de nition applies in a very general distributed environment in which possibly concurrent users sharemutable objects. Our approach is also constructive: One can prove whether a subtype relation holds byproving a small number of simple lemmas based on the speci cations of the two types.
1

The chapter also explores the rami cations of the subtype relation and shows how interesting type families
can be de ned. For example, arrays are not a subtype of sequences (because the user of a sequence expects
it not to change over time) and 32-bit integers are not a subtype of 64-bit integers (because a user of 64-bit
integers would expect certain method calls to succeed that will fail when applied to 32-bit integers). However,type families can be de ned that group such related types together and thus allow generic routines to be
written that work for all family members. Our approach makes it particularly easy to de ne type families:
it emphasizes the properties that all family members must preserve, and it does not require the introductionof unnecessary methods (i.e., methods that the supertype would not naturally have).
The chapter is organized as follows. Section 2 discusses in more detail what we require of our subtype
relation and provides the motivation for our approach. We describe our model of computation in Section 3
and present our speci cation method in Section 4. We give a formal de nition of subtyping in Section 5; wediscuss its rami cations on designing type hierarchies in Section 6. We describe related work in Section 7
and summarize our contributions in Section 8.

2 Motivation
To motivate the basic idea behind our notion of subtyping, let's look at an example. Consider a bounded
bag type that provides a put method that inserts elements into a bag and a get method that removes anarbitrary element from a bag. Put has a pre-condition that checks to see that adding an element will not
grow the bag beyond its bound; get has a pre-condition that checks to see that the bag is non-empty.
Consider also a bounded stack type that has, in addition to push and pop methods, a swap top methodthat takes an integer, i, and modi es the stack by replacing its top with i. Stack's push and pop methods
have pre-conditions similar to bag's put and get, and swap top has a pre-condition requiring that the stack
is non-empty.
Intuitively, stack is a subtype of bag because both kinds of collections behave similarly. The main
di erence is that the get method for bags does not specify precisely what element is removed; the pop
method for stack is more constrained, but what it does is one of the permitted behaviors for bag's getmethod. Let's ignore swap top for the moment.
Suppose we want to show stack is a subtype of bag. We need to relate the values of stacks to those ofbags. This can be done by means of an abstraction function, like that used for proving the correctness of
implementations [Hoa72]. A given stack value maps to a bag value where we abstract from the insertion
order on the elements.
We also need to relate stack's methods to bag's. Clearly there is a correspondence between stack's pushmethod and bag's put and similarly for the pop and get methods (even though the names of the corresponding
methods do not match). The pre- and post-conditions of corresponding methods will need to relate in some
precise (to be de ned) way. In showing this relationship we need to appeal to the abstraction function sothat we can reason about stack values in terms of their corresponding bag values.
Finally, what about swap top? Most other de nitions of the subtype relation have ignored such \extra"
methods, and it is perfectly adequate do so when programs are considered in isolation and there is no aliasing.
In such a constrained situation, a program that uses an object that is apparently a bag but is actually a stack
will never call the extra methods, and therefore their behavior is irrelevant. However, we cannot ignore extra
methods in the presence of aliasing, and also in a general computational environment that allows sharingof mutable objects by multiple users or processes. In particular, we need to pay attention to extra mutator
methods (like swap top) that modify their object.
Consider rst the case of aliasing. The problem here is that within a program an object is accessible bymore than one name, so that modi cations using one of the names are visible when the object is accessedusing the other name. For example, suppose  is a subtype of  and that variables
x: 
y: 
both denote the same object (which must, of course, belong to  or one of its subtypes). When the object
is accessed through x, only  methods can be called. However, when it is used through y,  methods can becalled and if these methods are mutators, their e ects will be visible later when the object is accessed via
2

x. To reason about the use of variable x using the speci cation of its type , we need to impose additional
constraints on the subtype relation.
Now consider the case of an environment of shared mutable objects, such as is provided by object-oriented
databases (e.g., Thor [Lis92] and Gemstone [MS90]). In such systems, there is a universe containing shared,
mutable objects and a way of naming those objects. In general, lifetimes of objects may be longer thanthe programs that create and access them (i.e., objects might be persistent) and users (or programs) may
access objects concurrently and/or aperiodically for varying lengths of time. Of course there is a need forsome form of concurrency control in such an environment. We assume such a mechanism is in place, andconsider a computation to be made up out of atomic units (i.e., transactions) that exclude one another. The
transactions of di erent computations can be interleaved and thus one computation is able to observe themodi cations made by another.
If there were subtyping in such an environment the following situation might occur. A user installs a
directory object that maps string names to bags. Later, a second user enters a stack into the directory undersome string name; such a binding is analogous to assigning a subtype object to a variable of the supertype.
After this, both users occasionally access the stack object. The second user knows it is a stack and accesses
it using stack methods. The question is: What does the rst user need to know in order for his or her
programs to make sense?
We think it ought to be sucient for a user to know only about the \apparent" type of the object; thesubtype ought to preserve any properties that can be proved about the supertype. In particular, the rst
user ought to be able to reason about his or her use of the stack object using invariant and history propertiesof bag.
Our approach achieves this goal by adding information to type speci cations. To handle invariants, we
add an invariant clause; to handle history properties, a constraint clause. Showing that  is a subtype of 
requires showing that (under the abstraction function) 's invariant implies 's invariant and 's constraint
implies 's constraint.
For example, for the bag and stack example, the two invariants are identical: both state that the size ofthe bag (stack) is less than or equal to its bound. Similarly, the two constraints are identical: both state thatthe bound of the bag (or stack) does not change. Showing that stack's invariant and constraint respectively
imply bag's invariant and constraint is trivial. The extra method swap top is permitted because even though
it changes the stack's contents, it preserves stack's invariant and constraint.
In Section 5 we present and discuss our subtype de nition. First, however, we de ne our model ofcomputation, and then discuss speci cations, since these de ne the objects, values, and methods that will
be related by the subtype relation.

3 Model of Computation
We assume a set of all potentially existing objects, Obj, partitioned into disjoint typed sets. Each object
has a unique identity. A type de nes a set of values for an object and a set of methods that provide the onlymeans to manipulate that object. E ectively Obj is a set of unique identi ers for all objects that can containvalues.
Objects can be created and manipulated in the course of program execution. A state de nes a value foreach existing object. It is a pair of mappings, an environment and a store. An environment maps program
variables to objects; a store maps objects to values.
State = Env  StoreEnv = Var ! Obj
Store = Obj ! Val
Given a variable, x, and a state, , with an environment, :e, and store, :s, we use the notation x to denotethe value of x in state ; i.e., x = :s(:e(x)). When we refer to the domain of a state, dom(), we mean
more precisely the domain of the store in that state.
We model a type as a triple, hO; V; M i, where O  Obj is a set of objects, V  Val is a set of values,and M is a set of methods. Each method for an object is a producer, an observer, or a mutator. Producersof an object of type  return new objects of type ; observers return results of other types; mutators modify
3objects of type . An object is immutable if its value cannot change and otherwise it is mutable; a type isimmutable if its objects are and otherwise it is mutable. Clearly a type can be mutable only if some of its
methods are mutators. We allow mixed methods where a producer or an observer can also be a mutator.
We also allow methods to signal exceptions; we assume termination exceptions, i.e., each method call either
terminates normally or in one of a number of named exception conditions. To be consistent with objectoriented language notation, we write x.m(a) to denote the call of method m on object x with the sequenceof arguments a.
Objects come into existence and get their initial values through creators. (These are often called constructors in the literature.) Unlike other kinds of methods, creators do not belong to particular objects, butrather are independent operations.
A computation, i.e., program execution, is a sequence of alternating states and transitions starting insome initial state, 0 :
0 Tr1 1 ::: n,1 Trn nEach transition, Tri , of a computation sequence is a partial function on states; we assume the execution ofeach transition is atomic. A history is the subsequence of states of a computation; we use  and to range
over states in any computation, c, where  precedes in c. The value of an object can change only throughthe invocation of a mutator; in addition the environment can change through assignment and the domain of
the store can change through the invocation of a creator or producer.
Objects are never destroyed:
8 1  i  n : dom(i,1 )  dom(i ).

4 Speci cations

4.1 Type Speci cations

A type speci cation includes the following information: The type's name; A description of the type's value space; A de nition of the type's invariant and history properties;
 For each of the type's methods:{ Its name;{ Its signature (including signaled exceptions);{ Its behavior in terms of pre-conditions and post-conditions.
Note that the creators are missing. Omitting creators allows subtypes to provide di erent creators thantheir supertypes. In addition, omitting creators makes it easy for a type to have multiple implementations,allows new creators to be added later, and re ects common usage: for example, Java interfaces and virtual
types provide no way for users to create objects of the type. We show how to specify creators in Section 4.2.
In our work we use formal speci cations in the two-tiered style of Larch [GHW85]. The rst tier de nes
sorts, which are used to de ne the value spaces of objects. In the second tier, Larch interfaces are used tode ne types.
For example, Figure 1 gives a speci cation for a bag type whose objects have methods put, get, card,and equal. The uses clause de nes the value space for the type by identifying a sort. The clause in thegure indicates that values of objects of type bag are denotable by terms of sort B introduced in the BBagspeci cation; a value of this sort is a pair, helems; boundi, where elems is a mathematical multiset of integers
and bound is a natural number. The notation f g stands for the empty multiset, [ is a commutative
operation on multisets that does not discard duplicates, 2 is the membership operation, and j x j is a4

cardinality operation that returns the total number of elements in the multiset x. These operations as wellas equality (=) and inequality (6=) are all de ned in BBag.
The invariant clause contains a single-state predicate that de nes the type's invariant properties. The
constraint clause contains a two-state predicate that de nes the type's history properties. We will discussthese clauses in more detail in subsequent sections.
bag = typeuses BBag (bag for B)
for all b: bag
invariant j b:elems j  b:boundconstraint b:bound = b :boundput = proc (i: int)
requires j bpre:elems j < bpre:boundmodi es b
ensures bpost:elems = bpre:elems [ fig ^ bpost :bound = bpre:boundget = proc ( ) returns (int)
requires bpre:elems =6 fg
modi es b
ensures bpost:elems = bpre:elems , fresultg ^ result 2 bpre :elems ^bpost :bound = bpre :boundcard = proc ( ) returns (int)ensures result = j bpre:elems jequal = proc (a: bag) returns (bool)
ensures result = (a = b)
end bag
Figure 1: A Type Speci cation for Bags
The body of a type speci cation provides a speci cation for each method. Since a method's speci cationneeds to refer to the method's object, we introduce a name for that object in the for all line. We use result
to name a method's result parameter. In the requires and ensures clauses x stands for an object, xpre forits value in the initial state, and xpost for its value in the nal state.1 Distinguishing between initial andnal values is necessary only for mutable types, so we suppress the subscripts for parameters of immutabletypes (like integers). We need to distinguish between an object, x, and its value, xpre or xpost , because
we sometimes need to refer to the object itself, e.g., in the equal method, which determines whether two(mutable) bags are the same object.
A method m's pre-condition, denoted m.pre, is the predicate that appears in its requires clause; e.g.,
put's pre-condition checks to see that adding an element will not enlarge the bag beyond its bound. If theclause is missing, the pre-condition is trivially \true."
A method m's post-condition, denoted m.post, is the conjunction of the predicates given by its modi es
and ensures clauses. A modi es x1 ; : : :; xn clause is shorthand for the predicate:
8 x 2 (dom(pre) , fx1; : : :; xng) : xpre = xpost
1

Note that pre and post are implicitly universally quanti ed variables over states. Also, more formally, xpre stands for; xpost stands for post.s(post.e(x)).

pre.s(pre.e(x))

5which says only objects listed may change in value. A modi es clause is a strong statement about all
objects not explicitly listed, i.e., their values may not change; if there is no modi es clause then nothing
may change. For example, card's post-condition says that it returns the size of the bag and no objects(including the bag) change, and put's post-condition says that the bag's value changes by the addition of its
integer argument, and no other objects change.
Methods may terminate normally or exceptionally; the exceptions are listed in a signals clause in themethod's header. For example, instead of the get method we might have had
get 0 = proc ( ) returns (int) signals (empty)
modi es b
ensures if bpre:elems = f g then signal empty
else bpost:elems = bpre :elems , fresultg ^result 2 bpre :elems ^ bpost :bound = bpre :bound

4.2 Specifying Creators

Objects are created and initialized through creators. Figure 2 shows speci cations for three di erent creatorsfor bags. The rst creator creates a new empty bag whose bound is its integer argument. The second andthird creators x the bag's bound to be 100. The third creator uses its integer argument to create a singletonbag. The assertion new(x) stands for the predicate:x 2 dom(post) , dom(pre)Recall that objects are never destroyed so that dom(pre)  dom(post).
bag create= proc (n: int) returns (bag)requires n  0
ensures new(result) ^ resultpost = hfg; ni

bag create small = proc ( ) returns (bag)ensures new(result) ^ resultpost = hfg; 100i
bag create single = proc (i: int) returns (bag)ensures new(result) ^ resultpost = hfig; 100i

Figure 2: Creator Speci cations for Bags

4.3 Type Speci cations Need Explicit Invariants

By not including creators in type speci cations and by allowing subtypes to extend supertypes with mutators
we lose a powerful reasoning tool: data type induction. Data type induction is used to prove type invariants.
The base case of the rule requires that each creator of the type establish the invariant; the inductive caserequires that each method (in particular each mutator) preserve the invariant. Without the creators, we haveno base case. Without knowing all mutators of type  (as added by 's subtypes), we have an incomplete
inductive case. With no data type induction rule, we cannot prove type invariants!
To compensate for the lack of a data type induction rule, we state the invariant explicitly in the typespeci cation through an invariant clause; if the invariant is trivial (i.e., identical to \true"), the clause canbe omitted. The invariant de nes the legal values of its type . For example, we include
invariant j b:elems j  b:boundin the type speci cation of Figure 1 to state that the size of a bounded bag never exceeds its bound. The
predicate (x ) appearing in an invariant clause for type  stands for the predicate: For all computations,c, and all states  in c,6

8x :  : x 2 dom() ) (x )Any additional invariant property must follow from the conjunction of the type's invariant and invariants
that hold for the entire value space. For example, we could show that the size of a bag is nonnegative because
this is true for all mathematical multiset values.
As part of specifying a type and its creators we must show that the invariant holds for all objects of thetype. All creators for a type  must establish 's invariant, I :For each creator for type , show for all x: that I [resultpost =x ].
where P[a=b] stands for predicate P with every occurrence of b replaced by a. Similarly, each producer must
establish the invariant on its newly-created object. In addition, each mutator of the type must preserve theinvariant. To prove this, we assume each mutator is called on an object of type  with a legal value (onethat satis es the invariant), and show that any value of a  object it modi es is legal:
For each mutator m of , for all x: assume I [xpre=x ] and show I [xpost=x ].
For example, we would need to show that the three creators for bag establish the invariant, and that
put and get preserve the invariant for bag. (We can ignore card and equal because they are observers.)
Informally the invariant holds because each creator guarantees that the size is no larger than the bound;
put's pre-condition checks that there is enough room in the bag for another element; and get either decreases
the size of the bag or leaves it the same.
The loss of data type induction means that additional invariants cannot be proved. Therefore the speci ermust be careful to de ne an invariant that is strong enough that all desired invariants follow from it.

4.4 Type Speci cations Need Explicit Constraints

We are interested in the history properties of objects in addition to their invariant properties. We canformulate history properties as predicates over state pairs, and prove them using the history rule:
History Rule: For each of the i mutators m of , for all x : :mi :pre ^ mi :post ) [xpre=x ; xpost=x ](x ; x )We cannot use this history rule directly, however. It is incomplete since subtypes may de ne additional
mutators. If we use it without considering the extra mutators, it is easy to prove properties that do not holdfor subtype objects!
To compensate for the lack of the history rule, we state history properties explicitly in the type specication through a constraint clause2 ; if the constraint is trivial, the clause can be omitted. For example,
the constraint

constraint b:bound = b :boundin the speci cation of bag declares that a bag's bound never changes. As another example, consider a fat set
object that has an insert but no delete method; fat sets only grow in size. The constraint for fat set wouldbe:constraint 8 i : int : i 2 s ) i 2 s
The predicate (x ; x ) appearing in a constraint clause for type  stands for the predicate: For allcomputations, c, and all states  and in c such that  precedes ,8x :  : x 2 dom() ) (x ; x )2 The use of the term \constraint" is borrowed from the Ina Jo speci cation language [SH92], which also includes constraints
in speci cations.

7Note that we do not require that be the immediate successor of  in c.
Just as we had to prove that methods preserve the invariant, we must show that they satisfy the constraint.
This is done by using the history rule for each mutator.
The loss of the history rule is analogous to the loss of a data type induction rule. A practical consequenceof not having a history rule is that the speci er must make the constraint strong enough so that all desired
history properties follow from it.

5 The Meaning of Subtype
5.1 Specifying Subtypes

To state that a type is a subtype of some other type, we simply append a subtype clause to its speci cation.
We allow multiple supertypes; there would be a separate subtype clause for each. An example is given in
Figure 3.
A subtype's value space may be di erent from its supertype's. For example, in the gure the sort, S,
for bounded stack values is de ned in BStack as a pair, hitems; limiti, where items is a sequence of integers
and limit is a natural number. The invariant indicates that the length of the stack's sequence component isless than or equal to its limit. The constraint indicates that the stack's limit does not change. In the preand post-conditions, [ ] stands for the empty sequence, jj is concatenation, last picks o the last element ofa sequence, and allButLast returns a new sequence with all but the last element of its argument.
Under the subtype clause we de ne an abstraction function, A, that relates stack values to bag values
by relying on the helping function, mk elems, that maps sequences to multisets in the obvious manner. (Wewill revisit this abstraction function in Section 5.3.) The subtype clause also lets speci ers relate subtype
methods to those of the supertype. The subtype must provide all methods of its supertype; we refer to theseas the inherited methods.3 Inherited methods can be renamed, e.g., push for put; all other methods of thesupertype are inherited without renaming, e.g., equal. In addition to the inherited methods, the subtype
may also have some extra methods, e.g., swap top. (Stack's equal method must take a bag as an argument
to satisfy the contravariance requirement. We discuss this issue further in Section 6.1.)

5.2 De nition of Subtype

The formal de nition of the subtype relation, , is given in Figure 4. It relates two types,  and , each ofwhose speci cations respectively preserves its invariant, I and I , and satis es its constraint, C and C .
In the rules, since x is an object of type , its value (xpre or xpost ) is a member of S and therefore cannot be
used directly in the predicates about  objects (which are in terms of values in T). The abstraction function
A is used to translate these values so that the predicates about  objects make sense. A may be partial,
need not be onto, but can be many-to-one. We require that an abstraction function be de ned for all legal
values of the subtype (although it need not be de ned for values that do not satisfy the subtype invariant).
Moreover, it must map legal values of the subtype to legal values of the supertype.
The rst clause addresses the need to relate inherited methods of the subtype. Our formulation is similar
to America's [Ame90]. The rst two signature rules are the standard contra/covariance rules. The exception
rule says that m may not signal more than m , since a caller of a method on a supertype object should not
expect to handle an unknown exception. The pre- and post-condition rules are the intuitive counterparts tothe contravariant and covariant rules for signatures. The pre-condition rule ensures the subtype's method
can be called at least in any state required by the supertype. The post-condition rule says that the subtype
method's post-condition can be stronger than the supertype method's post-condition; hence, any property
that can be proved based on the supertype method's post-condition also follows from the subtype's method's
post-condition.
The second clause addresses preserving program-independent properties. The invariant rule and theassumption that the type speci cation preserves the invariant suces to argue that invariant properties of asupertype are preserved by the subtype. The argument for the preservation of subtype's history properties
3 We do not mean that the subtype inherits the code of these methods but simply that it provides methods with the same
behavior (as de ned below) as the corresponding supertype methods.

8stack = typeuses BStack (stack for S)
for all s: stackinvariant length(s :items)  s :limit
constraint s:limit = s :limit
push = proc (i: int)
requires length(spre :items) < spre :limit
modi es s
ensures spost:items = spre:items jj [ i ] ^ spost :limit = spre :limit
pop = proc () returns (int)
requires spre :items =6 [ ]modi es s
ensures result = last(spre :items) ^ spost :items = allButLast(spre :items) ^spost :limit = spre :limit

swap top = proc (i: int)

requires spre :items 6= [ ]modi es s
ensures spost:items = allButLast(spre :items) jj [ i ] ^ spost :limit = spre :limit
height = proc ( ) returns (int)ensures result = length(spre :items)
equal = proc (t: bag) returns (bool)
ensures result = (s = t)
subtype of bag (push for put, pop for get, height for card)
8st : S : A(st) = hmk elems(st:items); st:limiti
where mk elems : Seq ! M
8i : Int; sq : Seq
mk elems([ ]) = f g
mk elems(sq jj [ i ]) = mk elems(sq) [ figend stackFigure 3: Stack Type9:  = hO ; S; M i is a subtype of  = hO ; T; N i if
there exists an abstraction function, A : S ! T, and a renaming map, R : M ! N, such that:
Definition of the subtype relation,

1. Subtype methods preserve the supertype methods' behavior. If m of  is the corresponding
renamed method m of , the following rules must hold: Signature rule.
{ Contravariance of arguments. m and m have the same number of arguments. If
the list of argument types of m is i and that of m is i , then 8i : i  i .
{ Covariance of result. Either both m and m have a result or neither has. If there
is a result, let m 's result type be and m 's be . Then  .
{ Exception rule. The exceptions signaled by m are contained in the set of exceptions

signaled by m .
 Methods rule. For all x : :
{ Pre-condition rule. m :pre[A(xpre )=xpre] ) m :pre:{ Post-condition rule. m :post ) m :post[A(xpre )=xpre; A(xpost)=xpost ]2. Subtypes preserve supertype properties. For all computations, c, and all states  and in csuch that  precedes , for all x : :
 Invariant Rule. Subtype invariants ensure supertype invariants.
I ) I [A(x )=x ] Constraint Rule. Subtype constraints ensure supertype constraints.
C ) C [A(x )=x; A(x )=x ]Figure 4: De nition of the Subtype Relationis completely analogous, using the constraint rule and the assumption that the type speci cation satis es its
constraint.
We do not include the invariant in the methods (or constraint) rule directly. For example, the precondition rule could have been(m :pre[A(xpre )=xpre] ^ I [A(xpre )=xpre ]) ) m :preWe omit adding the invariant because if it is needed in doing a proof it can always be assumed, since it is
known to be true for all objects of its type.
Note that in the various rules we require x : , yet x appears in predicates concerning  objects as well.
This makes sense because   .

5.3 Applying the De nition of Subtyping as a Checklist

Proofs of the subtype relation are usually obvious and can be done by inspection. Typically, the only interesting part is the de nition of the abstraction function; the other parts of the proof are usually straightforward.
However, this section goes through the steps of an informal proof just to show what kind of reasoning is
involved. Formal versions of these informal proofs are given in [LW92].
Let's revisit the stack and bag example using our de nition as a checklist. Here = hOstack; S; fpush; pop; swap top; height; equalgi
 = hObag ; B; fput; get; card; equalgi
Recall that we represent a bounded bag's value as a pair, helems; boundi, of a multiset of integers and a xed
bound, and a bounded stack's value as a pair, hitems; limiti, of a sequence of integers and a xed bound. It
can easily be shown that each speci cation preserves its invariant and satis es its constraint.
10

We use the abstraction function and the renaming map given in the speci cation for stack in Figure 3.
The abstraction function states that for all st : S
A(st) = hmk elems(st:items); st:limiti
where the helping function, mk elems : Seq ! M, maps sequences to multisets such that for all sq : Seq; i :Int:
mk elems([ ]) = f g
mk elems(sq jj [ i ]) = mk elems(sq) [ fig
A is partial; it is de ned only for sequence{natural numbers pairs, hitems; limiti, where limit is greater thanor equal to the size of items.
The renaming map R is
R(push) = put
R(pop) = getR(height) = cardR(equal) = equal

Checking the signature and exception rules is easy and could be done by the compiler.
Next, we show the correspondences between push and put, between pop and get, etc. Let's look at the preand post-condition rules for just one method, push. Informally, the pre-condition rule for put/push requiresthat we show4 :j A(spre ):elems j < A(spre ):bound)length(spre :items) < spre :limit
Intuitively, the pre-condition rule holds because the length of stack is the same as the size of the corresponding
bag and the limit of the stack is the same as the bound for the bag. Here is an informal proof with slightly
more detail:1. A maps the stack's sequence component to the bag's multiset by putting all elements of the sequence
into the multiset. Therefore the length of the sequence spre :items is equal to the size of the multisetA(spre ):elems.
2. Also, A maps the limit of the stack to the bound of the bag so that spre :limit = A(spre ):bound.
3. From put's pre-condition we know j A(spre ):elems j < A(spre ):bound.
4. push's pre-condition holds by substituting equals for equals.
Note the role of the abstraction function in this proof. It allows us to relate stack and bag values, andtherefore we can relate predicates about bag values to those about stack values and vice versa. Also, note
how we depend on A being a function (in step (4) where we use the substitutivity property of equality).
The post-condition rule requires that we show push's post-condition implies put's. We can deal with themodi es and ensures parts separately. The modi es part holds because the same object is mentioned inboth speci cations. The ensures part follows from the de nition of the abstraction function.
The invariant rule requires that we show that the invariant on stacks:
length(s :items)  s :limit
implies that on bags:j A(s ):elems j  A(s ):bound
4 Note that we are reasoning in terms of the values of the object, s, and that b and s refer to the same object (b appears inthe bag speci cation).

11

We can show this by a simple proof of induction on the length of the sequence of a bounded stack.
The constraint rule requires that we show that the constraint on stacks:s :limit = s :limit
implies that on bags:
A(s ):bound = A(s ):boundThis is true because the length of the sequence component of a stack is the same as the size of the multiset
component of its bag counterpart.
Note that we do not have to say anything speci c for swap top; it is taken care of just like all the othermethods when we show that the speci cation of stack satis es its invariant and constraint.

6 Type Hierarchies
The requirement we impose on subtypes is very strong and raises a concern that it might rule out many
useful subtype relations. To address this concern we looked at a number of examples. We found that our
technique captures what people want from a hierarchy mechanism, but we also discovered some surprises.
The examples led us to classify subtype relationships into two broad categories. In the rst category,the subtype extends the supertype by providing additional methods and possibly additional \state." In
the second, the subtype is more constrained than the supertype. We discuss these relationships below. In
practice, many type families will exhibit both kinds of relationships.

6.1 Extension Subtypes

A subtype extends its supertype if its objects have extra methods in addition to those of the supertype.
Abstraction functions for extension subtypes are onto, i.e., the range of the abstraction function is the set of
all legal values of the supertype. The subtype might simply have more methods; in this case the abstraction
function is one-to-one. Or its objects might also have more \state," i.e., they might record information thatis not present in objects of the supertype; in this case the abstraction function is many-to-one.
As an example of the one-to-one case, consider a type intset (for set of integers) with methods to insert
and delete elements, to select elements, and to provide the size of the set. A subtype, intset2, might havemore methods, e.g., union, is empty. Here there is no extra state, just extra methods. Suppose intset's
invariant and constraints are both trivial; intset2's would be as well. Thus, proving that intset2 preserves
intset's invariant and constraint is trivial.
It is easy to discover when a proposed subtype really is not one. For example, the fat set type discussed
earlier has an insert method but no delete method. Intset is not a subtype of fat set because fat sets only
grow while intsets grow and shrink; intset does not preserve various history properties of fat set, in particular,
the constraint that once some integer is in the fat set, it remains in the fat set. The attempt to show thatthe intset constraint (which is trivial) implies that of fat set would fail.
As a simple example of a many-to-one case, consider immutable pairs and triples (Figure 5). Pairs havemethods that fetch the rst and second elements; triples have these methods plus an additional one to fetch
the third element. Triple is a subtype of pair and so is semi-mutable triple with methods to fetch the rst,
second, and third elements and to replace the third element because replacing the third element does nota ect the rst or second element. This example shows that it is possible to have a mutable subtype of an
immutable supertype, provided the mutations are invisible to users of the supertype.
Mutations of a subtype that would be visible through the methods of an immutable supertype are ruledout. For example, an immutable sequence, whose elements can be fetched but not stored, is not a supertypeof mutable array, which provides a store method in addition to the sequence methods. For sequences we canprove elements do not change; this is not true for arrays. The attempt to construct the subtype relation will
fail because the constraint for sequences does not follow from that for arrays.
Many examples of extension subtypes are found in the literature. One common example concerns persons,
employees, and students (Figure 6). A person object has methods that report its properties such as its name,age, and possibly its relationship to other persons (e.g., its parents or children). Student and employee are
12immutable pair

immutable triple

semi-mutable triple

Figure 5: Pairs and Triples
subtypes of person; in each case they have additional properties, e.g., a student id number, an employee
employer and salary. In addition, type student employee is a subtype of both student and employee (andalso person, since the subtype relation is transitive). In this example, the subtype objects have more statethan those of the supertype as well as more methods.
personemployeestudent

student_employee

Figure 6: Person, Student, and Employee
Another example from the database literature concerns di erent kinds of ships [HM81]. The supertype isgeneric ships with methods to determine such things as who is the captain and where the ship is registered.
Subtypes contain more specialized ships such as tankers and freighters. There can be quite an elaborate
hierarchy (e.g., tankers are a special kind of freighter). Windows are another well-known example [HO87];
subtypes include bordered windows, colored windows, and scrollable windows.
Common examples of subtype relationships are allowed by our de nition provided the equal method (andother similar methods) are de ned properly in the subtype. Suppose supertype  provides an equal method
and consider a particular call x.equal(y). The diculty arises when x and y actually belong to , a subtypeof . If objects of the subtype have additional state, x and y may di er when considered as subtype objects
but ought to be considered equal when considered as supertype objects.
For example, consider immutable triples x = h0; 0; 0i and y = h0; 0; 1i. Suppose the speci cation of theequal method for pairs says:
equal = proc (q: pair) returns (bool)
ensures result = (p:first = q:first ^ p:second = q:second)(We are using p to refer to the method's object.) However, we would expect two triples to be equal only iftheir rst, second, and third components were equal. If a program using triples had just observed that x andy di er in their third element, we would expect x.equal(y) to return \false," but if the program were using
them as pairs, and had just observed that their rst and second elements were equal, it would be wrong forthe equal method to return false.
The way to resolve this dilemma is to have two equal methods in triple:
pair equal = proc (p: pair) returns (bool)
ensures result = (p:first = q:first ^ p:second = q:second)13

triple equal = proc (p: triple) returns (bool)

ensures result = (p:first = q:first ^ p:second = q:second^ p:third = q:third)

One of them (pair equal) simulates the equal method for pair;the other(triple equal) is a method just on triples. (In some object-oriented languages, such as Java, the additional
equal methods are obtained by overloading.)
The problem is not limited to equality methods. It also a ects methods that \expose" the abstract stateof objects, e.g., an unparse method that returns a string representation of the abstract state of its object.
x.unparse() ought to return a representation of a pair if called in a context in which x is considered to be apair, but it ought to return a representation of a triple in a context in which x is known to be a triple (orsome subtype of triple).
The need for several equality methods seems natural for realistic examples. For example, asking whether
e1 and e2 are the same person is di erent from asking if they are the same employee. In the case of a person
holding two jobs, the answer might be true for the question about person but false for the question about
employee.

6.2 Constrained Subtypes

The second kind of subtype relation occurs when the subtype is more constrained than the supertype. In thiscase, the supertype speci cation is written in a way that allows variation in behavior among its subtypes.
Subtypes constrain the supertype by reducing the variability. The abstraction function is usually into rather
than onto. The subtype may extend those supertype objects that it simulates by providing additional
methods and/or state.
Since constrained subtypes reduce variation, it is crucial when de ning this kind of type hierarchy tothink carefully about what variability is permitted for the subtypes. The variability will show up in the
supertype speci cations in two ways: in the invariant and constraint, and also in the speci cations of theindividual methods. In both cases the supertype de nitions will be nondeterministic in those places where
di erent subtypes are expected to provide di erent behavior.
A very simple example concerns elephants. Elephants come in many colors (realistically grey and white,
but we will also allow blue ones). However all albino elephants are white and all royal elephants are blue.
Figure 7 shows the elephant hierarchy. The set of legal values for regular elephants includes all elephants
whose color is grey or blue or white:invariant e:color = white _ e :color = grey _ e :color = blue
The set of legal values for royal elephants is a subset of those for regular elephants:
invariant e:color = blueand hence the abstraction function is into. The situation for albino elephants is similar. Furthermore, theelephant method that returns the color (if there is such a method) can return grey or blue or white, i.e.,
it is nondeterministic; the subtypes restrict the nondeterminism for this method by de ning it to return a
specifc color.
This simple example has led others to de ne a subtyping relation that requires non-monotonic reasoning[Lip92], but we believe it is better to use variability in the supertype speci cation and straightforward
reasoning methods. However, the example shows that a speci er of a type family has to anticipate subtypes
and capture the variation among them in the speci cation of the supertype.
The bag type discussed in Section 4.1 has two kinds of variability. First, as discussed earlier, the specication of get is nondeterministic because it does not constrain which element of the bag is removed. Thisnondeterminism allows stack to be a subtype of bag: the speci cation of pop constrains the nondeterminism. We could also de ne a queue that is a subtype of bag; its dequeue method would also constrain thenondeterminism of get but in a way di erent from pop.
In addition, the actual value of the bound for bags is not de ned; it can be any natural number, thus
allowing subtypes to have di erent bounds. This variability shows up in the speci cation of put, where we
14

elephantalbinoroyal

Figure 7: Elephant Hierarchy
do not say what speci c bound value causes the call to fail. Therefore, a user of put must be prepared for a
failure. (Of course the user could deduce that a particular call will succeed, based on a previous sequence of
method calls and the constraint that the bound of a bag does not change.) A subtype of bag might limit thebound to a xed value, or to a smaller range. Several subtypes of bag are shown in Figure 8; mediumbags
have various bounds, so that this type might have its own subtypes, e.g., bag 150.
baglargebag(bound = 2

mediumbag
32)(100 <= bound <= 1000)

smallbag(bound = 20)

bag_150(bound = 150)

Figure 8: A Type Family for Bags
The bag hierarchy may seem counterintuitive, since we might expect that bags with smaller bounds
should be subtypes of bags with larger bounds. For example, we might expect smallbag to be a subtypeof largebag. However, the speci cations for the two types are incompatible: the bound of every largebag is
232, which is clearly not true for smallbags. Furthermore, this di erence is observable via the methods: It islegal to call the put method on a largebag whose size is greater than or equal to 20, but the call is not legal
for a smallbag. Therefore the pre-condition rule is not satis ed.
Although the bag type can have subtypes with di erent bounds, it cannot have subtypes where thebounds of the bags can change dynamically. If we wanted a type family that included both bag and such
dynamic bags, we would need to de ne a supertype in which the bound is allowed, but not required, tovary. Figure 9 shows the new type hierarchy. Dynamic bags have a bound that tracks the size: each time anelement is added or removed from a dynamic bag, the bound changes to match the new size. Flexible bags
have an additional mutator, change bound:change bound = proc (n: int)
requires n  jbpre:elemsj
modi es b
ensures bpost:elems = bpre:elems ^ bpost :bound = n
Notice that other types in the family need not have a change bound method.
This example illustrates the di erent ways that subtypes reduce variability. All varying bag subtypes
reduce variability in the speci cation for the put method; varying bag's put method is non-deterministic,15

varying_bag
I: size <= bound
C: true

flexible_bag

dynamic_bag

I: size <= bound
C: true

I: size = bound
C: truebag
I: size <= bound
C: bound stays the same[...as in Fig. 8...]Figure 9: Another Type Family for Bags
since it might add the element (and change the bound) if the size is the same as the bound, or it mightnot. Bag and exible bag reduce this variability by not adding the element, whereas dynamic bag does
add the element. In addition, bag reduces variability by restricting the constraint: the trivial constraint
for varying bag can be thought of as stating \either a bag's bound may change or it stays the same;" theconstraint for bag reduces this variability by making a choice (\the bag's bound stays the same") and users
can then rely on this property for bags and its subtypes. Dynamic bag reduces variability by restricting
varying bag's invariant so that it no longer allows the size to be less than the bound. Finally, exible bag
reduces variability because of the extra mutator, change bound; all its subtypes must allow explicit re-settingof the bound.
Another example is a family of integer counters shown in Figure 10. When a counter is advanced, weonly know that its value gets bigger, so that the constraint is simply
constraint c  c
The doubler and multiplier subtypes have stronger constraints. For example, a multiplier's value always
increases by a multiple, so that its constraint is:constraint 9 n : int : [ n > 0 ^ c = n  c ]For a family like this, we might choose to have an advance method for counter (so that each of its subtypes isconstrained to have this method) or we might not. If we do provide an advance method, its speci cation will
have to be nondeterministic (i.e., it merely states the the size of the counter grows) to allow the subtypes toprovide the de nitions that are appropriate for them.
In the case of the bag family illustrated in Figure 8, all types in the hierarchy might be \real" in the sensethat they have objects. However, sometimes supertypes are virtual; they de ne the properties all subtypes
have in common but have no objects of their own. Varying bag of Figure 9 might be such a type.
Virtual types are useful in many type hierarchies. For example, we would use them to construct a
hierarchy for integers. Smaller integers cannot be a subtype of larger integers because of observable di erencesin behavior; for example, an over ow exception that would occur when adding two 32-bit integers would
not occur if they were 64-bit integers. Also, larger integers cannot be a subtype of smaller ones because
exceptions do not occur when expected. However, we clearly would like integers of di erent sizes to berelated. This is accomplished by designing a virtual supertype that includes them. Such a hierarchy isshown in Figure 11, where integer is a virtual type whose invariant simply says that the size of an integer isgreater than zero. Integer types with di erent sizes are subtypes of integer. In addition, small integer types
are subtypes of regular int, another virtual type; the invariant in the speci cation for regular int states thatthe size of an integer is either 16 bits or 32 bits. An integer family might have a structure like this, or it
might be atter by having all integer types be direct subtypes of integer.
16

counter(value never decreases)

incrementer(value never decreases)

doubler

multiplier(value multiplies)(value doubles)

Figure 10: Type Family for Counters

integer64-bit-int

regular_int
32-bit-int

16-bit-int

Figure 11: Integer Family

7 Related Work
Some research on de ning subtype relations is concerned with capturing constraints on method signatures via
the contra/covariance rules, such as those used in languages like Trellis/Owl [SCB+ 86], Emerald[BHJ+87],
Quest [Car88], Ei el [Mey88], POOL [Ame90], and to a limited extent Modula-3 [Nel91]. Our rules placeconstraints not just on the signatures of an object's methods, but also on their behavior.
Our work is most similar to that of America [Ame91], who has proposed rules for determining basedon type speci cations whether one type is a subtype of another. Meyer [Mey88] also uses pre- and postcondition rules similar to America's and ours. Cusack's [Cus91] approach of relating type speci cationsde nes subtyping in terms of strengthening state invariants. However, none of these authors considers neither
the problems introduced by extra mutators nor the preservation of history properties. Therefore, they allow
certain subtype relations that we forbid (e.g., intset could be a subtype of fat set in these approaches).
Our use of constraints in place of the history rule is one of two techniques discussed in [LW94]. That
paper proposes a second technique in which there is no constraint; instead, extra methods are not allowed
to introduce new behavior. It requires that the behavior of each extra mutator be \explained" in terms ofexisting behavior, through existing methods. We believe the use of constraints is simpler and easier to reason
about than this \explanation" approach.
The emphasis on semantics of abstract types is a prominent feature of the work by Leavens. In his Ph.D.
thesis Leavens [Lea89] de nes types in terms of algebras and subtyping in terms of a simulation relation
between them. His simulation relations are a more general form of our abstraction functions. Leavens
considered only immutable types. Dhara [Dha92, DL92, LD92] extends Leavens' thesis work to deal withmutable types, but rules out the cases where extra methods cause problems, e.g., aliasing. Because of theirrestrictions they allow some subtype relations to hold where we do not. For example, they allow mutablepairs to be a subtype of immutable pairs whereas we do not.
Others have worked on the speci cation of types and subtypes. For example, many have proposed Z as
the basis of speci cations of object types[CL91, DD90, CDD+ 89]; Goguen and Meseguer[GM87] use FOOPS;
Leavens and his colleagues use Larch[Lea91, LW90, DL92]. Though several of these researchers separate thespeci cation of an object's creators from its other methods, none has identi ed the problem posed by the17missing creators, and thus none has provided an explicit solution to this problem.

8 Summary
We de ned a new notion of the subtype relation based on the semantic properties of the subtype andsupertype. An object's type determines both a set of legal values and an interface with its environment(through calls on its methods). Thus, we are interested in preserving properties about supertype values
and methods when designing a subtype. We require that a subtype preserve the behavior of the supertype
methods and also all invariant and history properties of its supertype. We are particularly interested in an
object's observable behavior (state changes), thus motivating our focus on history properties and on mutabletypes and mutators.
We also presented a way to specify the semantic properties of types formally. One reason we chose tobase our approach on Larch is that Larch allows formal proofs to be done entirely in terms of speci cations.
In fact, once the theorems corresponding to our subtyping rules are formally stated in Larch, their proofs arealmost completely mechanical|a matter of symbol manipulation|and could be done with the assistance of
the Larch Prover[GG89, ZW97].
In developing our de nition, we were motivated primarily by pragmatics. Our intention is to capture
the intuition programmers apply when designing type hierarchies in object-oriented languages. However,intuition in the absence of precision can often go astray or lead to confusion. This is why it has been unclear
how to organize certain type hierarchies such as integers. Our de nition sheds light on such hierarchies
and helps in uncovering new designs. It also supports the kind of reasoning that is needed to ensure that
programs that work correctly using the supertype continue to work correctly with the subtype.
Programmers have found our approach relatively easy to apply and use it primarily in an informal way.
The essence of a subtype relationship is expressed in the mappings. These mappings can be de ned informally,in much the same way that abstraction functions and representation invariants are given as comments in a
program that implements an abstract type. The proofs can also be done informally, in the style given in
Section 5.3; they are usually straightforward and can be done by inspection.
We also showed that our approach is useful by looking at a number of examples. This led us to identify
two kinds of subtypes: ones that extend the supertype, and ones that constrain it. In the former case, thesupertype can be de ned without a great deal of thought about the subtypes, but in the latter case, this is
not possible; instead the supertype speci cation must be done carefully so that it allows all of the intended
subtypes. In particular the speci cation of the supertype must contain sucient nondeterminism in theinvariant, constraint, and method speci cations.
Our analysis raises two issues about type hierarchy that have been ignored previously by both theformal methods and object-oriented communities. First, subtypes can have more methods, speci cally moremutators, than their supertypes. Second, subtypes need to have di erent creators than supertypes. Theseissues forced us to revisit proof rules normally associated with type speci cations: the data type induction
rule and the history rule. We decided to preclude the use of these rules, and to have explicit invariants
and constraints to replace them. Although it is possible to de ne a subtype relation that avoids explicit
invariants and constraints, doing so is awkward and often requires invention of super uous supertype methods
and creators. We prefer to use explicit invariants and constraints because this allows a more direct way of
capturing the designer's intent.

References[Ame90] America, P. A parallel object-oriented language with inheritance and subtyping. SIGPLAN,
25(10):161{168, October 1990.
[Ame91] America, P. Designing an object-oriented programming language with behavioural subtyping. In
de Bakker, J. W., de Roever, W. P., and Rozenberg, G., editors, Foundations of Object-Oriented
Languages, REX School/Workshop, Noordwijkerhout, The Netherlands, May/June 1990, volume
489 of LNCS, pages 60{90. Springer-Verlag, NY, 1991.
18

[BHJ+ 87] Black, A. P., Hutchinson, N., Jul, E., Levy, H. M., and Carter, L. Distribution and abstract
types in Emerald. IEEE TSE, 13(1):65{76, January 1987.
[Car88] Cardelli, L. A semantics of multiple inheritance. Information and Computation, 76:138{164,1988.
[CDD+89] Carrington, D., Duke, D., Duke, R., King, P., Rose, G., and Smith, P. Object-Z: An object oriented extension to Z. In FORTE89, International Conference on Formal Description Techniques,
December 1989.
[CL91] Cusack, E. and Lai, M. Object-oriented speci cation in LOTOS and Z, or my cat really is objectoriented! In de Bakker, J. W., de Roever, W. P., and Rozenberg, G., editors, Foundations of
Object Oriented Languages, pages 179{202. Springer Verlag, June 1991. LNCS 489.
[Cus91] Cusack, E. Inheritance in object oriented Z. In Proceedings of ECOOP '91. Springer-Verlag,
1991.
[DD90] Duke, D. and Duke, R. A history model for classes in object-Z. In Proceedings of VDM '90:
VDM and Z. Springer-Verlag, 1990.
[Dha92] Dhara, K. K. Subtyping among mutable types in object-oriented programming languages. Master's thesis, Iowa State University, Ames, Iowa, 1992. Master's Thesis.
[DL92] Dhara, K. K. and Leavens, G. T. Subtyping for mutable types in object-oriented programming
languages. Technical Report 92-36, Department of Computer Science, Iowa State University,
Ames, Iowa, November 1992.
[DMN70] Dahl, O.-J., Myrhaug, B., and Nygaard, K. SIMULA common base language. Technical Report 22, Norwegian Computing Center, Oslo, Norway, 1970.
[GG89] Garland, S. and Guttag, J. An overview of LP, the Larch Prover. In Proceedings of the Third
International Conference on Rewriting Techniques and Applications, pages 137{151, Chapel Hill,
NC, April 1989. Lecture Notes in Computer Science 355.
[GHW85] Guttag, J. V., Horning, J. J., and Wing, J. M. The Larch family of speci cation languages. IEEE
Software, 2(5):24{36, September 1985.
[GM87] Goguen, J. A. and Meseguer, J. Unifying functional, object-oriented and relational programmingwith logical semantics. In Shriver, B. and Wegner, P., editors, Research Directions in Object
Oriented Programming. MIT Press, 1987.
[HM81] Hammer, M. and McLeod, D. A semantic database model. ACM Trans. Database Systems,
6(3):351{386, 1981.
[HO87] Halbert, D. C. and O'Brien, P. D. Using types and inheritance in object-oriented programming.
IEEE Software, 4(5):71{79, September 1987.
[Hoa72] Hoare, C. Proof of correctness of data representations. Acta Informatica, 1(1):271{281, 1972.
[LD92] Leavens, G. T. and Dhara, K. K. A foundation for the model theory of abstract data types with
mutation and aliasing (preliminary version). Technical Report 92-35, Department of Computer
Science, Iowa State University, Ames, Iowa, November 1992.
[Lea89] Leavens, G. Verifying object-oriented prograsm that use subtypes. Technical Report 439, MIT
Laboratory for Computer Science, February 1989. Ph.D. thesis.
[Lea91] Leavens, G. T. Modular speci cation and veri cation of object-oriented programs. IEEE Software, 8(4):72{80, July 1991.
[LG85] Liskov, B. and Guttag, J. Abstraction and Speci cation in Program Design. MIT Press, 1985.
19

[Lip92]

Lipeck, U. Semantics and usage of defaults in speci cations. In Foundations of Information
Systems Speci cation and Design, March 1992. Dagstuhl Seminar 9212 Report 35.
[Lis92] Liskov, B. Preliminary design of the Thor object-oriented database system. In Proc. of the
Software Technology Conference. DARPA, April 1992. Also Programming Methodology Group
Memo 74, MIT Laboratory for Computer Science, Cambridge, MA, March 1992.
[LW90] Leavens, G. T. and Weihl, W. E. Reasoning about object-oriented programs that use subtypes.
In ECOOP/OOPSLA '90 Proceedings, 1990.
[LW92] Liskov, B. and Wing, J. Family values: A semantic notion of subtyping. Technical Report 562,
MIT Lab. for Computer Science, 1992. Also available as CMU-CS-92-220.
[LW94] Liskov, B. and Wing, J. A behavioral notion of subtyping. ACM Trans. on Prog. Lang. and
Systems, pages 1811{1841, November 1994.
[Mey88] Meyer, B. Object-oriented Software Construction. Prentice Hall, New York, 1988.
[MS90] Maier, D. and Stein, J. Development and implementation of an object-oriented DBMS. In Zdonik,
S. and Maier, D., editors, Readings in Object-Oriented Database Systems, pages 167{185. Morgan
Kaufmann, 1990.
[Nel91] Nelson, G. Systems Programming with Modula-3. Prentice Hall, 1991.
[SCB+ 86] Scha ert, C., Cooper, T., Bullis, B., Kilian, M., and Wilpolt, C. An introduction to Trellis/Owl.
In Proceedings of OOPSLA '86, pages 9{16, September 1986.
[SH92] Scheid, J. and Holtsberg, S. Ina Jo speci cation language reference manual. Technical Report
TM-6021/001/06, Paramax Systems Corporation, A Unisys Company, June 1992.
[Str86] Stroustrup, B. The C++ Programming Language. Addison-Wesley, 1986.
[ZW97] Zaremski, A. and Wing, J. Speci cation matching of software components. ACM Trans. on
Software Engineering and Methodology, 6(4):333{369, October 1997.

20