Picture Omitted
slide: Abstraction function and representation invariant
In order to verify that our implementation
of the abstract data type stack is correct
(that is as long as the bound MAX is not exceeded),
we must show, given that the representation invariant holds,
that the pre-conditions of the
concrete operations imply the pre-conditions
of the corresponding abstract operations,
and, similarly, that the post-conditions
of the abstract operations imply the post-conditions
of the concrete operations.
First, we show that for the operation push
the post-condition of the
abstract type specification
is indeed stronger than the (implicit) post-condition
of the implementation.
This is expressed by the following formula.
Since we know that , we may derive that
and .
To establish the correctness of the operation pop,
we must prove that the pre-condition specified
for the abstract operation is indeed stronger
than the pre-condition specified for the concrete
operation, as expressed by the formula
It is easy to see that immediately follows
from the requirement that the sequence is non-empty.
Finally, to prove that the operator pop
leaves the stack in a correct state, we must prove that
which is done in a similar manner as for push.
The correspondence relation
Instructor's Guide
intro,
types,
verification,
behavior,
objects,
composition,
summary,
Q/A,
literature
Behavioral refinement is not restricted
to the realization of abstract specifications.
We will now look at a definition of behavioral
refinement, following [Liskov93],
that may serve as a guideline for programmers
to define behavioral subtypes, both abstract and concrete,
including subtypes extending the behavioral
repertoire of their supertypes.
In [Liskov93] the relation between behavioral
types is explained by means of a so-called
correspondence mapping, that relates
a subtype to its (abstract) supertype.
Picture Omitted
slide: The subtype correspondence mapping
A correspondence mapping is a triple
consisting of an abstraction function
α
(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.
α
slide: Behavioral subtyping constraints
To determine whether a type
σ 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
mτ),
and corresponding method
mτ
(which is determined by applying the renaming
ρ)
we must check the (contravariant) function subtyping
rule, that is
dom( mτ ) \leqslant dom( m σ )
and
dom( mτ ) \leqslant dom( m σ ),
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
pre( mτ )[ xτ : = α( xσ )] ⇒ pre( mσ )
and that
post( m σ ) ⇒ post( m τ )[ x τ : = α( x σ ) ].
Moreover, the invariant characterizing
post( m σ ) ⇒ post( m τ )[ x τ : = α( x σ ) ]
must respect the invariant
characterizing
τ,
that is
τ.
The substitutions
[ x τ : = α( x σ )]
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
x.m(a) where a represents
the arguments to the call,
is mapped to a program
x.m(a) 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 [Liskov93] a distinction is made between
constructors (by which objects are created),
mutators
(that modify the state or value of an object)
and observers
(that leave the state of an object unaffected).
Extension maps are only needed for mutator methods.
Clearly, for observer methods the result
of
φ is empty, and constructors
are taken care of by the abstraction function.
Behavioral subtypes
The behavioral subtyping rules defined above
are applicable to arbitrary (sub)types, and not only
to (sub)types defined by inheritance.
As an example, we will sketch (still
following [Liskov93]) that a stack may be defined as
a behavioral subtype of the type bag.
Recall that a bag is a set allowing duplicates.
See slide [10-ex-subtype].
φ
slide: Behavioral subtypes -- example
Let the type bag support the methods
φ and
φ and assume
that the type stack supports
the methods
push(i:Int),
pop():Int and
in addition a method
pop():Int
that replaces the top element of
the stack with its argument.
Now, assume that a bag is represented by
a pair
〈 elems, bound 〉 , 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
〈 elems, bound 〉 ,
where items is a sequence and limit is
the maximal length of the sequence.
For example
〈 {1,2,7,1}, 12 〉
is a legal value of bag
and
〈 {1,2,7,1}, 12 〉
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
〈 {1,2,7,1}, 12 〉
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
〈 {1,2,7,1}, 12 〉 and
〈 {1,2,7,1}, 12 〉
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
〈 {1,2,7,1}, 12 〉 as in slide [10-ex-correspondence].
- α( 〈 items, limit 〉 ) =
〈 mk_set( items ), limit 〉
where
mk_set( ε ) = ∅
mk_set( e ·s ) = mk_set(s) \uplus {e}
- ρ( push ) = put, ρ( pop ) = get
- ξ(s.settop(i)) =
s.pop(); s.push(i)
slide: Behavioral subtypes -- correspondence
To map the representation of a stack to
the bag representation we use the function
mk_set (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
mk_set 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
settop(i)
as the application of (subsequently)
pop() and
pop().
pop()
slide: Behavioral subtypes -- proof obligations
With respect to the behavioral definitions given for
push and put we have to verify that
pop()
and that
post( push(i) ) ⇒ post( put(i) )[ b : = α(s) ].
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 [Liskov93],
the definition of the appropriate behavioral
constraints and the formulation of
a correspondence mapping is already a significant
step towards verifying that the types have the
desired behavioral properties.