Behavioral Subtyping Using Invariants and Constraints
Author: Barbara Liskov and Jeannette M. Wing
Click here for the
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.
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.