Abstraction and representation

intro, types, verification, behavior, objects, composition, summary, Q/A, literature

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

contract model-view< V > {

Representation function -- abstraction

α(ξ)( α(φ)) = α(φ′) \desdak ξ(φ) = φ′

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.

α(ξ)( α(φ)) = α(φ′) \desdak ξ(φ) = φ′

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.

α(a,t) = < a[0],…,a[t] >

I(a,t,s) ≡ t = length(s) ∧t \geqslant 0 ∧s = α(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.