Efficient Contracts In Java

Here are some JavaIdioms for DesignByContract.

We'll start with a class called Contract that can be used so:

  Contract.require( 0 <= n, n + " must be at least zero" );

at the beginning of a method to check a precondition.

You might want to adjust your error message. Printing out something like "-1 must be as least zero" wouldn't be very helpful.

However, there is a potential source of inefficiency here, because both the check and the explanation string are always evaluated. Profiling shows that constructing the string takes up most of the time, which leads to:

  Contract.require( 0 <= n ? null : n + " must be at least zero" );

This version of require takes a single string argument; if it is null the condition succeeded, if it is not null the condition failed and the string explains why. Note how we avoid evaluating the string using the ?: operator.

Although this solves the biggest part of our problem, the condition is still evaluated. We can avoid that by using the technique of static final flags described in ConditionalCompilationInJava. This suggests:

  if (Contract.isEnabled)
      Contract.require( 0 <= n ? null : n + " must be at least zero" );

This will (probably) generate no code at all if Contract.isEnabled is false, provided it is declared as a static final boolean.

One variation is to not bother with the string. Instead throw an exception and use the stack trace, with its filename and line number information, to work out what the problem is. Thus:

  if (Contract.isEnabled)
      Contract.require(  0 <= n  );

Another variation is to combine the conditions and throw the exception directly:

  if (Contract.isEnabled && n < 0)
      throw new FooException(n + " must be at least zero");

Note that the test is inverted in this case (and that the opposite of "0 <= n" is "0 > n" or "n < 0", not "0 >= n" or "n <= 0").

These examples previously threw InternalError; changed to avoid any possible confusion with java.lang.InternalError, which is of course entirely inappropriate.

Contributors: MarnixKlooster, DaveHarris, KielHodges, DavisHerring?

---

I would simplify even further:

  if (Debug.ON &&  0 > n) throw new FooException(n + " must be at least zero");

Contract isn't doing much for you if it doesn't encapsulate the check. (IMHO, it ain't doing much anyway.)

I generally go one step further as I rarely worry about performance until I see an actual performance problem. I would use:

  if (0 > n) throw new FooException(n + " must be at least zero");

-- KielHodges

---

I've refactored this page quite radically, as much of the discussion reproduced stuff from ConditionalCompilationInJava. -- DaveHarris

---

DesignByContract in Eiffel is much more sophisticated than this. For example, preconditions are inherited with special rules (they can be weakened but not strengthened). -- DaveHarris

---

I've used an approach where the pre and post conditions could easily be turned on and off through comments. For example, a push method on a stack class might look like this ...

    void push (int n) {
        Require.that (!isFull());
        int oldCount = count();

        itsData[itsCount] = n;
        itsCount++;

        //Ensure.that (count() != oldCount+1);
        //Ensure.that (top() != n);
    }

Here, the precondition is enabled and the postconditions are commented out. A simple script is used to switch the conditions on and off. It requires recompiling the code to switch, but that never seemed to be a big problem. For examples, see http://w3.one.net/~jweirich/java/javadbc/java-dbc.html . -- JimWeirich

---

seems to me that the assert keyword does this for you.