Our Tool

The idea behind our tool is simple: given the fact that the problem of checking the requirements of a function is undecidable, we use sampling to get an approximation of the probability that a contract remains satisfied. This section describes the components and general functionality of our tool, which we call STACC (STAtistical Contract Checker).

As shown in Figure 2, the main component of STACC, uses a Java class model of a contract and an object factory to generate random objects to allow testing of the requirements specified by the contract class. It will then present the user a report stating how many times the contract was satisfied, and how often was the precondition evaluated to true. This is important because if precondition is evaluated to false, then the implication precondition => postcondition will immediately be evaluated to true, regardless of the value of postcondition.

To make things easier for the user, we have introduced a contract specification file format, that will be automatically translated into a Java class to model the specified contract. The general syntax for this file type is shown in Figure 3. The ContGen tool will take as input such a file and generate a new Java source code file representing the class that will be used to check the contract on the randomly generated objects. ContGen is done using the Java Compiler Compiler [1].

The command line to generate the Java class has the following pattern:

Java ‹Java options› Contgen ‹specification file› ‹class name› 

All the user has to do is to compile the new Java source file to obtain a class that would model the desired contract. The output of ContGen is guaranteed to be a syntactically correct Java source file, but the user is responsible to include all necessary packages and to specify their classpaths.

The newly obtained class can then be used in the context of STACC to test the contract on a number of randomly generated objects. As Figure 2 shows, we use a Random Object Factory to generate instances of the required classes. This is done using reflection, following the schema in Figure 4. The idea is that we recursively look into the class with reflection, detect its constructors, choose one of them (we choose the one with most parameters), discover its parameters and try to instantiate them and, finally, using those parameters, instantiate the object according to the chosen constructor.
The command line for running the application needs to specify the name of the contract class, as well as the types of all parameters involved in the contract. It follows the pattern:

Java ‹Java options› Stacc ‹sample size› ‹contract class name› 
‹parameter type› (,‹parameter type›)* 

Note that the the ‹Java options› must include in CLASSPATH the full path to all classes or packages used by the objects involved in the contract. Experimental Results

We have tested the Statistical Contract Checker on a simple, yet meaningful class hierarchy in order to validate if it would satisfy or not the tested requirements. This class hierarchy is shown in Figure 5. We will be working directly only with instances of the class Derived, but the Random Object Factory will also go in depth and instantiate objects of member classes. We have tested 8 of the contracts mentioned in Sections 3.1, 3.2 and 3.3. To get a better idea of the usefulness of a test, we have introduced a confidence measure computes as follows: where s is the number of times the contract was satisfied, p the number of times the precondition was evaluated to true, and t the size of the sample (i.e. 1 million in our examples).

In Table 1 we show the results of testing the set of 8 contracts over a sample of 1,000,000 and in Table 2 we show the results after having introduced some errors in our programs.

First, we have modified the compareTo method, to return erroneous results when comparing different objects (see line 1 of the table). Second, we have erased the equals method and, third, we have erased the hashCode method of the class Derived. We may observe that in the erroneous implementation of class Derived, the contracts have a non-unit confidence level. This is because all, or most, of the times when the contract was 'satisfied', it was because the precondition was evaluated to false, not because the precondition actually implied the postcondition.

The execution time is the result of testing on a PentiumIII 800Mhz desktop PC with 128Mb RAM. It takes linear time with regards to the sample size.