Example -- $IntSet \not<= FatSet$
- FatSet -- insert, select, size
- IntSet -- insert, delete, select, size
History property -- not satisfied by $IntSet$
post( push(i) ) ⇒ post( put(i) )[ b : = α(s) ]
slide: History properties -- example
With respect to its signature, IntSet merely extends
FatSet with a delete method and hence
could be regarded as a subtype of FatSet.
However, consider the history property stated above,
which says that for any (FatSet) s, when an
integer x is an element of s in state
then x will also be an element of s
in any state that comes after .
This property holds since instances of FatSet
do not have a method delete by which elements
can be removed.
Now if we take this property into account,
IntSet may not be regarded as a subtype
of FatSet, since instances of IntSet may grow
and shrink and hence do not respect the
FatSet history property.
This observation raises two questions.
Firstly, how can we characterize the behavior
of an object or function and, more importantly,
how can we extend our notion of types to
include a behavioral description?
And secondly, assuming that we have the means to
characterize the behavior of a function or object
type, how can we verify that a subtype respects
the behavioral constraints imposed by the supertype?
The answer to the first question is suggested
by the observation that we may also express the constraints
imposed by the signature by means of logical formulae
that state the constraints as assertions which must
be satisfied.
post( push(i) ) ⇒ post( put(i) )[ b : = α(s) ]
slide: Types and behavioral constraints
For example, we may express the requirement imposed
by typing a variable as an element of an integer
subrange also by stating that the variable is an integer
variable that respects the bounds of the subrange.
Similarly, we can express the typing constraints
on the domain and range of a function by
means of pre- and post-conditions asserting these
constraints.
See slide [10-constraints].
More generally, we may characterize the behavior
of a function type by means of pre- and post-conditions
and the behavior of an object type by means
of pre- and post-conditions for its methods
and an invariant clause expressing the
invariant properties of its state and behavior.
Recall that
this is precisely what is captured in our
notion of contract, as discussed in section [contracts].
With regard to the second question,
to verify behavioral properties (expressed as assertions)
we need an assertion logic in the style of Hoare.
Such a logic will be discussed in the next section.
In addition, we need a way in which to verify that
(an instance of) a subtype respects
the behavioral properties of its supertype.
In section [correspondence]
we will give precise guidelines for a programmer
to check the behavioral correspondence between two types.