topical media & game development

[] readme course(s) preface I 1 2 II 3 4 III 5 6 7 IV 8 9 10 V 11 12 afterthought(s) appendix reference(s) example(s) resource(s) _

object-oriented programming

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

Objects as behavioral types

A syntax-directed correctness calculus as presented in section \ref{10:verification} provides, in principle, excellent support for a problem-oriented approach to program development, provided that the requirements a program has to meet can be made explicit in a mathematical, logical framework. When specifying requirements, we are primarily interested in the abstract properties of a program, as may be expressed in some mathematical domain. However, when actually implementing the program (and verifying its correctness) we mostly need to take recourse to details we do not wish to bother with when reasoning on an abstract level. In this section we will discuss how we may verify that an abstract type is correctly implemented by a behavioral (implementation) subtype, following [Am90]. Also, we will define precise guidelines for determining whether two (behavioral) types satisfy the (behavioral) subtype relation, following [Liskov93].

Abstraction and representation

In [Am90] a proposal is sketched to define the functionality of objects by means of behavioral types. Behavioral types characterize the behavioral properties of objects in terms of (possible) modifications of an abstract state. So as to be able to ignore the details of an implementation when reasoning about the properties of a particular program, we may employ a representation abstraction function which maps the concrete data structures and operations to their counterparts in the abstract domain.

Abstract data types -- representation function

Representation function -- abstraction

$%a(%c)( %a(%f)) = %a(%f')$ $<=>$ $%c (%f) = %f'$

slide: Abstraction and representation

The diagram in slide 10-ADT pictures the reasoning involved in proving that a particular implementation is correct with respect to a specification in some abstract mathematical domain. Assume that we have, in the concrete domain, an action a that corresponds with a state transformation function

%c

. Now assume that we have a similar operation in the abstract domain, that we will write as

%a(a)

, with a corresponding state transformation function

%a(%c)

. To prove that the concrete operation a correctly implements the abstract operation

%a(a)

, we must prove that the concrete state modification

%c

resulting from a corresponds with the modification that occurs in the abstract domain. Technically speaking, we must prove that the diagram above commutes, that is, that

%c(%f) = %f' <=> %a(%c)(%a(%f)) = %a(%f')

whenever we have that

%f -{a}-> %f'

. To prove that a particular implementation a respects the abstract operation

%a(a)

, for which we assume that it has abstract pre- and post-conditions

%a(P)

and

%a(Q)

, we must find a representation invariant I and (concrete) pre- and post-conditions P and Q for which we can prove that

%a(P) /\ I => P

and that

%a(Q) /\ I => Q

. Furthermore, the representation invariant I must hold before and after the concrete operation a. The proof strategy outlined above is of particular relevance for object-oriented program development, since the behavior of objects may, as we have already seen, be adequately captured by contracts. As an additional advantage, however, the method outlined enables us to specify the behavior of an object in a more abstract way than allowed by contracts as supported by Eiffel.

Realization

As an example, consider the specification of a generic stack as given in slide 10-specification. The specification of the stack is based on the (mathematically) well-known notion of sequences. We distinguish between empty sequences, that we write as

<< >>

, and non-empty (finite) sequences, that we write as

< >

. Further, we assume to have a concatenation operator for which we define

s \. <<>> = <<>> \. s = s

and

< > \. < > = < >

. A sequence is employed to represent the state of the stack.

Sequences -- abstract domain

empty sequence -- $<< >>$
concatenation -- $< > \. < >$ $=$ $< >$

