Contracts in Java using iContract

When searching for design by contract tools for Java, the first one I came across was iContract. There is a good article at JavaWorld that describes how to use iContract, but unfortunately the link it contains for downloading iContract no longer works. Apparently iContract has been abandoned by its creators for a while, but it has been revived as JContractS. I have used JContractS to create my example below, but I am still referring to it as iContract since this name is well established, and JContractS seems to be functionally equivalent to the original iContract.

iContract uses the special Javadoc tags @pre and @post to specify a method’s preconditions and postconditions (see my earlier post for an introduction to these terms). There is also an @invariant tag that can be used on the class level to specify a common condition that must hold before and after any of the class’s methods are executed.

Let’s See some Code

The following example code is based on the swarm robotics example described in my previous post. iContract does not support the new language features of Java 5, so I adapted my example to Java 1.4 syntax. I am only going to include some code snippets here to show how to use iContract, but you can get the full source code for this example from my Subversion repository or download it as a zip file. All you need to run this example is JDK 1.4 (or higher) and Ant.

Simple Conditions

The hasFeature method in the Robot interface is used to check whether a robot has a specific feature. It expects its argument to be one of the predefined constants in the FEATURES array. Using the Arrays.binarySearch method (which returns a non-negative result if the value is found in the array), this precondition can be specified as follows:


    /**
     * @pre java.util.Arrays.binarySearch(FEATURES,
     *      feature) >= 0
     */
    public boolean hasFeature(int feature);

A Robot may be part of a Swarm, which is returned by the getSwarm method. The return value must be either null (if the robot does not belong to a swarm), or it must be a Swarm instance whose members (given by its getRobots method) include this robot. This postcondition can be specified as follows:

    /**
     * @post return == null ||
     *       return.getRobots().contains(this)
     */
    public Swarm getSwarm();

Implications

The postcondition of the getSwarm method can be expressed in another way: If this method returns a non-null value, then it must be a swarm that includes this robot among its members. This kind of condition can be expressed in iContract using the implies operator. With this operator, the above condition could be rewritten as follows:

return != null implies return.getRobots().contains(this)

The implies operator is also used in the precondition of the setSwarm method. This precondition is supposed to prevent people from calling setSwarm directly when they want to add a robot to a swarm. Instead, they should call the addRobot method in the Swarm class, which adds the robot to its list of members and then calls Robot.setSwarm.


    /**
     * @pre swarm != null implies
     *      swarm.getRobots().contains(this)
     * @post getSwarm() == swarm
     */
    public void setSwarm(Swarm swarm);

Pre-State Values

For methods that modify an object’s state, it often makes sense to specify the postcondition in terms of how the new state relates to the state before method execution (the pre-state). To express this kind of postcondition, iContract supports the @pre operator, which can be appended to an expression and represents the expression’s value before method execution. For example, after executing the addRobot method in the Swarm class, the swarm’s collection of members should contain the newly added robot, as well as all the robots it already contained before (but no others). Using the @pre operator to express these postconditions, the method would look like this:


    /**
     * @pre robot.getSwarm() == null
     * @post getRobots().contains(robot)
     * @post getRobots().containsAll(getRobots()@pre)
     * @post getRobots().size() ==
     *       1 + getRobots().size()@pre
     */
    public void addRobot(Robot robot) {
        robots.add(robot);
        robot.setSwarm(this);
    }

Quantifiers

There are two ways to tell that a given Robot instance belongs to a given Swarm instance: the robot’s getSwarm method returns the swarm, and the robot is contained in the collection returned by the swarm’s getRobots method. To ensure that the two sides of this relationship are always consistent, we can define an invariant for the Swarm class using the forall quantifier. This quantifier specifies a condition (after the vertical bar) that must be satisfied for all elements in a collection:


/**
 * @invariant forall Robot r in getRobots() |
 *            r.getSwarm() == this
 */
public class Swarm {
    // ...
}

Besides the forall quantifier, iContract supports the exists quantifier, which only requires that at least one element of a collection satisfies the given condition. By nesting the exists quantifier n times, you can specify that at least n elements of a collection must satisfy the condition. This approach is used in the precondition for the Robot‘s getLocation method, which specifies that in order to determine its location, a robot must either have a GPS device or be part of a swarm in which at least 3 other robots have GPS devices, from which it could triangulate its location:


    /**
     * @pre !hasFeature(FEATURE_GPS) implies
     *      exists Robot a in getSwarm().enumRobots()|
     *      exists Robot b in getSwarm().enumRobots()|
     *      exists Robot c in getSwarm().enumRobots()|
     *      a != b && a != c && b != c &&
     *      a.hasFeature(FEATURE_GPS) &&
     *      b.hasFeature(FEATURE_GPS) &&
     *      c.hasFeature(FEATURE_GPS)
     * @post return != null
     */
    public Point2D getLocation();

To make this work, I had to add the enumRobots method to the Swarm class, which returns the swarm’s robots as a java.util.Enumeration. For some reason, iContract wouldn’t accept this condition when using the getRobots method instead of enumRobots.

Runtime Checking

Let’s see what happens when a contract is violated at runtime, for example when we try to directly call Robot.setSwarm instead of going through Swarm.addRobot:


    public static void main(String[] args) {
        Worker worker = new Worker();
        Swarm swarm = new Swarm();
        worker.setSwarm(swarm);
    }

Note: The Worker class implements the Robot interface. As you would expect (based on the Liskov substitution principle), iContract automatically applies the contracts defined in the Robot interface to the Worker class.

In order to enable runtime checking of the contracts, the source code needs to be instrumented with the iContract tool (see the build.xml file for details on how it is invoked). This step results in a new set of source files with embedded code for checking the contracts. When compiling and running these instrumented source files, a RuntimeException is thrown at the beginning of the setSwarm method, indicating that its precondition was violated.

Contract Documentation

Contract specifications can be included in the Javadoc documentation by using iDoclet. However, this only seems to work with JDK 1.3, not with any newer version.

Discussion

What I like about iContract is the declarative language with its logic operators, similar to OCL. This kind of language should be more suitable for static analysis techniques than other contract tools that are based on more general scripting languages. However, I’m not aware of any existing static analysis tools for iContract. There is also nothing to keep you from using arbitrary Java methods in your contract specifications, including methods with side effects.

There are some drawbacks inherent in iContract’s approach of embedding contract specifications in Javadoc comments. First of all, it means that any tool operating on contracts needs to have access to the source code. But contract specifications should really be included in the byte code of a class, since they are part of its public interface. In a perfect world, I would imagine that third-party jar files come with embedded contract specifications that could be seamlessly included in any sort of runtime or static contract checking that you apply to your project, along with the contracts in your own code.

Another problem with specifying contracts within comments is that you don’t get IDE support (such as code completion, syntax checking, refactoring) when writing contracts. Of course this problem could be addressed by special IDE plug-ins, but I’m not aware of any such plug-ins for iContract.

As mentioned above, runtime checking of contracts requires source code instrumentation as a preprocessing step before compilation. This means that, unlike with standard Java assertions, contract checking cannot be enabled or disabled at runtime.

Unfortunately, iContract proved unsuitable for my professional work, mainly because it does not support Java 5 syntax and is no longer actively developed.

Overall, my impression of iContract is that it was an early implementation of design by contract for Java, making best use of what was available at the time. But from today’s perspective, iContract’s approach seems somewhat outdated, and I think that some of its limitations could be overcome by leveraging more recent developments, such as annotations, aspect-oriented programming, the Java Scripting API and instrumentation support. In fact, there are several newer tools based on these technologies, and I will be reviewing some of them in upcoming posts.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: