This chapter extended the notion of
subtyping to include
behavioral properties.
In section 1,
we discussed the interpretation of types
as behavior and we looked at
the issues involved in preserving
invariance and history properties.
Also, we discussed the duality between
static and dynamic type constraints.
In section 2,
a brief characterization of an assertion logic
for verifying behavioral properties
was given.
We looked at a formal characterization of
states and state transitions and correctness
formulae were introduced as a means to
verify the correctness of transitions.
We also looked at an axiomatic characterization of the
correctness properties of programming
language constructs.
In section 3,
we looked at how the behavior of
an object may be defined in a formal
way by means of a transition system.
A transition system for an object-based
language specifies the rules for assignment,
object creation and method call,
as well as the computation steps
resulting from the evaluation
of compound statements.
In section 4,
it was shown how actual objects may be related to abstract types
by means of a representation abstraction function.
Further, we discussed explicit guidelines
for defining a subtype
correspondence relation between behavioral types.
Finally, in section 5, we looked at the problems involved
in determining global invariants and
we discussed what formal means we have available
to specify behavioral properties of
a collection of objects.
