(that projects the values of the subtype
on the value domain of the supertype),
a renaming 
(that defines the relation between methods defined
in both types)
and an extension map 
(that defines the
meaning of additional methods).
See slide 10-correspondence.
Technically, the function 
must be onto, that is
each value of the supertype domain must be
representable by one or more values of the subtype domain.
Generally, when applying the abstraction function,
we loose information (which is irrelevant from
the perspective of the supertype), for
example the specific ordering of items in a container.
is a
(behavioral) subtype of a type 
, one
has to define a correspondence mapping
and check the issues listed in slide 10-subtyping.
First, syntactically, we must check that the
signature of 
and 
satisfy the (signature)
subtyping relation defined in the previous chapter.
In other words, for each method m associated
with the object type 
(which we call 
),
and corresponding method 
(which is determined by applying the renaming 
)
we must check the (contravariant) function subtyping
rule, that is
and
,
where ran is the range or result type of m.
Secondly, we must check that the behavioral
properties of 
respect those of 
.
In other words, for each method m
occurring in 
we must check
that 
and that
.
Moreover, the invariant characterizing 
must respect the invariant
characterizing 
,
that is
.
The substitutions 
occurring in the behavioral rules are meant
to indicate that each variable of
type 
must be replaced by a corresponding variable
of type 
to which the abstraction function is applied
(in order to obtain a value in the (abstract) domain of 
).
And thirdly, in the final place,
it must be shown that the extension map
is well-defined.
The extension map must be defined in such a way
that each method call for an object
x of type 
,
which we write as 
where a represents
the arguments to the call,
is mapped to a program 
in
which only calls appear to methods shared by
and 
(modulo renaming)
or external function or method calls.
In addition the diamond rule
must be satisfied,
which means that the states 
and 
resulting from
applying respectively 
and 
in state 
must deliver identical
values for x from the perspective of 
,
that is after applying the abstraction function.
In other words, extension maps allow us to understand
the effect of adding new methods and to establish
whether they endanger behavioral compatibility.
In 
is empty, and constructors
are taken care of by the abstraction function.
and 
and assume
that the type stack supports
the methods 
, 
and
in addition a method 
that replaces the top element of
the stack with its argument.
Now, assume that a bag is represented by
a pair 
, where
elems is a multiset (which is a set
which may contain multiple elements of the same value)
and bound is an integer indicating the maximal
number of elements that may be in the bag.
Further, we assume that a stack is represented as
a pair 
,
where items is a sequence and limit is
the maximal length of the sequence.
For example 
is a legal value of bag
and 
is a legal value of stack.
The behavioral constraints for respectively the
method put
for bag
and push
for stack
are given as pre- and post-conditions in slide 10-ex-subtype.
To apply put, we require that the size
of the multiset is strictly smaller than the bound
and we ensure that the element i is inserted
when that pre-condition is satisfied.
The multi-set union operator 
is employed to add the new element to
the bag.
Similarly, for push we require the length
of the sequence to be smaller than the limit
of the stack
and we then ensure that the element is appended
to the sequence.
As before, we use the primed variables 
and 
to denote the value of respectively
the bag b and the stack s after
applying the operations, respectively put and push.
Proceeding from the characterization of bag
and stack we may define the correspondence
mapping 
as in slide 10-ex-correspondence.
(which is inductively defined to map
the empty sequence to the empty set and to
transform a non-empty sequence into the union
of the one-element multiset of its first element
and the result of applying 
to the remaining
part).
The stack limit is left unchanged, since
it directly corresponds with the bound of the bag.
The renaming function 
maps push to put
and pop to get, straightforwardly.
And, the extension map describes the result of 
as the application of (subsequently) 
and 
.
and that
.
These conditions, written out fully in slide 10-ex-proof,
are easy to verify.
Generally, a formal proof is not really necessary
to check that two types satisfy the behavioral
subtype relation.
As argued in |
Hush Online Technology
hush@cs.vu.nl
12/29/99 |
|
|