This page links the files used in the experiment described in the appendix of Automatically 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.

  1. original Vector.java
  2. instrumented Vector.java
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.

  1. Driver test-1/TestDriver.java chooses the operation to call with equal probability.
  2. Driver test-2/TestDriver.java 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,
  3. Driver test-3/TestDriver.java calls operations of a flawed implementation of class Vector. This gives us an opportunity to verify the effectiveness of self-checkin.
File flawed 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.