Design By Contract

Design by Contract views the precondition and postcondition of a method as a contract between

  • the method (supplier or server)
  • its callers (clients)

If a client calls the method with the precondition satisfied, then the supplier delivers a final state in which the postcondition is satisfied.

  • client
    • precondition is an obligation
    • postcondition is a right
  • supplier
    • precondition is a right
    • postcondition is an obligation

To correctly apply design by contract, each of the following rules must be observed or the program may behave unexpectedly:

Assumed Precondition Rule

Design by Contract adopts the demanding design of the precondition by assuming the precondition always holds.

The Assumed Precondition Rule (The Non-Redundancy Principle)

The body of a method should not test for its precondition because it is an assumed benefit for the supplier.

In other words, if a call to the method does not satisfy the precondition, the method is not bound by the postcondition.

Pre/Postcondition Violation Rules

Violation of a pre/postcondition at runtime indicates the existence of a bug.

The Precondition Violation Rule

A precondition violation is the manifestation of a bug in the client regardless of whether the postcondition is satisfied or violated.

In other words, if the client does not fulfill its contract, then the supplier is not bound by the postcondition.

// Precondition:  x >= 0
// Postcondition: abs(sqrt(x) * sqrt(x) - x) < epsilon
double sqrt(double x);

When x = -1, the implementation breaks. Because the client violated the precondition, the client code is faulty.

The Postcondition Violation Rule

A postcondition violation is the manifestation of a bug in the supplier because the supplier did not fulfill its contract.

// Precondition:  letter in 'a'..'z' || 'A'..'Z'
// Postcondition: return true  if letter is a vowel
//                       false otherwise

boolean isVowel(char letter) {
    String vowels = "aiouy" // 'e' is missing
    char ch = Character.toLowerCase(letter);
    return vowels.indexOf(ch) >= 0;
}

The call isVowel('E') incorrectly returns false. Because the client satisfied the precondition and the server violated the postcondition, the supplier code is faulty.

Reasonable Precondition Rule

In design by contract, the precondition is meant to clarify which cases the method cannot handle concerning logical requirements.

The Reasonable Precondition Rule

Requires that:

  1. The precondition should appear in the official documentation distributed to authors of clients.
  2. The need for the precondition should be justified logically in terms of the specification, not for the supplier's convenience of implementation.
public class BankAccount() {
    public BankAccount();
    public deposit(double amount);
}

In the class above, should deposit accept a negative amount to mean withdrawal? Obviously not, because deposit and withdraw exhibit different behaviors.

  • hi, can I deposit $-100 please?

In this case, a precondition of amount > 0 would be reasonable.

Precondition Availability Rule

The precondition must not rely on private variables or methods hidden from the clients.

The Precondition Availability Rule

Every client of the method should be able to check for its precondition.