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.