Automatically Checking an Implementation against Its Formal Specification.
AbstractWe propose checking the execution of an abstract data type's imperative implementation against its algebraic specification. An explicit mapping from implementation states to abstract values is added to the imperative code. The form of specification allows mechanical checking of desirable properties such as consistency and completeness, particularly when operations are added incrementally to the data type. During unit testing, the specification serves as a test oracle. Any variance between computed and specified values is automatically detected. When the module is made part of some application, the checking can be removed, or may remain in place for further validating the implementation. The specification, executed by rewriting, can be thought of as itself an implementation with maximum design diversity, and the validation as a form of multiversion-programming comparison.
Introduction
Encapsulated data abstractions, also called abstract data types (ADTs), are the most promising
programming-language idea to support software engineering. The ADT is the basis for the "informa-
tion-hiding" design philosophy [50] that makes software easier to analyze and understand, and that
can hope to support maintenance and reuse. There are several formal specification techniques for
ADTs [30], a growing number of language implementations of the idea [27], and accepted theories
of ADT correctness [20, 26, 28]. The ADT is a good setting for work on unit testing and testability
[34].
However, for all the ADT's promise, fundamental problems remain concerning ADTs, their
specifications, and implementations. In this paper we address the problem of checking agreement
between an ADT's formal specification and its implementation. We use a particular kind of equational
specification (as rewrite rules) [4], and the C ++ implementation language [54]. The latter
choice is not crucial to this work-almost any ADT programming language, e.g., Ada or Java,
would work as well. We do use special properties of one kind of rewrite specification, which would
make it more difficult to substitute a different kind of specification part. We show how to write C ++
classes and their formal specifications so that the implementation is automatically checked against
the specification during execution. Thus the specification serves as an "effective oracle," and in
any application the self-checking ADT cannot deviate from specified behavior without the failure
being detected.
Because the specification oracle may be inefficient in comparison to the C ++ implementation, its
use may be confined to prototyping and the testing phase of software development. However, for
some applications the specification and implementation may be viewed as independent "versions"
of the same software, which continually check each other. Since both were produced by human
beings, both are subject to error, but their utterly different form and content suggest that there is
minimum chance of a common-mode failure [43].
The central idea that allows self checking is to implement, as part of the C ++ code, the mapping
between concrete implementation states and abstract specification objects. Failure to mechanically
capture this important part of design is a weakness of all existing ADT systems.
Self-checking ADTs
We describe ADTs that check their implementations against specifications at run time, and give a
simple illustrative example.
2.1 Automatic Testing
The implementation side of our system is available "off the shelf." We use C ++ , but any language
that supports ADTs, such as Ada, Eiffel, Java, Smalltalk, etc. would do as well (we make no use
of the "inheritance" part of an object-oriented language). One component of our scheme is thus a
class implementation. (Whether the implementation is thought of as arising from an intuitive
set of requirements, or from a formal specification that is the second component of our scheme, is
immaterial to this description; however, we discuss the issue in section 5.2.)
The second component we require is a formal specification of the axiomatic variety. Here we do
not have so much leeway, because the specification form determines our ability to mechanically check
for specification properties like the consistency of a newly added operation, and plays an essential
role in efficiently checking for abstract equality when the specification serves as an implementation
oracle. We choose to use a rewrite system restricted so that the desirable properties of confluence
and termination can be largely obtained from the syntactic forms [4]. It would be possible to employ
more general specifications, but at the cost of using more powerful (and less efficient) theorem
provers. The limited goal of our scheme argues against this generality and loss of efficiency. We
have made the engineering decision to use a specification fitted to the role of automatic oracle.
The user of our system must supply one additional component, of central importance in our
scheme: a "representation" mapping 1 between the concrete data structures of C ++ instance vari-
ables, and the abstractions of the specification. It is a major weakness of present ADT theory
that the representation mapping is nowhere explicit. The existing theory is framed so that the
implementation is correct if there exists an appropriate representation [22]. But in practice, the
implementor must have a representation in mind. That there is no way to formally record and
maintain this early, crucial design decision is a flaw in all existing ADT design methodologies.
Having written an axiomatic specification, a C ++ class, and an explicit representation mapping,
the user may now test the composite ADT using any unit-test technique. For example, a conventional
driver and code coverage tool could be used to ensure that the C ++ code has been adequately
tested according to (say) a dataflow criterion [52]. Or, tests could be generated to exercise traces
of class operations [34]. Whatever techniques are used, our system will serve as the automatic
test oracle that all existing testing systems lack. It determines the correctness of each operation
invoked, according to the specification. Alternately, the user might decide to test the ADT "in
place," by writing application code using it, and conducting a system test (perhaps using randomly
generated inputs according to an expected operational profile [47]) on the application program with
embedded ADT. During this test, the ADT cannot fail without detection.
2.2 Example: A Small Integer Set
To illustrate our ideas, we use the class "small set of integer" (first used by Hoare [33] to discuss
the theory of data abstraction). The signature for this ADT is shown in figure 1 (from Stroustrup
[54]).
The signature diagram captures the complete syntax of ADT usage. For example, in figure 1
empty takes two arguments, an elem and a nat, and the operations for these types are also shown
in the diagram.
2.2.1 The Specification
The semantics of an ADT can be specified with a set of equations (also called axioms) expressed
in the names of its operations. For example, the intuitive axioms for the insertion operation on a
set are:
These equations determine which combinations of operations are equivalent, and along with an
assumption about combinations not handled by the equations, determine exactly which objects
This name was used by Hoare in his foundational paper [33]. Perhaps "abstraction mapping" is the more common
name, which also better expresses the direction.
set nat
elem
bool
maxsize
cardinality
member
empty
insert
true
false
succ
Figure

