Bartussek and Parnas, "Using assertions about traces to write abstract specifications for software modules," in Proceedings of the 2nd Conference on European Cooperation in Informatics, Springer-Verlag, 1978, pp. 111--130.
Parnas and Wang, "The trace assertion method of module interface specification," Technical Report 89-261, Queen's Univ., Kingston, Ontario, October 1989.
Meadows, "A method for automatically translating trace specifications into Prolog," Technical Report 9131, Naval Research Lab, September 1988.
name: argType, ... , argType --> retType
L(trace)
V(trace) = value
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
push(6).push(2).pop.top.push(4)Here, let T be
push(6).push(2).popand let S be
top.push(4)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.
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.
NAME stack SYNTAX push: integer; pop: ; top: --> integer; SEMANTICS /*1*/ (forall T,i) ( L(T) --> L(T.push(i)) ) /*2*/ (forall T) ( L(T.top) <--> L(T.pop) ) /*3*/ (forall T,i) ( T equiv T.push(i).pop ) /*4*/ (forall T) ( L(T.top) --> T equiv T.top ) /*5*/ (forall T,i) ( L(T) --> V(T.push(i).top) = i )
NAME queue SYNTAX add: integer; remove: ; front: --> integer; SEMANTICS /*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) )
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:
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:
name STACK syntax push: int ; pop: ; top: --> int ; predicates NormalForm(T) <--> length(T)=count(push,T) semantics 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 ) ) ) )
name QUEUE syntax add: int ; remove: ; front: --> int ; predicates NormalForm(T) <--> length(T)=count(add,T) semantics 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 ) ) ) )
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.