Tutorial

Download dbc_example.zip
Download dbc_example.tar.gz
Check out iContract Extras

This is a short tutorial in how to use iContract, iControl and iDoclet with Jakarta Ant. You'll need to investigate the source code of the example to understand what's going on.

Before you start, you should make sure you have installed Jakarta Ant 1.3 or above. Download it from http://jakarta.apache.org/
If you're using Ant 1.3, you'll have to replace the ant.jar and optional.jar files with a patched version that includes the icontract task.
The patched versions are here:
ant.jar
optional.jar
If you have Ant 1.4 or above, you shouldn't patch, as the icontract task is part of the Ant distribution.

So far for Ant. In addition you'll have to copy the following jar files to the devlib directory of this tutorial:

iContract-jdk1_2.jar The iContract preprocessor
iControl.jar A GUI that lets you adjust what parts of your code iContract will instrument (preprocess)
iDoclet.jar A doclet that includes assertions in the JavaDoc (HTML API documentation)

(I usually keep two library directories for my projects: devlib for "development libraries" and lib for "runtime libraries").

Ok, you should be ready to start exploring the wonders of Design By Contract. The example consists of some interfaces and classes that have iContract assertions. They implement a ridiculously simple airline reservation system. -And there are a few bugs in that system that we'll discover and fix with help from DBC. First, let's compile the classes and make sure all assertions are disabled:

build instrument

This will create a file called icontrol.properties in the same directory as the build.xml file. (It will also instrument a copy of the source files and compile them, but don't worry about that for now). Now, let's fire up iControl and create the control file that will tell iContract what parts of the code should be processed.

build icontrol

This will start iControl. Play around with iControl for a while. Make sure all check boxes are off before you quit and save.

Now, you're ready to run the example without assertions. Check in a passenger with light luggage. Open a new console and type:

build run-light

then

build run-heavy

Both times you'll get a message indicating that the passenger was successfully taken to his destination. That's nice, but the program has bugs in it, and you never discovered it. Let's try to enable the assertions and see what happens. Check all assertions in the com.bekk.dbcdemo package and click 'Save' to save the settings. Check in a passenger with light luggage:

build run-light

This results in a postcondition violation. That indicates a bug in the class that fired the postcondition violation error, namely the FlightImpl class. According to the specification (the contract) of Flight, the last postcondition of the accept method states that accepting a passenger should result in the total number of passengers being incremented by one. FlightImpl does not fulfill this contract, and therefore you get a postcondition violation. Edit FlightImpl's implementation of the accept method, and run the same target again:

build run-light

This time, you shouldn't get any errors. Now, try the passenger with heavy language again:

build run-heavy

This time you should get a precondition violation. This means there is a bug in the class that called the method firing the precondition violation. The sinner is Client. Client didn't make sure the Passenger has less or equal to the maximum allowed hand luggage weight before checking in. Fix the bug in Client and run the same target again:

build run-heavy

Now, you have corrected two bugs thanks to iContract! Let's say you were writing the Client.java class from scratch, and that the Other classes were
already written by someone else. How can you know what the contracts are without having to read to the code? iDoclet comes to rescue. iDoclet is an extension of Sun's standard doclet which includes documentation for the contracts in the generated JavaDocs. Let's generate JavaDocs for the example classes:

build javadocs

Take a look at the API documentation under the build/api directory. See the contracts?

That's it, really! You have used iContract, iControl and iDoclet - all managed by Ant. You can use the build.xml file as a template for your own project. Good luck!