Design by Contract in Java with Google

Design by Contract in Java with Google

By Lance Finney, OCI Principal Software Engineer

September 2011

Introduction

Design by Contract™ is an approach to designing robust yet simple software. It provides methodological guidelines to achieve these goals without resorting to defensive programming. Instead, Design by Contract builds class invariants and pre/post validation of methods arguments and return values into the code itself.

Design by Contract received a lot of attention when it was initially released, but it has never become a significant approach in most languages (the most obvious exception is Eiffel, which was built around Design by Contract).

Several libraries have been introduced for using DbC in Java, but none ever gained mass acceptance. However, a new library called Contracts for Java has been introduced by Google. With Google's weight behind it, perhaps this implementation will finally bring Design by Contract to the attention of the general Java community.

Design By Contract

Design by Contract (DbC) was introduced in the mid 1980s in the Eiffel language by Bertrand Meyer, a French computer scientist. The goal of DbC is to enable programmers to "build software specification into the software source code and make it self-checking at runtime." This is achieved through the introduction of "contracts" — executable code contained within the source that specifies obligations for classes, methods, and their callers.

The primary advantage of DbC is that contracts and obligations are made explicit instead of implicit. For example, many methods have an implicit requirement that an argument be non-null (though there are many tools that add support for this through annotations, none are standard yet). With contracts, these requirements are fully documented and enforced in the code itself.

DbC generally provides three types of validations:

Preconditions
Preconditions specify conditions that must be true before a method can execute. These conditions can be imposed upon the arguments passed into the method or upon the state of the called class itself. Preconditions impose obligations on the client of the method; if the conditions are not met, it is a bug in the client.
Postconditions
Postconditions specify conditions that must be true when a method is finished executing. These conditions can involve the current class state, the class state as it was before the method was called, the method arguments, and the method return value. Postconditions impose obligations on the method; if the conditions are not met, it is a bug in the method.
Invariants
Invariants specify conditions that must be true of a class whenever it is accessible to a client (specifically when the class has finished loading and whenever its methods are called).

Additionally, Eiffel provides more types of validation than these standard types, such as invariants and variants for loops. We will see later that Contracts for Java does not share this feature. However, Contracts for Java instead adds validations on thrown exceptions.

Some of these features can be implemented in Java with simple assertions, but contracts are more powerful for several reasons:

Contracts for Java

