|
CMU-CS-99-156
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMU-CS-99-156
Behavioral Subtyping Using Invariants and Constraints
Barbara H. Liskov*, Jeannette M. Wing
July 1999
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.
CMU-CS-99-156.ps
CMU-CS-99-156.pdf
Keywords: Subtype, object-oriented design, abstraction function,
mutable types, invariants, constraints, specifications
We present a way of defining the subtype relation that
ensures that subtype objects preserve behavioral properties
of their supertypes. The subtype relation is based on the
specifications 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 specifications. We also discuss
the ramifications of our approach of subtyping the design of
type families.
23 pages
*Massachusetts Institute of Technology, 545 Technology Square, Cambridge,
MA 02139
|