Design by Contract in Java with Examples

Introduction

What is Design by Contract

• Preconditions: what must be true when the method is called. Ensuring them is the caller's obligation, and the method may assume them. For example, the number of leave days requested must be positive and not more than the balance.
• Postconditions: what the method guarantees when it returns, provided the preconditions held. Ensuring them is the method's obligation, and the caller may rely on them. For example, the balance is reduced by exactly the days taken.
• Class invariants: what is always true of every object of the class - after construction, and before and after every public method call. For example, the balance is never negative and never above the yearly allowance.

Why contracts help

• What may I pass? The preconditions are the method's real input rules, beyond what the parameter types say.
• What will I get? The postconditions say exactly what the method does, which is also exactly what its tests should check.
• Whose bug is it? A failed precondition is a bug in the caller; a failed postcondition or invariant is a bug in the method. When a contract check fails, you know where to look.

Example - a leave account with a checked contract

//DesignByContract.java
public class DesignByContract {

  // Small helpers that make the contract checks readable
  static final class Contract {
    static void require(boolean condition, String rule) {     // the caller's obligation
      if (!condition) throw new IllegalArgumentException("Precondition failed: " + rule);
    }
    static void ensure(boolean condition, String rule) {      // the method's obligation
      if (!condition) throw new AssertionError("Postcondition failed: " + rule);
    }
    static void invariant(boolean condition, String rule) {   // always true
      if (!condition) throw new AssertionError("Invariant broken: " + rule);
    }
  }

  static class LeaveAccount {
    private final int allowance;
    private int balance;

    LeaveAccount(int allowance) {
      Contract.require(allowance > 0, "allowance > 0");
      this.allowance = allowance;
      this.balance = allowance;
      Contract.invariant(balanceInRange(balance), "0 <= balance <= allowance");
    }

    /**
     * Requires: 0 < days <= balance().
     * Ensures:  balance() == old balance() - days.
     */
    void take(int days) {
      Contract.require(days > 0, "days > 0, but was " + days);
      Contract.require(days <= balance,
          "days <= balance (" + balance + "), but was " + days);

      int newBalance = deduct(balance, days);

      Contract.ensure(newBalance == balance - days, "balance == old balance - days");
      Contract.invariant(balanceInRange(newBalance), "0 <= balance <= allowance");
      balance = newBalance;                 // committed only when the contract holds
    }

    int deduct(int from, int days) { return from - days; }

    int balance() { return balance; }

    private boolean balanceInRange(int value) { return 0 <= value && value <= allowance; }
  }

  // A subclass with a bug: it rounds leave up to whole weeks of 5 days
  static class WeeklyLeaveAccount extends LeaveAccount {
    WeeklyLeaveAccount(int allowance) { super(allowance); }

    @Override
    int deduct(int from, int days) { return from - ((days + 4) / 5) * 5; }
  }

  static void attempt(String label, Runnable action) {
    try {
      action.run();
      System.out.println(label + " -> ok");
    } catch (IllegalArgumentException | AssertionError e) {
      String error = e.getClass().getSimpleName();
      System.out.println(label + " -> " + error + ": " + e.getMessage());
    }
  }

  public static void main(String[] args) {
    LeaveAccount tom = new LeaveAccount(20);
    attempt("Tom takes 3 days ", () -> tom.take(3));
    System.out.println("Tom's balance: " + tom.balance());
    attempt("Tom takes 0 days ", () -> tom.take(0));
    attempt("Tom takes 30 days", () -> tom.take(30));

    LeaveAccount harry = new WeeklyLeaveAccount(20);
    attempt("Harry takes 3 days", () -> harry.take(3));
    System.out.println("Harry's balance: " + harry.balance());
  }
}

Tom takes 3 days  -> ok
Tom's balance: 17
Tom takes 0 days  -> IllegalArgumentException: Precondition failed: days > 0, but was 0
Tom takes 30 days -> IllegalArgumentException: Precondition failed: days <= balance (17), but was 30
Harry takes 3 days -> AssertionError: Postcondition failed: balance == old balance - days
Harry's balance: 20

Explanation of the code

• The Javadoc comment on take() states the contract for readers; the Contract calls enforce it at runtime. Ideally the two say the same thing.
• Precondition failures: taking 0 days or 30 days is the caller's mistake. require() throws IllegalArgumentException, the standard Java exception for a bad argument, and the message states the rule that was broken and the value that broke it.
• Postcondition failure: WeeklyLeaveAccount overrides deduct() and takes 5 days instead of 3. The caller did nothing wrong, so the check throws an AssertionError - the conventional signal for a bug in the code itself.
• Because take() computes newBalance and checks it before assigning it, the failed call leaves Harry's balance at 20. A contract check is most useful when it stops a bad state from being stored.
• The constructor establishes the invariant, and take() preserves it. Since the field is private and only take() changes it, those two checks are enough to guarantee the invariant for the object's whole life.

Contracts and inheritance

Ways to express contracts in Java

• Javadoc: document preconditions with @param and @throws, and postconditions with @return. It is the contract every reader sees, even if nothing checks it.
• Exceptions for preconditions of public methods: Objects.requireNonNull(), Objects.checkIndex() and IllegalArgumentException. These checks must always run, because callers of a public API cannot be trusted - Effective Java recommends checking parameters this way.
• assert for postconditions and invariants: an assert statement documents an internal assumption and checks it when assertions are enabled with java -ea, typically in development and tests. They are off by default, so they cost nothing in production - and so they must never be used for input validation.
• Record compact constructors: the natural home for a value's invariant, since every instance passes through them.
• Bean Validation: in Jakarta EE and Spring, annotations such as @NotNull, @Positive and @Size on parameters and return values declare simple contracts that a framework checks.
• Types: the strongest contract is one the compiler checks. A parameter of type EmployeeId instead of String, or Optional<Employee> for a result that may be missing, puts part of the contract into the signature.

Design by Contract and defensive programming

Summary