This page links the files used in the experiment described in the appendix
Checking an Implementation against its Formal Specification. The paper
proposes a technique to self-check the execution of an abstract data type's
imperative implementation against its algebraic specification. Consult
the paper for description of both the self-checking technique and the experiment
that uses these files.
The abstract data type that we wish to check is a vector. A vector
is an indexed collection similar to a built-in array of most programming
languages. It differs from a typical array in that it provides operations
to insert or remove elements at a given index. Consequently a vector
can be extended or contracted at run time. A formal specification of vector
is in file specification. The language of the
imperative implementation of the specification is Java. Java package
util contains a class, called Vector, that efficiently implements
the specification. In the following we refer to version 1.36 of the code
that is distributed with version 1.1 of the Java Development Kit.
The technique described in the paper requires to instrument the imperative
implementation of the self-checking abstract data type. The instrumented
version of the implementation is, except for
a small part, automatically generated from the original version. The
links to both original and instrumented version of the code follow.
The formal specification of class Vector
is implemented in Java and is used to check the execution of the imperative
implementation of class Vector. The specification is implemented
by a base class, absVector.java, and by one
additional class for each constructor of the abstract data type. Class
Vector has two constructors implemented by classes absEmpty.java
and absMap.java respectively.
A self-checking experiment involves an instrumented implementation of
an abstract data type, an implementation of the abstract data type's specification
and a driver. The driver repeatedly calls the public operations (constructors
and methods) of the class. Each operation of the class is instrumented
to check, at the end of its execution, whether the state of the objects
it belongs to is the same as the state computed by the specification. The
sequence of calls executed by the driver are randomly choosen. The arguments,
if any, of a call are randomly choosen within predefined ranges.
We perform three sets of tests with different drivers.
Vector.java contains the source code of the flawed implementation.
A trace of the execution of the driver with the flawed implementation is
in file trace-30000.
This is a large file (over 1Mb) that is more easily re-created on a client
than downloaded from this server. Script compile-and-run
compiles the Java source files and executes them to generate the trace.
chooses the operation to call with equal probability.
avoid new constructions and the operation that remove all the elements
of a vector. This test generates many more overflows of a vector
with consequent reallocation of a vector storage,
calls operations of a flawed implementation of class Vector. This
gives us an opportunity to verify the effectiveness of self-checkin.