1: Signature of a generic, bounded ADT set.
(expressed as ground terms using the operations) consitute the set which forms the ADT. The
most common assumption is the initial one [26]: that any objects which cannot be proved equal
using the equations are distinct. A good deal of work has been done on algebraic specification; see
[12].
When equations are viewed as rewrite rules, the proofs of equivalences are simplified. In this view
care must be taken that a rewrite system is a correct implementation of an algebraic specification.
For this purpose, it suffices to consider ground-convergent (i.e., confluent and terminating) systems.
The above equations will not do as rewrite rules, because the first rule can be applied infinitely often.
A suitable rewrite system can be obtained from an equational specification by completion [41],
although the procedure is not guaranteed to terminate. Alternately, the form of the equations can
be suitably restricted [4], which is the approach chosen here.
Furthermore, most implementations of sets will impose bounds on both set size and the values
of the set's elements, as the type intset given by Stroustrup [54, x5.3.2] does. The simple equations
above do not describe these "practical" set ADTs.
We specify the type intset, from our understanding of the code in [54], using a notation similar
to those of several other "algebraic" specifications, such as Act One [20], Asf [11] or Larch [29],
and explain only those parts needed to understand the example. User-defined sorts are specified by
an enumeration of constructors each with its arity and parameter types, followed by axioms. An
axiom is a rewrite rule of the form
where l and r are respectively the left and right sides of the rule and c is an optional condition [39]-a
guard for the application of the rule. The symbol "?" on the right side of a rule denotes an exceptional
result. Its semantics should be formalized within the framework of order sorted algebras [25].
For our more modest purposes, "?" denotes a computation that must be aborted. Following Prolog
conventions [15] the identifier of a variable begins with an upper case letter and the underscore
symbol denotes an anonymous variable.
The ADT intset of [54] is specified as follows:
intset
constructor
maxsize and element upper bound
element to set
axiom
!= not member(E,insert(F,S))
and cardinality(insert(F,S)) ?= maxsize(insert(F,S))
!= not member(E,insert(F,S))
and
The operations member, cardinality, and maxsize will be axiomatized shortly. We rely on the
reader's intuition of these concepts to explain the above axioms. The style used in these axioms
handles exceptional cases with a "?" axiom, guarded by a constraint defining the exceptional
condition. Thus in the empty axiom the exception occurs only if the parameters are inconsistent.
Similarly, the first axiom for insert handles the error case in which an attempt is made to insert
an element that violates the upper-bound restriction; and, the third axiom for insert handles an
attempt to insert a new element into a set that is already at maximum size. The second and fourth
insert axioms establish that the normal form for a nest of insertions is in element order, without
duplicates.
The last three axioms of insert create overlays, i.e., critical pairs overlapping at the root. We
require the conditions of overlay axioms to be mutually exclusive, so that the overlays created are
vacuously joinable, and consequently [18] the system is confluent.
We make specifications grow incrementally adopting the "stepwise specification by extension"
approach [20]. Each increment adds new operations to a specification. The new specification is a
complete and consistent extension of the old one. We adopt two design strategies [4] to guarantee
completeness and consistency, as follow:
The binary choice strategy generates a set of complete and mutually exclusive arguments
for an operation. Once we have a left side of a rule we define a set of right sides such that the
set of conditions associated with the right sides are mutually exclusive.
The recursive reduction strategy uses a mechanism similar to primitive recursion, but more
expressive, for defining the right side of a rule in a way which ensures termination. The symbol
"!" in the right side of a rule stands for the term obtained from the left side by replacing,
roughly speaking, recursive constructors with their recursive arguments. For example, "!" in
the axioms of cardinality below stands for cardinality(S).
The promised axioms for cardinality, maxsize and member are as follows:
operation cardinality(intset) -? integer
axiom
operation maxsize(intset) -? integer
axiom
operation member(integer,intset) -? boolean
axiom
member(-,empty(-? false
This completes the example specification of intset.
2.2.2 Implementations of the Specification
We consider three implementations of the above specification. They are referred to as a by-hand
implementation, a direct implementation, and a self-checking implementation. A by-hand implementation
is C ++ code written by a programmer to provide the functionality expressed by the
specification. This code is naturally structured as a C ++ class in which operations are implemented
as class member functions. A by-hand implementation of intset appears as the first example in
Stroustrup's text [54, x5.3.2]. The direct implementation [30] is C ++ code automatically generated
from the specification by representing instances of abstract data types as terms, and manipulating
those terms according to the rewrite rules. The self-checking implementation is the union of the
by-hand implementation and the direct implementation with some additional C ++ code to check
their mutual agreement.
We describe the self-checking implementation first, even though it uses the direct implementa-
tion. This presentation order motivates the need for the direct implementation before its considerable
detail is given.
The Self-checking Implementation
As described in the following section, the direct implementation provides the mechanism, in C ++ ,
for computing normal-form terms corresponding to any sequence of specification operations. The
by-hand implementation provides a similar mechanism for computing a result using any sequence of
its member-function calls. These two computations correspond respectively to the upper (abstract)
and lower (concrete) mappings in diagrams such as that displayed in figure 2.
In the abstract world, 2 is the binary relation for set membership. In the concrete world,
member is an operation that transforms the values of state variables. If starting at the lower left
of the diagram and passing to the upper right by the two possible paths always yields the same
result, we say that the diagram commutes. The concrete implementation in a commuting diagram
is by definition correct according to the abstract specification there. In figure 2, suppose that the
boolean result returned by member is m(x; S) where x is an integer value and S is an intset
value. (That is, m is the function computed by member.) Then the diagram commutes iff 2
set
elem 2 bool
State State
member

Figure

2: Commuting diagram for the member operation of the ADT set.
To check the by-hand result against the direct result only requires that code be available for
the representation function, to complete a diagram such as figure 2. The self-checking implementation
comprises the C ++ code of both by-hand and direct implementations, plus a representation
function, and appropriate calls connecting them. The locus of control is placed in the by-hand
implementation. When its member functions are invoked, corresponding normal-form terms are
requested from the direct implementation. The comparison of results, however, takes place in the
abstract world; what is actually compared are the normal forms computed there.
The self-checking implementation for intset illustrates this structure. A self-checking class has
two additional private entities declared first, in the example of type absset, which is the type mark
for a set in the direct implementation. The additional variable abstract contains values of sets from
the direct implementation. The additional function conc2abstr is the representation mapping; it
takes as input parameters the instance variables of intset and returns the corresponding absset
instance.
// Declaration of the self-checking intset class.
class intset -
absset abstract; // abstract version of this class
absset concr2abstr(); // representation function
// Below this line the class is identical to Stroustrup, p. 146ff
int cursize, maxsize;
int *x;
public:
intset(int m, int n); // at most m ints in 1.n
. // (most of the code omitted)
Member functions of the self-checking implementation differ from the corresponding ones in the
by-hand implementation only by the addition of two statements just before each function return.
2 It is more precise to think of a state oe as a mapping from instance-variable names to their values. Then in
any diagram with abstract operation F and concrete operation f , if the variables of the state are x1 ; x2 ; :::; xn , the
diagram commutes iff
For example, the self-checking member function implementing the specification operation empty
follows:
intset::intset(int m, int n) // at most m ints in 1.n
new int[maxsize];
Additional statements for self-checking
abstract value
verify; // check mutual agreement
The direct-implementation function empty is called and its result-a normal form encoded in the
data structures of the direct implementation-saved in the added variable abstract. (The code
for empty appears in the following section.)
The macro verify performs an equality test between the value stored in abstract and that
computed by conc2abstr, which is also a normal-form value. This equality test is particularly
simple because in the direct implementation equality means identity of normal forms. The verify
macro includes an error report if the two values differ. Its code follows.
#define verify "
if (!
cerr !! form("Direct differs from by-hand at line %d of '%s'.``n'', "
The last significant piece of code of the self-checking implementation is the representation
function. The mapping is straightforward, starting with an empty abstract set and adding elements
from the concrete version one at a time to calculate the corresponding abstract set.
absset intset::concr2abstr()
absset upper bound not implemented!
for (int
return h;
It was only when writing this function that the programmer noticed that the by-hand implementation
[54] pays no attention to the upper bound on element size, so MAXINT must be used for this
parameter. The implications of this omission are further discussed in 2.2.3.
The Direct Implementation
In the C ++ direct implementation a user-defined sort has a data structure that is a pointer to a
discriminated union. The discriminant values are tokens whose values stand for constructors of
the sort. Each arm of the union is a C ++ struct whose components represent the arguments of
the constructor associated with the discriminant. Dynamic polymorphism would be a more elegant
alternative, but less portable to other languages. In the example:
int elem; // kind of generic
enum tag - EMPTY, INSERT -; // tokens for the discriminants
struct set-node -
tag t; // constructor discriminant
union -
struct -
int m;
int associated to "empty"
struct -
elem
set-node* s; -1; // arm associated to "insert"
set-node(int m, int r) -
set-node(elem e, set-node* s) -
// Simple macro definitions to improve readability
#define tag-of(w) (w-?t)
#define maxsize-of(w) (w-0.m)
#define range-of(w) (w-0.r)
#define elem-of(w) (w-1.e)
#define set-of(w) (w-1.s)
// Declare a function for each signature symbol
extern absset empty(int m, int r);
extern absset insert(elem e, absset s);
extern int cardinality(absset s);
extern int maxsize(absset s);
extern bool member(elem e, absset s);
// equality-test function
extern bool equal(absset s1, absset s2); // normal-form (syntactic) equality
Constructors and operations are implemented by functions without side effects. The execution
of a function implementing a constructor dynamically allocates its associated union and returns a
pointer to it. Each function implementing a non-constructor consists of a nest of cases whose labels
correspond to the patterns in the rewrite rules. Rule conditions are implemented by conditional
statements. Since both the patterns and the conditions are mutually exclusive the order of execution
may affect the efficiency, but not the result, of a computation. The completeness of the patterns
implies that the execution of a function implementing an operation is bound to find a matching
rule and eventually to execute a call which represents the rule right side. Except for the case of "?"
the execution of this call generates a finite tree of calls whose leaves are always calls to constructor
functions and consequently an abstract representation of a sort instance is always returned. We
translate the condition of a rule with "?" as the right side by means of a macro exception very
similar to the macro assert provided by the GNU C ++ compiler, which we use in our project.
#define
cerr !! "Exception '" !! #ex "
!! form("' at line %d of `%s'."n", -LINE-FILE-)
Examples of the direct implementation of constructor functions and an operation function follow.
absset empty(int m, int r)
absset
absset insert(elem e, absset s)
absset h;
switch
case EMPTY:
new set-node(e,s);
break;
case INSERT:
int cardinality(absset s)
switch
case EMPTY: return 0;
case INSERT: if (member(elem-of(s),set-of(s))) return cardinality(set-of(s));
return
2.2.3 Executing the Small Integer Set
The execution of the self-checking implementation of intset raises some interesting issues about
the by-hand implementation in [54]. Although the documentation in the code seems to require an
upper bound for the value of an element, this constraint is not enforced in the by-hand implementa-
tion. The self-checking implementation detects the problem during testing and issues the following
warning:
Exception 'e ? range-of(s)' at line 41 of `absset.C'.
The message "e ? range-of(s)" is the textual code appearing in an exception macro in the
direct implementation of insert. As the comment there indicates, the exception implements a
violated condition in the axiom:
This problem is undetected during the same test of the code in [54].
The direct implementation includes the operation cardinality that has no corresponding member
function in the by-hand implementation of [54]. A naive programmer might add this observer
function by returning the value of cursize, the counter of elements stored in the array that represents
a set. However, the self-checking implementation would report a failure of such a cardinality
on any test where the by-hand implementation creates a set with insert of duplicate elements.
What the naive programmer missed is that the by-hand implementation in fact stores duplicates
in its array. The specification we wrote for cardinality does not have this unexpected behavior,
and would thus catch the mistake in the naive cardinality implementation.
The small-integer-set example illustrates the benefits gained from a formal specification. Direct
implementation of the specification provides a careful check on a by-hand implementation, allowing
self-checking of test values. Of course, it requires additional effort to write the specification; it can
be argued, however, that without a formal specification, correct code is impossible to write. We
have seen two examples of this in a well understood class of a textbook example.
2.2.4 An example of self-checking
An example will make clear the way in which the explicit representation function allows the results
computed by the by-hand implementation to be checked against those specified by the direct im-
plementation. Consider a previously created intset containing elements 1 and 5. Perhaps this set
was created with the C ++ code:
intset Ex(6,MAXINT);
Then it has already been checked that the state defined by the instance variables, including the
concrete array in which the first two elements are 1 and 5, properly correspond to the term
insert(1,insert(5,empty(6,MAXINT))),
which is the normal form assigned to this state by the representation function.
Now suppose that the element 2 is added to this set, perhaps by the C ++ call Ex.insert(2).

Figure

3 shows the particular case of the commuting diagram that checks this computation. At
the lower level are the instance variables that comprise the concrete state, with the initial value at
concr2abstr
concr2abstr

Figure

3: Commuting diagram for inserting 2 into the Ex intset.
the left. The member function insert in the by-hand implementation transforms these variables
as shown when called with arguments Ex and 2. At the upper level are the corresponding abstract
values, transformed by rewriting in the direct implementation. The explicit representation mapping
concr2abstr() connects the two levels. From the concrete instance variables it constructs the
abstract values, and the comparison that shows the computation to be correct occurs when the
abstract value
is obtained by the two paths around the diagram starting at the lower left and ending at the upper
right.
Of course, what is actually compared in the self-checking is not "abstract values," but bit
patterns of a computer state, a state created by the compiled C ++ program for the direct imple-
mentation. However, these states are so transparently like the structure of the abstract terms, as
words in a word algebra, that it is obvious that they properly correspond. It is impossible to do
better than this in any mechanical way. Mechanical comparisons must be done on computer states,
not the true abstractions that exist only in a mathematical universe, and the best we can do is to
make the states be simple, faithful mirrors of this universe.
3 A Proposed Automatic Testing System
The example of section 2.2 begins with two human-created objects: a specification and a by-hand
implementation. We constructed the self-checking implementation from these by adding a few lines
to the by-hand implementation, lines that call a direct implementation of the specification. We
now consider how to automate the construction of these additional elements in the self-checking
implementation. Mechanical creation of the self-checking implementation helps to justify the extra
effort needed to create independent specifications and by-hand implementations.
3.1 Automating the Direct Implementation
The direct implementation of the specification is nothing else than the implementation of a term
rewriting system. Implementations of this kind are numerous and often add extra features to
rewriting. For example, the Equational Interpreter [49] adds total laziness, Obj3 [27] adds a
sophisticated module system, and SbReve [2] adds a Knuth-Bendix completion procedure. These
are stand-alone systems; in contrast, our direct implementation must appear as a block of C ++ code
to be integrated with the by-hand implementation.
A data representation and the implementation of rewrite rules have been discussed in detail in
section 2.2.2, and it is not difficult to "compile" the appropriate C ++ code from the specification
using compiler-compiler techniques, such as those of the Unix system [38, 42] or some other envi-
ronment, e.g., Standard ML of New Jersey [6, 7]. The most difficult part of the compilation will be
the "semantic" processing to guarantee that the specification rewrite rules possess the termination
and confluence properties that make the direct implementation work. Wherever possible, we will
try to convert semantic properties to syntax properties so that they can be statically checked. For
example, by expressing rewrite rule conditions in an if . then . else form, the mutual exclusion
sufficient to make overlays joinable would be guaranteed by the syntax.
The "object-oriented" reader will have noticed that section 2.2.2 uses a functional-like style
instead of an object-oriented one. Initially we made each abstract object a C ++ class, but changed
because: (1) "functional" code is natural for this application, since abstract objects have no internal
state; and (2) the encapsulation protection offered by a C ++ class is wasted in this case, since the
direct-implementation code is created by a compiler and not for human use. On the other hand,
the modularity of C ++ can be used to good advantage.
3.2 Automating Calls on the Direct Implementation
The additional statements that must be added to the by-hand implementation are few, and present
no difficulties. One way is to write a preprocessor from C ++ into C ++ that effects their addition.
Using a C ++ grammar that omits most of the language's detail, with a compiler compiler that simply
copies most code through directly, is one way to write the preprocessor quickly [9]. A second idea
takes advantage of the existence of the parser in an existing C ++ compiler. It is very easy to modify
the code generator to insert object code for the necessary calls [32]. These ideas converge if the
C ++ compiler is itself more of a preprocessor (into C, say) than a true compiler. In the easiest case,
such a preprocessor might be itself written using a compiler compiler.
There are a number of technical problems in modifying the by-hand implementation. For
example, the abstract and concrete worlds share built-in types like Boolean, and for operations
returning these types the representation function is identity. Thus the machinery of abstract
and verify is not needed, and the inserted calls take a simpler form. A slightly more difficult
problem arises for by-hand implementations that are not functional, such as insert. The usual
implementation uses update in place, as in [54], so the abstact operation has a different arity than
the concrete. Thus slightly different code is required:
void intset::insert(int t)
// Code from Stroustrup, section 3.2
(++cursize ? maxsize) error("too many elements");
int
while (i?0 && x[i-1]?x[i]) -
int
// Self-checking added
3.3 The Representation Function
There remains only the representation function that maps between the concrete and abstract do-
mains, the function named concr2abstr in section 2.2.2. There seems to be no way that essential
parts of this function can be automated. The correspondence between concrete and abstract objects
is a primary design decision made early on in the by-hand implementation, and the designer
is not constrained in its choice. Furthermore, it is crucial to the proper working of the system
we propose that the representation correctly capture the link between concrete and abstract. To
take an extreme example, if the programmer codes a representation that maps all inputs to a (sort
overloaded) constant, then all the equality checks in the verify macro will trivially succeed, and
no errors can be caught.
It can be argued that the extra programming required to code the representation function is a
blessing in disguise. Unless the programmer has a detailed and accurate idea of this function, it is
impossible to write correct functions that implement the specification's operations. What better
way to force this understanding than to insist that it be put into code? What better way to protect
against changes that are inconsistent with the representation than to make use of its code? (Both
of these issues arose in the example above, section 2.2.3.) There is even an answer to the possibility
that an incorrect representation function will trivialize self checking. Programmers are more likely
to err in the direction of misguided elaboration than toward trivial simplicity. The more baroque
a representation is, the less likely it is to conceal its faults; putting in too much will lead to our
system reporting ersatz failures, not to false success.
It has been suggested [44] that very often the representation function is structurally similar to
a routine that pretty-prints a class value from its internal representation to human-readable form.
This insight again underscores how easy it is to code the representation function, and how essential
its capture is.
3.4 System Overview

Figure

4 shows the self-checking implementation that would result from the example in section 2.2.
The direct implementation is invoked from the by-hand implementation by additional code that
computes a term (abstract) in the data structure of the direct implementation, then applies the
representation function concr2abstr to map the implementation state to a term, and compares
these (verify macro).
self-checking implementation
struct setnode.
Direct implementation
class intset f
int cursize,.
intset::intset(int m, .
By-hand implementation
selfcheck;
absset intset::concr2abstr()
absset
Representation function
Sort intset
constructor
empty(.
intset(.
Specification Hand Gen.
Auto. Gen.

Figure

4: Construction of the self-checking implementation.
4 Relation to Previous Work
Previous attempts to link formal specification to ADT implementation have taken a variety of
forms.
Proof systems. The correctness of data type representation is proved using diagrams such as that
presented in figure 2. The subroutine member tests the membership of an element in a set. A
program might represent each set as a fixed-size array of elements and a pointer to the last
element. Hoare [33] shows that the existence of a representation mapping, R that makes the
diagram commutative is proof of the implementation correctness. This mapping is somewhat
"retrospective", since the concrete implementation originates from the abstract world which
is the formalization of intuitive concepts.
Executable specifications. A specification is a non-procedural description of a computation. In
an algebraic specification this description takes the form of a set of equations. When equations
are given an orientation, i.e., are transformed into rewrite rules, the resulting structure, called
a rewrite system [39], allows us to "compute." An elementary step of computation consists
in rewriting some subterm of an expression by means of a rule. A computation is a sequence
of elementary steps. Often two fundamental properties are required: termination, i.e., any
computation sequence ends up in some element which cannot be further rewritten [17], and
confluence, i.e., the choice of which term to rewrite in an expression does not affect the result
of the computation [37]. Rewrite systems with these properties are the model of computation
underlying programming languages such as O'Donnell's Equational Interpreter [49] and
Automatic programming. If ADT specifications are viewed as a very-high-level programming
language (and the executable nature of axiomatic specifications supports this view), then
there is no need to write an implementation at all. The specification when executed is the
implementation. Thus questions of correctness do not arise, and the only difficulty lies in
improving the efficiency of execution. Antoy et al. [3, 5] investigate specification translation
into a number of different languages. Volpano [55] proposes to "compile" the specification
into an imperative language like C. Using ideas from functional languages like ML, he is able
to effect this compilation, although in some cases the efficiency does not approach what would
be obtained in an implementation by hand.
Testing systems. There appear to be three distinct threads in the attempt to use ADTs with
tests.
First, any proof technique can be used to instrument implementation code with run-time
assertions, which check test instances of proof assertions that could not be established by the
theorem prover. The GYPSY system [1] uses this technique.
Second, ADT specifications can be used to formalize the generation of specification-based tests
for an ADT implementation. Gerhart [24] describes a logic-programming approach to generate
test points according to any scheme the tester imposes. In a slightly different approach, an
ESPRIT project automatically generates tests based on traces (operation sequences) without
direction by the tester [23, 13, 14].
Third, the daists system [21] attempted to check consistency of an implementation and
algebraic ADT specification, by executing the concrete code corresponding to the two sides
of a specification axiom, and comparing the results with an implementation-supplied equality
function.
Anna [45] specifications for Ada are intended to cut across these categories, but work has progressed
less far than in the more specialized projects cited above.
Our approach might be described in these terms as a combination of a proof- and a testing
system. In contrast to the executable specification approach, we consider both formal specification
and independently devised implementation. (Perhaps both are derived from a common intuitive
description.) In contrast to the automatic programming approach, the implementation code is not
guaranteed to be correct by transformational origin; indeed, the implementation may be full of the
tricks that are the death of formal proof (but essential in practice for efficiency).
The view that specifications are their own implementation is attractive; for one thing, it cuts
the work of specification and implementation in half. However, its drawback is that it merely
moves the correctness problem up a level. However carefully a specification is devised, it may fail
to capture the intuitive ideas of problem solution that led to it, and that intuition necessarily exists
on a plane inaccessible to formal methods. Hence it may be wise to duplicate the work of problem
solution in very different specifications and implementations, both drawing on the intuitive problem
model. One may then hope that where the model is unclear or faulty, the independent attempts to
capture it formally will differ, and precise correctness methods will detect the difficulty and lead
to correction of the model.
Unlike those who use proof systems, we do not attempt to verify the implementation, but only
to check it for particular cases. (The return for this drastic restriction is a large improvement in the
success rate of the process, and a lowering of the skill level needed to use it.) Ours is a testing system
using some proof techniques, whose nearest precursor is daists [21]. Unlike daists, however, our
test for equality of ADT values is conducted in the abstract domain (hence the proof techniques)
rather than in the concrete domain. We thus avoid both practical and theoretical deficiencies that
could falsify a daists success, yet do not pay an efficiency penalty, because we use rewriting for the
abstract proofs, with an explicit mapping from the concrete to abstract domain. This mapping and
its expression as part of the implementation are our main contribution. The extra programming
required for the representation function corresponds to the need for the daists programmer to
explicitly code a concrete equality function, but is easier and more natural to satisfy.
Our system can also be viewed as checking runtime behavior using code assertions. Unlike
ad hoc systems [46] or proof-based systems such as GYPSY [1], however, these assertions are not
written by the user, even in conjunction with a theorem prover. Rather, they are automatically
generated, and are guaranteed to detect deviation from specifications.
We do not generate test data, nor judge the adequacy of test data, but any scheme that does
generate tests [35, 36] or measure test quality [16, 48] can be used with our system supplying
the test oracle, a facility that all testing systems presently lack. Frankl and Doong [19] describe
a system that uses rewriting to obtain one (abstract) test case from another, so that the results
of an implementation can be compared on these cases. Sankar [53] uses a much more powerful
rewriting theorem prover to attempt to prove abstract equality between all terms an implementation
generates. Antoy and Gannon [4] use rewrite systems similar to ours to prove the correctness of
loops and subtypes with the help of a theorem prover. All these systems are less straightforward
than ours, because they lack the explicit representation function and/or the specification restrictions
needed to guarantee rewriting termination.
Compared to automatic proof schemes for ADTs, and to automatic programming of efficient programs
from formal specifications, the goal for our testing system is modest. We imagine no more
than an automatically generated, perfect set of run-time assertions, which make it impossible for a
by-hand implementation to silently disagree with the specification. We can attain the limited goal
where more ambitious ones present formidable problems, but is it worthwhile? In this section we
try to answer that question in the affirmative.
5.1 The Need for Test Oracles
The testing literature almost universally assumes that test output is examined for correctness;
and, it almost universally fails to say how this can be done. Furthermore, research examples [51]
and empirical studies [10] alike show that it is common for testers to have failures in their hands,
yet ignore them. Thus the "effective oracle problem"-the difficulty of mechanically judging if
a program's output meets specifications-is an important one. It assumes extra importance for
random testing. Recent work suggests that true random testing based on a valid operational
profile is essential, and that confidence in such tests requires a vast number of test points [31]. The
adequacy criteria in widespread use require hundreds of points; adequate random testing requires
millions. Such tests are flatly impractical without an effective oracle.
Given the oracle, random testing is doubly attractive, however. Not only is it theoretically
valid, able to provide a true estimate of reliability, but it approximates the ideal of a "completely
automatic" test. The random inputs can be selected mechanically, and with a means of mechanically
examining outputs, a test suite can be run without the need for human intervention.
5.2 Multi-version Specification/Programming
When a specification is viewed as a program in a very high level language, yet no general algorithm
exists for compiling that language into efficient code, there is still a place for by-hand implementa-
tion. In this view, the development process is directed. First comes a requirements phase in which
the developers, in communication with the end users, attempt to create a formal specification that
captures the necessary intuitive problem solution. In this process the prototyping aspect (see section
5.3) of the specification formalism is of great importance. Next, the specification is efficiently
implemented, automatically where possible, by hand otherwise. Formal methods are used to show
that this implementation is correct. In practice, we believe that there will always be a need for
by-hand implementations, and that general methods of proof will always need to be supplemented
by tests. The system we have proposed can automate the testing process efficiently.
One can argue that when development proceeds from requirements to formal specification to
by-hand implementation, the declarative form of specification is not the best. Rather, a form of
specification much closer to the ultimate imperative implementation language is called for [56]. The
advantages are twofold: first, such procedural specifications are easier to write; and second, many
of the detailed problems of an imperative-program solution must be addressed in the prototype, so
that the by-hand implementation is easier, and less prone to introduce subtle disagreements with
the specification.
However, there is a rather different view of specification/implementation in program develop-
ment. In this view, both specification and implementation are imperfect reflections of intuitive
requirements for problem solution. This view is particularly appropriate in safety-critical applica-
tions. In an attempt to provide software fault tolerance, the technique of multi-version programming
(mvp) has been suggested [8]. However, it has been observed [40] that so-called "common-mode
failures" are more frequent than might be expected-working from the same (informal) specifica-
tion, independent programming teams make mistakes that lead to coincident wrong results. The
proposed solution is design diversity, that is, programs that differ so radically that they are truly
independent. A recent study [43] casts doubt on the whole idea of mvp, and in contrast suggests
that internal self-checking is more valuable, particularly when the checking involves the details of
internal program states.
The system we propose fits the needs of safety-critical applications very well. It is the ultimate in
self-checking code, and the checks are applied to internal data-structure states, through the explicit
representation function that maps those states into the direct implementation. At the same time,
because the direct implementation is executed, a self-checking implementation can be viewed as
a two-version programming package with ultimate design diversity. The declarative nature of the
axiomatic specification, and its direct execution by rewriting, should make common-mode failure
with a conventional by-hand implementation unlikely.
5.3 Rapid Prototyping
Previous systems implementing specifications directly, such as Obj3 [27], have been designed so
that specifications can be executed as prototypes, to allow potential users to interact with software
before a complete development effort freezes the wrong design. Our direct implementation adds a
new dimension to this idea. The by-hand implementation and the direct one implement the same
specification completely and independently. In our software development approach we use the
former for production, both for testing, and the latter for prototyping. Our two implementations
coexist in the same environment, that of the final product. In earlier systems prototypes are
confined to unusual software and/or hardware platforms (e.g., Obj3 lives inside Common Lisp).
Our prototype and production modules interact in very similar ways with the rest of the system.
From an external point of view, the only difference between the two versions of an operation is
that the direct implementation is side-effect free, while the by-hand implementation, for efficiency
reasons, might not be. This gap can be filled by a trivial interface limited to renaming operations
and rearranging parameters and modes of function declarations.
6 Summary and Future Work
We have proposed a modest testing system for modules using an algebraic specification executable
as rewrite rules. The programmer must write a specification, C ++ code to implement it, and a
representation function relating implementation data structures to abstract terms. From these three
elements a self-checking implementation can be constructed automatically, in which the specification
serves as a test oracle. The self-checking implementation can be viewed as a vehicle for testing only,
or as a special kind of two-version programming system with exceptional design diversity.
We are pursuing two quite different goals for the future. First, we are investigating more expressive
languages for the formal specification component of our approach and by-hand implementation
languages, such as Java, simpler than C ++ . Second, we want to use these ideas in a practical set-
ting, to learn more about the difficulty of writing specifications, and the value of a test oracle. The
ideal testbed is an industrial user of object-oriented design with a central group responsible for
developing highly reliable support software that other developers use. In such a group, it should
be worthwhile putting the extra effort into specification, in return for better testing and reliability.



--R

A language for specification and implementation of verifiable programs.
A term rewriting laboratory with (AC-)unfailing completion

Using term rewriting systsem to verify software.

A lexical analyzer generator for Standard ML.
ML-Yacc, version 2.0.
Fault tolerance by design diversity: concepts and experiments.
Prototype testing tools.
Comparing the effectiveness of software testing strategies.
Algebraic Specification.
Algebraic System Specification and Development.
Application of prolog to test sets generation for algebraic specifications.
Test data generation using a Prolog with constraints.
Programming in Prolog.
A formal notion of program-based test data adequacy
Termination. In RTA'85
Confluence of conditional term rewrite systems.
Case studies on testing object-oriented programs
Fundamentals of Algebraic Specification 1.
Data abstraction implementation
Theory of modules.
Generation of test data from algebraic specifications.
Test generation method using prolog.
Operational semantics of order-sorted algebras
An initial algebra approach to the specifi- cation
Introducing Obj3.
The algebraic specification of abstract data types.
The Larch family of specification languages.
The design of data type specifications.
Partition testing does not inspire confidence.
Testing programs with the aid of a compiler.
Proof of correctness of data representations.
Hardware testing and software ICs.
Module test case generation.
Methodology for the generation of program test data.
Confluent reductions: Abstract properties and applications to term-rewriting sys- tems
Yacc: yet another compiler compiler.
rewriting systems.
An experimental evaluation of the assumption of independence in multi-version programming
Simple word problems in universal algebras.

The use of self checks and voting in software detection: An empirical study.
Personal communication.
Programming with Specifications: An Introduction to ANNA

Software Reliability: Measurement
A comparison of some structural testing strategies.
Equational Logic as a Programming Language.
On the criteria to be used in decomposing systems into modules.
On the automated generation of program test data.
Selecting software test data using data flow information.


Software templates.
The operational versus the conventional approach to software development.
--TR

--CTR
Daniel Hoffman , Durga Prabhakar , Paul Strooper, Testing iptables, Proceedings of the conference of the Centre for Advanced Studies on Collaborative research, p.80-91, October 06-09, 2003, Toronto, Ontario, Canada
Dick Hamlet, When only random testing will do, Proceedings of the 1st international workshop on Random testing, July 20-20, 2006, Portland, Maine
Qing Xie , Atif M. Memon, Designing and comparing automated test oracles for GUI-based software applications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.16 n.1, p.4-es, February 2007
Johannes Henkel , Amer Diwan, A Tool for Writing and Debugging Algebraic Specifications, Proceedings of the 26th International Conference on Software Engineering, p.449-458, May 23-28, 2004
David Owen , Dejan Desovski , Bojan Cukic, Random testing of formal software models and induced coverage, Proceedings of the 1st international workshop on Random testing, July 20-20, 2006, Portland, Maine
James H. Andrews , Susmita Haldar , Yong Lei , Felix Chun Hang Li, Tool support for randomized unit testing, Proceedings of the 1st international workshop on Random testing, July 20-20, 2006, Portland, Maine
Douglas Gregor , Sibylle Schupp, STLlint: lifting static checking from languages to libraries, SoftwarePractice & Experience, v.36 n.3, p.225-254, March 2006
rewriting;formal specification;self-checking code;object-oriented software testing