Contracts in Java using iContract

April 13, 2008

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.

Read the rest of this entry »

Advertisements

When Robots Go to Law School…

April 13, 2008

…they learn how to write contracts! Well, I wanted to use something a little different from the typical customers and orders, so I came up with an example from the field of swarm robotics for my upcoming posts on design by contract tools.

Disclaimer: This example is only for illustration and not meant to be useful for any real robotics application.

The following UML class diagram (created with NetBeans) shows a simple object model for robots and swarms. Each Robot may or may not belong to a Swarm, and a swarm can consist of any number of robots. The AbstractRobot class implements some common functionality defined by the Robot interface and serves as the base class for two concrete robot implementations: Navigator and Worker.
Robots class diagram

The Navigator is equipped with a GPS system that enables it to determine its own location. The Worker‘s unique feature is its robot arm that allows it to pick up and manipulate objects. So each of these specialized robots has only limited functionality, but when working together in a swarm they are much more powerful. For example, consider the task of picking up an object from a specific location and dropping it off somewhere else. Neither one of these two robot types could perform this task by itself, because the navigator cannot pick up objects, and the worker does not know how to get to the object’s location. But if they work together, the navigator can lead the way to the object, and the worker can then pick up the object.

Read the rest of this entry »


Smart Objects Put their Contracts in Writing

March 10, 2008

When you write a function or method that is going to be called from other people’s code, then you would want to let them know how to use it, right? If you are using Java, the typical way of doing that would be to document your method in a JavaDoc comment. As an example, consider the specification for the Arrays.binarySearch method in the Java API. It clearly states that the array that you pass into this method must be sorted in order for the method to work correctly. This is what the method expects from its caller. The documentation goes on to explain what values the method returns under which conditions. This is what the caller can expect from the method. You can think of these mutual expectations as forming a contract between the method (service provider) and the caller (client, service consumer). The service provider basically tells the client: As long as you ensure X before calling my method, I guarantee Y when my method returns. X is known as the precondition, Y as the postcondition.

Read the rest of this entry »