Preconditions, Postconditions, Invariants : Design by Contract for Java

In his famous book Object-Oriented Software Construction Bertrand Meyer described a design technique called "Design by Contract" (DBC) which can improve software quality dramatically. His programming language Eiffel supports this design technique inherently. This valuable technique is universal and widely accepted and can be used regardless in which programming language you are developing. To apply this technique in Java you need to define and execute assertions at runtime. The pre-, and postconditions of a method should also be part of the javadoc documentation.

There are a lot of tools and framework which help you to apply DBC to your Java code. For example OVal, Contract4J, which are using AspectJ, iContract or Jass, which are using a preprocessor for Java.

In some circumstances it might be too much effort to apply one of these tools to you development project. Luckily there was a rudimentary support for testing assertions added to the Java language starting with release 1.4. The assert statement allows to define runtime checks inside your code. With some simple conventions you can benefit from DBC without heavy tool support. Here is an example how to use the assertion mechanism of Java to apply "Design by Contract":

/**
* Is the editor in the edit mode?
* @return True, if the editor is in the edit mode. Otherwise false.
*/
public boolean isInEditMode() {
 ...
}

/**
* Sets a new text.
* Precondition: isEditMode()
* Precondition: text != null
* Postcondition: getText() == text
* @param name
*/
public void setText(String text) {
 assert isInEditMode() : "Precondition: isInEditMode()";
 assert text != null : "Precondition: text != null";

 this.text = text;

 assert getText() == text : "Postcondition: getText() == text";
}


/**
* Delivers the text.
* Precondition: isEditMode()
* Postcondition: result != null
* @return
*/
public String getText() {

 assert isInEditMode() : "Precondition: isInEditMode()";

 String result = text;

 assert result != null : "Postcondition: result != null";
 return result;
}

So you can use "Design by Contract" effectively with three simple rules:

• Use the assert mechanism of Java to check preconditions, postconditions and invariants at runtime.
• Describe each assert with a string that starts either with "Precondition:", "Postcondition:" or "Invariant:" followed by the textual description of the assert expression.
• Add each assert description string to the javadoc comment of the method

We can get a little more support, when we write our own pre- and postcondition class:

public class Assertion {

   /**
    * Precondition.
    * @param condition we expect to be true.
    * @param description repeats the condition or describes it in
    * other words.
    */
   public static void Require(boolean condition, String description) {
       if (!condition) {
           throw new RuntimeException("Precondition: The expectation '" + description + "' is violated");
       }
   }
  
   /**
    * Precondition.
    * @param objectToBeTested is an object we expect to be not null
    * @param objectName is the name of the variable we test.
    */
   public static void RequireNotNull(Object objectToBeTested,String objectName) {
       if (objectToBeTested == null) {
           throw new RuntimeException("Precondition: The expectation '" + objectName + " is not null' is violated");
       }
   }

   /**
    * Postcondition.
    * @param condition we expect to be true.
    * @param description repeats the condition or describes it in
    * other words.
    */
   public static void Ensure(boolean condition, String description) {
       if (!condition) {
           throw new RuntimeException("Postcondition: The expectation '" + description + "' is violated");
       }
   }

   /**
    * Common condition to be used in the middle of methods
    * @param condition we expect to be true.
    * @param description repeats the condition or describes it in
    * other words.
    */
   public static void Check(boolean condition, String description) {
       if (!condition) {
           throw new RuntimeException("Condition: The expectation '" + description + "' is violated");
       }
   }
}

Using this class instead of 'assert' has the advantage that we can't forget to switch on the runtime checking of the assertions with -enableassertions. But keep in mind you still have to add method comments for the assertions. This is important, because the assertions should help the users of your class without forcing them to read your implementation details:

/**
* Sets a new text.
* Require: isEditMode()
* Require: text != null
* Ensure: getText() == text
* @param name
*/
public void setText(String text) {
 Assertion.Require(isInEditMode(),"isInEditMode()");
 Assertion.RequireNotNull(text, "text");

 this.text = text;

 Assertion.Ensure(getText() == text,"getText() == text");
}


/**
* Delivers the text.
* Require: isEditMode()
* Ensure: result != null
* @return
*/
public String getText() {

 Assertion.Require(isInEditMode(),"isInEditMode()");

 String result = text;

 Assertion.Ensure( result != null, "result != null";
 return result;
}

There is also an article "Using Assertions in Java Technology" on the Sun Developer network. See "Preconditions, Postconditions, Invariants : Design by Contract for Java #2" for further infos.