Contracts for Java

If you’ve ever spent hours debugging your Java code, today’s blog post is for you.

Often bugs that are frustratingly elusive and hard to track down appear simple or even trivial once you have found their cause (the fault). Why are those bugs hard to track down? One possibility is that the fault is in a completely different part of the program than its symptom (the failure).


Contracted code reveals failures much closer to their fault, leaving you with a far simpler problem to solve:

Traditionally, Java programmers enforced preconditions using explicit parameter validation code in public methods, and assertions in non-public methods. Likewise, they enforced invariants and postconditions using assertions. This approach is described in detail here. Since then, new features in Java 5 have enabled a more convenient and expressive implementation of contracts.

Contracts for Java is our new open source tool. Preconditions, postconditions, and invariants are added as Java boolean expressions inside annotations. By default these do nothing, but enabled via a JVM argument, they’re checked at runtime.

• @Requires, @Ensures, @ThrowEnsures and @Invariant specify contracts as Java boolean expressions
• Contracts are inherited from both interfaces and classes and can be selectively enabled at runtime

Contracts help you turn interface documentation into code. For example:

/**
* @param left a sorted list of elements
* @param right a sorted list of elements
* @return the contents of the two lists, merged, sorted
*/
List merge(List left, List right);

Could be expressed as:

@Requires({
"Collections.isSorted(left)",
"Collections.isSorted(right)"
})
@Ensures({
"Collections.containsSame(result, Lists.concatenate(left, right))",
"Collections.isSorted(result)"
})
List merge(List left, List right);

The interface is now precise and every class that implements it can be checked at runtime.

Contracts are a powerful language feature and can provide great benefit if used correctly. We recommend that newcomers find an expert to learn from or spend some time reading around the subject to pick up good habits and avoid bad ones.

One point that often surprises people is that contracts must not be used to validate data. Contracts exist to check for programmer error, not for user error or environment failures. Any difference between execution with and without runtime contract checking (apart from performance) is by definition a bug. Contracts must never have side effects.

Another important point is that by convention module interfaces in Java are total, that is, they are defined for all input. In the case of incorrect input, they promise that a particular exception will be thrown. This behavior remains part of each method’s implementation and cannot be moved to the contract.

Contracts for Java is based on Modern Jass by Johannes Rieken. Rather than being a full time project it was conceived and developed in the 20% time of two software engineers and then developed further through an internship. The internship report (PDF) goes into detail about the work done and the methodologies used.

Contracts for Java was inspired by Eiffel, a language invented by Bertrand Meyer, which has built in support for contracts.

By David Morgan, Andreas Leitner and Nhat Minh Le, Contracts for Java 20% Team