Toy Example

This is a toy project to test Toradocu+Randoop integration. This project contains a bug that Toradocu+Randoop can discover while Randoop alone cannot.

Folder Organization and Fault Description

Under folder src you can find two Java source files: Resource.java and ResourceManager.java. Both classes are documented with Javadoc so that Toradocu can derive specification about them.

Class Resource represents a simple resource that can be locked (i.e. not available) or not. Class ResourceManager has a field of type Resource and methods that permit to interact with such resource. In particular, method canUseResource() tells whether the resource is available for use or not: the resource can be used only if it is not locked.

The Java class all.ResourceManager (all.ResourceManager.java) contains a bug:

    /**
     * Tells if it is possible to use the resource.
     *
     * @return true if the resource is not locked, false otherwise
     */
    public boolean canUseResource(){
        // bug! Should be: !resource.isLocked();
        return resource.isLocked();
    }

The return statement of method canUseResource() does not match what the Javadoc @return tag states. Randoop, by itself, is not able to detect such bug. However, when Toradocu specifications are supplied to Randoop, it will be able to detect the bug.

Prerequisites

Clone this repository:

git clone https://github.com/ariannab/toyproject

Download Randoop, and clone and build Toradocu:

wget https://github.com/randoop/randoop/releases/download/v4.0.3/randoop-all-4.0.3.jar
git clone https://github.com/albertogoffi/toradocu.git
cd toradocu
./gradlew shadowJar

Move the jars you obtained in a new folder libs under toyproject:

cd ../toyproject && mkdir libs
mv ../randoop-all-4.0.3.jar libs
mv ../toradocu/build/libs/toradocu-1.0-all.jar libs

Using Toradocu to find the fault

Be sure you are still in the toyproject folder to execute the following stesps.

1. Compile the source code:

mkdir bin/ && javac src/*/*.java -d bin/

2. Generate the Toradocu specifications over the example class:

java -jar libs/toradocu-1.0-all.jar --target-class all.ResourceManager --source-dir src/ --class-dir bin/ --randoop-specs toy-specs.json

toy-specs.json contains the specifications generated by JDoctor over class all.ResourceManager.

3. Run Randoop on the toyproject sources:

java -classpath libs/randoop-all-4.0.3.jar:bin randoop.main.Main gentests --classlist=classlist.txt --time-limit=10

Randoop generates tests and prints: "No error-revealing tests to output".

4. Now feed Randoop with the specifications generated at step 2:

java -classpath libs/randoop-all-4.0.3.jar:bin randoop.main.Main gentests --classlist=classlist.txt --time-limit=10 --specifications=toy-specs.json --stop-on-error-test

Randoop stops almost immediately because an error-revealing test is produced. You should see ErrorTest0.java in the current folder.

5. Compile and then execute the error test generated at step 4:

javac -classpath libs/randoop-all-4.0.3.jar ErrorTest0.java -sourcepath src/

java -classpath .:libs/randoop-all-4.0.3.jar:bin org.junit.runner.JUnitCore ErrorTest0

You should get the following error:

java.lang.AssertionError: Post-condition: true if the resource is not locked, false otherwise.
    at org.junit.Assert.fail(Assert.java:88)
    at org.junit.Assert.assertTrue(Assert.java:41)

Which means Randoop fed with the Toradocu specifications was able to detect the bug on the postcondition.