Design by Contract

What is Design by Contract?

Design by Contract (DbC), introduced by Bertrand Meyer for the Eiffel language, is an approach to software design where components define formal, precise, and verifiable interface specifications. It uses preconditions, postconditions, and invariants to specify the obligations and benefits of each component.

Think of it like a legal contract: both parties (caller and callee) have obligations, and both get benefits. If the caller fulfills the preconditions, the callee guarantees the postconditions.

The Three Pillars

1. Preconditions
   ──────────────
   What the CALLER must guarantee before calling a method.
   If the precondition is not met, the method is not obligated to work.
   Think: "You must do this before calling me."

   Example: withdraw(amount) requires amount > 0 && amount <= balance

2. Postconditions
   ───────────────
   What the METHOD guarantees after it completes (if preconditions were met).
   Think: "I will do this if you meet the requirements."

   Example: withdraw(amount) guarantees balance decreased by amount

3. Invariants
   ───────────
   Conditions that must ALWAYS be true for the object, before and after
   any method call. Think: "This must always hold."

   Example: balance must always be >= 0

Implementation Example

class BankAccount {
  #balance;
  #owner;

  constructor(owner, initialBalance) {
    // Invariant check: balance must be non-negative
    if (initialBalance < 0) {
      throw new Error("Invariant violated: initial balance cannot be negative");
    }
    this.#owner = owner;
    this.#balance = initialBalance;
  }

  // Precondition: amount must be positive
  // Postcondition: balance increases by amount
  // Invariant: balance remains >= 0
  deposit(amount) {
    // ─── PRECONDITION ───
    if (amount <= 0) {
      throw new Error("Precondition failed: deposit amount must be positive");
    }

    const oldBalance = this.#balance;

    // ─── METHOD BODY ───
    this.#balance += amount;

    // ─── POSTCONDITION ───
    if (this.#balance !== oldBalance + amount) {
      throw new Error("Postcondition failed: balance not updated correctly");
    }

    // ─── INVARIANT ───
    this.#checkInvariants();

    return this.#balance;
  }

  // Precondition: amount > 0 && amount <= balance
  // Postcondition: balance decreases by amount
  // Invariant: balance remains >= 0
  withdraw(amount) {
    // ─── PRECONDITION ───
    if (amount <= 0) {
      throw new Error("Precondition failed: withdrawal amount must be positive");
    }
    if (amount > this.#balance) {
      throw new Error("Precondition failed: insufficient funds");
    }

    const oldBalance = this.#balance;

    // ─── METHOD BODY ───
    this.#balance -= amount;

    // ─── POSTCONDITION ───
    if (this.#balance !== oldBalance - amount) {
      throw new Error("Postcondition failed: balance not updated correctly");
    }

    // ─── INVARIANT ───
    this.#checkInvariants();

    return this.#balance;
  }

  get balance() {
    return this.#balance;
  }

  // ─── INVARIANT CHECK ───
  #checkInvariants() {
    if (this.#balance < 0) {
      throw new Error("Invariant violated: balance is negative");
    }
    if (!this.#owner || this.#owner.length === 0) {
      throw new Error("Invariant violated: owner cannot be empty");
    }
  }
}

// Usage
const account = new BankAccount("Alice", 1000);
account.deposit(500);    // ✓ Works — preconditions met
account.withdraw(200);   // ✓ Works — preconditions met

try {
  account.withdraw(-50); // ✗ Fails precondition
} catch (e) {
  console.log(e.message); // "Precondition failed: withdrawal amount must be positive"
}

try {
  account.withdraw(99999); // ✗ Fails precondition
} catch (e) {
  console.log(e.message); // "Precondition failed: insufficient funds"
}

DbC in Practice

Benefits of Design by Contract:

  1. Clear Documentation
     Contracts ARE the documentation. No separate docs needed.
     "What does this method expect? What does it guarantee?"

  2. Better Error Detection
     Catch errors at the point they occur, not downstream.
     Preconditions catch bad inputs immediately.

  3. Facilitates Reuse
     Clear contracts make it safe to reuse components.
     You know exactly what you need to provide.

  4. Supports Testing
     Contracts serve as built-in test assertions.
     Every method call is implicitly a test.

Contracts vs Assertions:
  ┌──────────────────┬──────────────────────────────────┐
  │ Feature          │ Design by Contract               │
  ├──────────────────┼──────────────────────────────────┤
  │ Scope            │ Per method and per class         │
  │ Part of API      │ Yes — part of the interface      │
  │ Can be disabled  │ In production for performance    │
  │ Checked at       │ Call boundaries                  │
  │ Includes         │ Pre, Post, Invariant             │
  └──────────────────┴──────────────────────────────────┘

DbC and Inheritance

When a subclass overrides a method, it must respect the contract of the parent class. This is closely related to the Liskov Substitution Principle:

DbC Rules for Inheritance:

  Precondition Rule (Covariance):
    Subclass preconditions must be EQUAL TO OR WEAKER than
    the parent's. The subclass cannot add new preconditions.

    Parent:  withdraw(amount) — amount > 0
    Child:   withdraw(amount) — amount > 0  ✓ (same)
    Child:   withdraw(amount) — amount > 0 && isBusinessDay  ✗ (stronger)

  Postcondition Rule (Contravariance):
    Subclass postconditions must be EQUAL TO OR STRONGER than
    the parent's. The subclass cannot weaken guarantees.

    Parent:  withdraw(amount) — balance decreases by amount
    Child:   withdraw(amount) — balance decreases by amount  ✓ (same)
    Child:   withdraw(amount) — balance decreases by amount minus fee  ✗ (weaker)

  Invariant Rule:
    Subclass invariants must include ALL parent invariants.
    The subclass can add new invariants but cannot remove parent ones.

    Parent:  balance >= 0
    Child:   balance >= 0 && accountActive == true  ✓ (added invariant)
    Child:   (no balance check)  ✗ (removed parent invariant)