Contracts for Java is a new open-source library released by Google to bring DbC to Java (this library is based on Johnannes Rieken's older Modern Jass library). As mentioned above, this is not the first DbC library introduced for Java, but it has a major advantage over many of the previous implementations: the introduction of Pluggable Annotation Processing in Java 6. This means that the contracts can be written within annotations that are compiled and executed as part of the bytecode. Older implementations used other mechanisms like methods named by convention, instrumenting comments, or using a custom compiler. Processed annotations are better integrated into Java, so they should be more robust without needing to jump through as many hoops.

Contract Annotations

As mentioned earlier, Contracts for Java supports the three main types of DbC validation: preconditions, postconditions, and invariants. It does not support some Eiffel extensions like loop validation, but it does add a special postcondition check for exceptions when they are thrown:

Annotation Type Comments
com.google.java.contract.Invariant Invariant Checked after the constructor and at the start and end of all public and package-private methods
com.google.java.contract.Requires Precondition Checked at the start of the annotated method
com.google.java.contract.Ensures Postcondition Checked at the end of the annotated method
com.google.java.contract.ThrowEnsures   Exceptional postcondition Checked at when an exception has been thrown

The content of each validation is expressed in String arguments to the annotation. Using Strings for the validation is definitely a compromise - in Eiffel, the contracts are expressed in full normal language syntax. While it feels strange at first to write executable Java code within quotation marks, it is not as bad as it initially seems, because the Contracts for Java compilation step gives appropriate and understandable error messages (see below for information on how to set this up). The Java code can validate any visible state of the Object, including static state.

There are two forms of the syntax: the "Simple form" to use when there's only one expression and the "Multi-clause form" to use with more than one expression.

Example

To demonstrate using Contracts for Java, we will look at a very primitive shopping cart for an online bookseller. First, we look at the very simple definition of a Book, which contains only title and price information.

package com.ociweb.sett.sep2011;
 
import com.google.java.contract.*;
import org.apache.commons.lang3.builder.EqualsBuilder;
import org.apache.commons.lang3.builder.HashCodeBuilder;
 
 
@Invariant({"title != null && title.length() > 0", "price > 0"})
public class Book {
    private final String title;
    private int price;
 
    @Requires({"title != null && title.length() > 0", "price > 0"})
    public Book(String title, int price) {
        this.title = title;
        this.price = price;
    }
 
    public int getPrice() {
        return price;
    }
 
    @Requires("price > 0")
    public void setPrice(int price) {
        this.price = price;
    }
 
    public String getTitle() {
        return title;
    }
 
    @Override
    public boolean equals(Object obj) {
        // boilerplate implementation from Apache Commons Lang
        return EqualsBuilder.reflectionEquals(this, obj, "price");
    }
 
    @Override
    public int hashCode() {
        // boilerplate implementation from Apache Commons Lang
        return HashCodeBuilder.reflectionHashCode(this, "price");
    }
}

This class uses the @Invariant and @Requires contract types to ensure that a Book has a legal title and price (defined solely as a non-empty title and a positive price).

The @Invariant and the constructor's @Requires appear to be identical. However, the @Requires validation is enforced on the constructor's arguments, whereas the @Invariant validation is enforced on the instance fields. So, although they have redundant effect in this particular example, both are probably worth keeping because there is a semantic difference.

The validation on the @Requires for setPrice() functions similar to constructor's @Requires. However, note that the syntax is slightly different. Because setPrice() has only one expression, we can use the "Simple form" without the braces that are necessary for the constructor's multiple expressions.

Incidentally, this class also uses EqualsBuilder and HashCodeBuilder from Commons Lang to simplify using a Book as the key in a collection in the following code.

Now that we have our simple Book class defined with our validations, we can use it in our simple Shopping Cart below:

package com.ociweb.sett.sep2011;
 
import com.google.common.collect.*;
import com.google.java.contract.*;
 
@Invariant("books != null")
public class ShoppingCart {
    private final Multiset<Book> books = HashMultiset.create();
 
    @Requires("book != null")
    @Ensures("books.count(book) == old(books.count(book)) + copies")
    public void addBooks(Book book, int copies) {
        books.add(book, copies);
    }
 
    @Requires({"book != null", "books.count(book) >= copies"})
    @Ensures("books.count(book) == old(books.count(book)) - copies")
    public void removeBooks(Book book, int copies) {
        books.remove(book, copies);
    }
 
    @Requires("book != null")
    @Ensures("books.count(book) == old(books.count(book)) - copies")
    @ThrowEnsures("books.count(book) == old(books.count(book))")
    public void removeBooksUnsafe(Book book, int copies) {
        if (books.count(book) >= copies) {
            books.remove(book, copies);
        } else {
            throw new IllegalStateException("Not enough books to remove");
        }
    }
 
    @Ensures("result >= 0")
    public int getTotal() {
        int total = 0;
        for (Book book : books) {
            total += book.getPrice() * books.count(book);
        }
        return total;
    }
 
    public static void main(String[] args) {
        Book hp = new Book("Harry Potter and the Goblet of Fire", 10);
        Book hhg = new Book("The Hitchhiker's Guide to the Galaxy", 12);
        Book lotr = new Book("The Two Towers", 15);
 
        ShoppingCart cart = new ShoppingCart();
        cart.addBooks(hp, 1);
        cart.addBooks(hhg, 2);
        cart.addBooks(lotr, 3);
        System.out.println("initial total = " + cart.getTotal());
 
        cart.removeBooks(hp, 1);
        System.out.println("total after removing = " + cart.getTotal());
 
        try {
            cart.removeBooksUnsafe(hhg, 4);
        } catch (IllegalStateException e) {
            System.out.println("error message: " + e.getMessage());
        }
        System.out.println("total after exception = " + cart.getTotal());
 
 
        System.out.println("\n//precondition violated here - only two books in the cart");
        cart.removeBooks(hhg, 4);
    }
}

This class has a lot more going on in it, so let's go through it piece by piece.

@Invariant("books != null")
public class ShoppingCart {
    private final Multiset<Book> books = HashMultiset.create();

We define a class invariant requiring that the books property be not null. Since books is a final field and is instantiated when it is declared, we know that this invariant will never be violated. However, that wouldn't necessarily be true if the implementation changed, and the invariant protects against such an accidental change.

Note that books is a HashMultiset, a useful Collection from Google Guava that allows duplicates and keeps a count of them. With this data structure, we have a shopping cart that is capable of holding books and keeping track of the number of copies of each title in the cart.

@Requires("book != null")
@Ensures("books.count(book) == old(books.count(book)) + copies")
public void addBooks(Book book, int copies) {
    books.add(book, copies);
}
 
@Requires({"book != null", "books.count(book) >= copies"})
@Ensures("books.count(book) == old(books.count(book)) - copies")
public void removeBooks(Book book, int copies) {
    books.remove(book, copies);
}
 
@Requires("book != null")
@Ensures("books.count(book) == old(books.count(book)) - copies")
@ThrowEnsures("books.count(book) == old(books.count(book))")
public void removeBooksUnsafe(Book book, int copies) {
    if (books.count(book) >= copies) {
        books.remove(book, copies);
    } else {
        throw new IllegalStateException("Not enough books to remove");
    }
}

These three methods show full use of the preconditions and postconditions.

All three method enforce the precondition that the book argument be not null. For addBooks and removeBooksUnsafe, this is the only precondition, so they can use the "Simple form" syntax. removeBooks adds an additional precondition that you can't remove books that aren't in the cart to begin with.

All three methods ensure the correct implementation through postconditions: addBooks makes sure that the expected number of copies were added to the cart for the title, and removeBooks and removeBooksUnsafe both make sure that the expected number of copies were removed from the cart for the title. These postconditions use a special keyword from Contracts for Java: old. This keyword can be used in @Ensures and @ThrowEnsures to interrogate the value of an expression as it existed when the method started.

So, for example, if we call addBooks with three copies of a particular title that is new to the cart, we can be sure that the method correctly added three copies of that title to the cart's internal data structure. This will work because books.count(book) == old(books.count(book)) + copies will resolve to 3 == 0 + 3, which is correct.

Finally, removeBooksUnsafe uses an annotation that is unique in our example: @ThrowEnsures. In this mock shopping cart, there are two methods to remove copies, and they have different semantics:

Which of these implementations is the better choice? That's a design decision that depends on the needs of the project. However, by providing @ThrowEnsures, Contracts for Java gives the flexibility of this choice.

@Ensures("result >= 0")
public int getTotal() {
    int total = 0;
    for (Book book : books) {
        total += book.getPrice() * books.count(book);
    }
    return total;
}

This method calculates the total cost of all the books in the shopping cart. For our purposes, the interesting new feature is contained in the postcondition, the result special keyword. This keyword is usable only in @Ensures. In this case, this postcondition confirms that the total returned by the method is never negative.

Finally, here is a main method that exercises the code. This test code creates three different books that have varying prices and adds a few copies of each to a ShoppingCart via addBooks. After checking the total price via getTotal, it removes one of the books via removeBooks and checks the price again. At the end, it attempts to remove too many copies of one of the books using both removeBooksUnsafe (which throws an exception) and removeBooks (which has a precondition that is being violated).

public static void main(String[] args) {
    Book hp = new Book("Harry Potter and the Goblet of Fire", 10);
    Book hhg = new Book("The Hitchhiker's Guide to the Galaxy", 12);
    Book lotr = new Book("The Two Towers", 15);
 
    ShoppingCart cart = new ShoppingCart();
    cart.addBooks(hp, 1);
    cart.addBooks(hhg, 2);
    cart.addBooks(lotr, 3);
    System.out.println("initial total = " + cart.getTotal());
 
    cart.removeBooks(hp, 1);
    System.out.println("total after removing = " + cart.getTotal());
 
    try {
        cart.removeBooksUnsafe(hhg, 4);
    } catch (IllegalStateException e) {
        System.out.println("error message: " + e.getMessage());
    }
    System.out.println("total after exception = " + cart.getTotal());
 
 
    System.out.println("\n//precondition violated here - only two books in the cart");
    cart.removeBooks(hhg, 4);
}

Here's the output from calculation, which demonstrates the total cost calculations, the error message from the expected exception, and the exception thrown when a Contracts for Java contract is violated by a client:

>> initial total = 193
>> total after removing = 183
>> error message: Not enough books to remove
>> total after exception = 183
>>
>> //precondition violated here - only two books in the cart
>> Exception in thread "main" com.google.java.contract.PreconditionError: books.count(book) >= copies
>>    at com.ociweb.sett.sep2011.ShoppingCart.removeBooks.<pre>(ShoppingCart.java:16)
>>    at com.ociweb.sett.sep2011.ShoppingCart.removeBooks(ShoppingCart.java)
>>    at com.ociweb.sett.sep2011.ShoppingCart.main(ShoppingCart.java:64)

Compilation and Execution

Unlike many open source libraries, Contracts for Java doesn't work by simply adding a jar file to the classpath. Instead, as mentioned above, Contracts for Java integrates through Pluggable Annotation Processing. In order to compile your code to add the contracts to the bytecode, use the following argument to the javac command:

javac -processor com.google.java.contract.core.apt.AnnotationProcessor YourClass.java

Compilation fully checks the Java code included within the annotation's String and gives useful messages if there is an error. For example, if I had accidentally mistyped "title" in the precondition for Book's constructor, I would have received the following compilation failure message:

   error in contract: com.google.java.contract://com.google.java.contract/com/ociweb/sett/sep2011/Book.java:36:
        cannot find symbol variable tile
@Requires({"tile != null && title.length() > 0", "price > 0"})
^

To run the compiled application with the annotations turned on, use the following argument to the java command:

java -javaagent:path/to/agent.jar YourMainClass

Of course, this can get ungainly with many files. Fortunately, you can set up these commands inEclipse and IntelliJ IDEA using direction from links on the Contracts for Java home page. Unfortunately, neither IDE has code completion and other features of full integrations at this point, but it might come later through plugins.

If we don't include the javaagent argument to the java command, then the contract validations are turned off. This is likely how you would want to run your applications in the production environment, just as you likely run with Java assertions disabled.

Conclusion

Design by Contract is a powerful approach for building simple and robust software. Contracts for Java isn't the first attempt to bring this approach to Java, but it's a simple and powerful implementation that might become a standard tool for ensuring Java software validity.

References

Notes

Contracts for Java is a very young open-source project. The code in this article was built using the development snapshot revision 138. Since this was a development snapshot and not a released version, the API should be considered extremely fluid. Therefore, code examples in this article likely will not work in future versions.

The examples given here used version 0.9 of Google Guava and version 3.0 of Commons Lang.

Design by Contract™ is a registered trademark of Eiffel Software in the United States.