Trace Specifications


What are Trace Specs?

Traces vs. subtraces

A subtrace is any sequence of calls to the procedures/functions in a module.
A trace is a subtrace that represents the entire history of activity in a module. Thus, a trace must start with the first call made on a new instance of the module.

If T.S is a trace, then so is T (as is any prefix of T.S). S is a subtrace, but not necessarily a trace.

For example, consider

Here, let T be
and let S be
Clearly T is a trace, but S is not a trace since a top operation cannot be done as the first operation on a new stack.

Equivalence of Traces

If we assert that (T1 equiv T2) we are saying this:
  forall S: ( 
     L(T1.S) <--> L(T2.S) and 
     forall F: ( L(T1.S.F) --> V(T1.S.F) = V(T2.S.F) ) 
where S is any subtrace and F is any value-returning function.

This says, in effect, that two traces are equivalent if we can substitute one for the other without affecting legality or returned values.

Example: a STACK module


  push: integer;
  pop:  ;
  top:  --> integer;

  /*1*/  (forall T,i) ( L(T) --> L(T.push(i)) )
  /*2*/  (forall T)   ( L( <--> L(T.pop) ) 
  /*3*/  (forall T,i) ( T equiv T.push(i).pop )
  /*4*/  (forall T)   ( L( --> T equiv )
  /*5*/  (forall T,i) ( L(T) --> V(T.push(i).top) = i )

Example: a QUEUE module


  add:     integer;
  remove:  ;
  front:   --> integer;

  /*1*/  (forall T,i) ( L(T) --> L(T.add(i)) )
  /*2*/  (forall T,i) ( L(T) --> L(T.add(i).remove) )
  /*3*/  (forall T)   ( L(T.remove) <--> L(T.front) ) 
  /*4*/  (forall T)   ( L(T.front) --> T equiv T.front )
  /*5*/  (forall T,i) ( L(T.remove) --> 
             T.add(i).remove equiv T.remove.add(i) )
  /*6*/  (forall i)   ( add(i).remove equiv e )
  /*7*/  (forall i)   ( V(add(i).front) = i )
  /*8*/  (forall T,i) ( L(T.front) --> 
             V(T.add(i).front) = V(T.front) )

Normal Form Method

How does one know when to stop in generating Trace Specs? How can one tell when all the important behavioral information has been captured for an ADT?

As with algebraic specs, we rely on a canonical form on which to base a systematic generation procedure.

Parnas observed that there are basically 3 types of trace assertion:

  1. assertion about Legality of a trace
  2. assertion about Equivalence of traces
  3. assertion about Value produced by a function on a trace
He suggested organizing the specifications into these three groups, conquering each category of information separately.

Hoffman and Snodgrass propose a different systematic method, but one that recognizes the importance of capturing each category of information about the operations in an ADT.

They came up with 5 heuristics:

  1. base the spec on a normal form
  2. structure the semantics according the normal form prefixes;
  3. use predicates to abbreviate
  4. develop specs incrementally
  5. use macros to hide record structure
We will examine the first two more closely, by example:

Example: Normal form STACK specs

name STACK

  push: int ;
  pop:  ;
  top:  --> int ;

  NormalForm(T) <--> length(T)=count(push,T)

  forall T,C ( NormalForm(T) & length(C)=1 -->
    forall i (C=push(i) -->
      /*L*/ L(T.C)
    ) & 
    (C=pop -->
      /*L*/ ( L(T.C) <--> T != e ) &
      /*E*/ ( L(T.C) --> forall T1,i (T==T1.push(i) --> T.C == T1) )
    ) &
    (C=top -->
      /*L*/ ( L(T.C) <--> T != e ) &
            ( L(T.C) -->
      /*E*/    T.C == T &
      /*V*/    forall T1,i ( T==T1.push(i) --> V(T.C) = i ) )

Example: Normal form QUEUE specs

name QUEUE

  add: int ;
  remove: ;
  front: --> int ;

  NormalForm(T) <--> length(T)=count(add,T)

  forall T,C ( NormalForm(T) & length(C)=1 -->
    forall i (C=add(i) -->
      /*L*/ L(T.C)
    ) &
    (C=remove -->
      /*L*/ ( L(T.C) <--> T != e ) &
      /*E*/ ( L(T.C) --> forall T1,i (T=add(i).T1 --> T.C==T1 ) ) 
    ) &
    (C=front -->
      /*L*/ ( L(T.C) <--> T != e ) &
            ( L(T.C) -->
      /*E*/    T.C==T &
      /*V*/    forall T1,i ( T=add(i).T1 --> V(T.C)=i ) ) 

More Complicated Examples: Iterators

It was realized early on in the development of ADTs that programmers often wanted a way to systematically access every element in a type, much like stepping through all elements in an array by incrementing a subscript variable in a loop.

The concept of a iterator was developed to provide this capability. Iterators were included in several research languages, including Alphard and CLU.

An iterator abstractly give a way to create a sequence of elements, and then provides operations to return the "next" element in that sequence. Creation of thesequence, and the meaning of "next", are of course dependent on implementation details. At an abstract level, however, use of an iterator is the same no matter what the underlying type is. Thus, an iterator can be thought of as an ADT itself.