Specification


  type stack T {
   $s : seq   T$ ;
  axioms:
   ${ true } push(t:T) { s' = s \. < > }$ 
   ${ s \neq << >> } pop() { s = { s' } \. < > }$ 
  };

slide: The specification of a stack

The operations push and pop may conveniently be defined with reference to the sequence representing the (abstract) state of the stack. We use s and

s'

to represent the state respectively before and after the operation. The operations themselves are completely specified by their respective pre- and post-conditions. Pushing an element e results in concatenating the one-element sequence

< >

to the stacks state. For the operation pop we require that the state of the stack must be non-empty. The post-condition specifies that the resulting state

s'

is a prefix of the original state, that is the original state with the last element (which is returned as a result) removed. To prove that a particular implementation of the stack is conformant with the type definition given above we must prove that

{ I /\ pre(%a(m(e))) } m(e) { I' /\ post(%a(m(e))) }

for both methods push and pop. These proofs involve both an abstraction function

%a

and a representation invariant I, relating the abstract state of the stack to the concrete state of the implementation. Now consider an implementation of the generic stack in C++, as given in slide 10-realization.


  template    implementation  
  class as {
  int t;
  T a[MAX];
  public:
  as() { t = 0; }
  void push(T e) { 
         require(t0); return a[--t]; }
  
  invariant:
  	0 <= t && t < MAX;
  };

slide: The realization of a stack

To prove that this implementation may be regarded as an element of the (abstract) type stack, we must find a representation (abstraction) function to map the concrete implementation to the abstract domain, and further we must specify a representation invariant that allows us to relate the abstract properties to the properties of the implementation. For the implementation in slide 10-realization, the abstraction function

%a

simply creates the sequence of length t, with elements

a[0],...,a[t-1]

. The representation invariant, moreover, gives an explicit definition of this relation. See slide 10-absf.

Abstraction function

$%a(a,t) =$

Representation invariant

$I(a,t,s) == t = length(s) /\ t >= 0 /\ s = %a(a,t)$

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.


   $s' = s \. /\  I(a',t',s') => t' = t + 1 /\ a'[t'] = e$

Since we know that

I(a',t',s')

, we may derive that

t' = t + 1

and

a'[t'] = e

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 $I(a,t,s) /\ s \not= <> => t > 0$ It is easy to see that $t > 0$ 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 $s = s' \. /\ I(a',t',s') => result = a'[t] /\ t' = t - 1$ which is done in a similar manner as for push.

The correspondence relation

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.

Correspondence

$<< %a, %r, %x >>$

$%a$ abstraction -- maps $%s$ values to $%t$ values
$%r$ renaming -- maps subtype to supertype methods
$%x$ extension -- explains effects of extra methods

slide: The subtype correspondence mapping

A correspondence mapping is a triple consisting of an abstraction function

%a

(that projects the values of the subtype on the value domain of the supertype), a renaming

%r

(that defines the relation between methods defined in both types) and an extension map

%x

(that defines the meaning of additional methods). See slide 10-correspondence. Technically, the function

%a

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.

Signature

$%s <= %t$

$dom( m_{%t} ) <= dom( m_{%s} )$
$ran( m_{%s} ) <= ran( m_{%t} )$

Behavior

$pre( m_{%t} )[ x_{%t} := %a( x_{%s} )] => pre( m_{ %s } )$
$post( m_{ %s } ) => post( m_{ %t } )[ x_{ %t } := %a( x_{ %s } ) ]$
$invariant( %s )$ $=>$ $invariant( %t )[ x_{ %t } := %a( x_{ %s } ) ]$

Extension -- diamond rule

$%x(x.m(a)) = %p_{m}$

$%f \apijl{ x.m(a) } %f' /\ %f \apijl{ %p_{m} } %Q$
$=>$ $%a( x_{ %f } ) = %a( x_{ %Q } )$

slide: Behavioral subtyping constraints

To determine whether a type

%s

is a (behavioral) subtype of a type

%t

, one has to define a correspondence mapping

<< %a, %r, %x >>

and check the issues listed in slide 10-subtyping. First, syntactically, we must check that the signature of

%s

and

%t

satisfy the (signature) subtyping relation defined in the previous chapter. In other words, for each method m associated with the object type

%t

(which we call

m_{%t}

), and corresponding method

m_{%s}

(which is determined by applying the renaming

%r

) we must check the (contravariant) function subtyping rule, that is

dom( m_{%t} ) <= dom( m_{ %s } )

and

ran( m_{%s} ) <= ran( m_{ %t } )

, where ran is the range or result type of m. Secondly, we must check that the behavioral properties of

%s

respect those of

%t

. In other words, for each method m occurring in

%t

we must check that

pre( m_{%t} )[ x_{%t} := %a( x_{%s} )] => pre( m_{%s} )

and that

post( m_{ %s } ) => post( m_{ %t } )[ x_{ %t } := %a( x_{ %s } ) ]

. Moreover, the invariant characterizing

%s

must respect the invariant characterizing

%t

, that is

invariant( %s ) => invariant( %t )[ x_{ %t } := %a( x_{ %s } ) ]

. The substitutions

[ x_{ %t } := %a( x_{ %s } )]

occurring in the behavioral rules are meant to indicate that each variable of type

%t

must be replaced by a corresponding variable of type

%s

to which the abstraction function is applied (in order to obtain a value in the (abstract) domain of

%t

). And thirdly, in the final place, it must be shown that the extension map

%x

is well-defined. The extension map must be defined in such a way that each method call for an object x of type

%s

, which we write as

x.m(a)

where a represents the arguments to the call, is mapped to a program

%p_{m}

in which only calls appear to methods shared by

%s

and

%t

(modulo renaming) or external function or method calls. In addition the diamond rule must be satisfied, which means that the states

%f'

and

%q

resulting from applying respectively

x.m(a)

and

%p_{m}

in state

%f

must deliver identical values for x from the perspective of

%t

, 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

%x

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.

Behavioral subtypes

$stack <= bag$

bag -- put, get
stack -- push, pop, settop

Representation

bag -- $<< elems, bound >>$ \zline{multiset}
stack -- $<< items, limit >>$ \zline{sequence}

Behavior -- put/push


   $put(i):$ 
     $require   size( b.elems ) < b.bound$ 
     $promise   b' = << b. elems \uplus { i }, b.bound >>$ 
  
   $push(i):$ 
     $require   length( s.items ) < s.limit$ 
     $promise   s' = << s.items \. i, s.limit >>$

slide: Behavioral subtypes -- example

Let the type bag support the methods

put(i:Int)

and

get():Int

and assume that the type stack supports the methods

push(i:Int)

pop():Int

and in addition a method

settop(i:Int)

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

<< items, limit >>

, 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

\uplus

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

b'

and

s'

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

<< %a, %r, %x >>

as in slide 10-ex-correspondence.

Correspondence

$stack -> bag$

%a(< >) =

<< mk_set( items ), limit >>

where


   $mk_set($ \%e ) = \0
   $mk_set( e \. s ) = mk_set(s) \uplus { e }$

$%r( push ) = put$ , $%r( pop ) = get$
$%x(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

%r

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

push(i)

Proof obligations -- push/put

$size( %a(s). elems ) < %a(s).bound$
$=>$ $length( s.items ) < s.limit$
$s' = << s.items \. i, s.limit >>$
$=>$ $%a(s')$ $=$ $<< %a(s).elems \uplus { i }, %a(s).bound >>$

slide: Behavioral subtypes -- proof obligations

With respect to the behavioral definitions given for push and put we have to verify that

pre( put(i) )[ b := %a(s) ] => pre( push(i) )

and that

post( push(i) ) => post( put(i) )[ b := %a(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.

[] readme course(s) preface I 1 2 II 3 4 III 5 6 7 IV 8 9 10 V 11 12 afterthought(s) appendix reference(s) example(s) resource(s) _

You may not copy or print any of this material without explicit permission of the author or the publisher. In case of other copyright issues, contact the author.