Contract Programming

Overview

Design by Contract (DbC) formalises method interfaces with preconditions (what the caller must guarantee), postconditions (what the method guarantees on return), and class invariants (conditions that must hold throughout an object's lifetime). Bertrand Meyer introduced the concept in Eiffel (1986). It shifts responsibility for input validation from the method body to the call site, making APIs self-documenting and bugs easier to localise.

Origin

Bertrand Meyer coined "Design by Contract" and implemented it as first-class language features in Eiffel (1986). His book "Object-Oriented Software Construction" (1988, 2nd ed. 1997) formalised the theory. Clojure.spec (2016) and Python's hypothesis library bring contract-like validation to dynamic languages. TypeScript's type system enforces a compile-time subset of contracts.

Examples

function assert(condition: boolean, message: string): asserts condition {
  if (!condition) throw new Error('Contract violation: ' + message);
}

function divide(dividend: number, divisor: number): number {
  // Preconditions
  assert(Number.isFinite(dividend), 'dividend must be finite');
  assert(Number.isFinite(divisor), 'divisor must be finite');
  assert(divisor !== 0, 'divisor must be non-zero');

  const result = dividend / divisor;

  // Postcondition
  assert(
    Number.isFinite(result),
    'result must be finite, implementation error'
  );

  return result;
}

class Stack<T> {
  private items: T[] = [];

  push(item: T): void {
    const sizeBefore = this.items.length;
    this.items.push(item);
    assert(this.items.length === sizeBefore + 1, 'push must increase size by 1');
  }

  pop(): T {
    assert(this.items.length > 0, 'pop requires non-empty stack');
    return this.items.pop()!;
  }
}

require 'dry-validation'

class CreateOrderContract < Dry::Validation::Contract
  params do
    required(:customer_id).filled(:integer, gt?: 0)
    required(:items).array(:hash) do
      required(:product_id).filled(:integer, gt?: 0)
      required(:quantity).filled(:integer, gt?: 0, lteq?: 100)
      required(:unit_price).filled(:decimal, gt?: 0)
    end
    optional(:discount_code).maybe(:string, max_size?: 20)
  end

  rule(:items) do
    key.failure('must not be empty') if value.empty?
  end

  rule(:items) do
    total = value.sum { |i| i[:quantity] * i[:unit_price] }
    key.failure('order total must not exceed 10000') if total > 10_000
  end
end

contract = CreateOrderContract.new
result = contract.call(
  customer_id: 42,
  items: [{ product_id: 1, quantity: 2, unit_price: 29.99 }]
)
result.success? # => true

Use Cases

• 01Library and framework APIs where clear caller/callee responsibility boundaries prevent misuse and improve error messages
• 02Safety-critical systems (medical devices, aviation software) where formal verification of preconditions is required
• 03Public APIs where contract violations indicate integration bugs and must fail loudly rather than silently returning corrupt data
• 04Domain model methods where business invariants (non-negative quantities, valid date ranges) must be enforced consistently

When Not to Use

• //User-facing input validation where precondition failures should produce user-friendly messages, not exceptions
• //Performance-critical hot paths where assertion overhead is measurable; DbC frameworks typically provide a way to disable checks in production builds
• //External data ingestion (API responses, CSV imports) where data quality cannot be guaranteed by contract; defensive validation is more appropriate

Technical Notes

• Eiffel's contract system is inherited: subclass contracts can only weaken preconditions and strengthen postconditions (contravariance/covariance respectively), enforcing LSP at the contract level
• Clojure.spec (Rich Hickey, 2016) allows specifying the shape of function inputs and outputs as data and generating test cases from specs via test.check generative testing; this is the closest mainstream equivalent to DbC outside Eiffel
• Google's Guava library provides Preconditions.checkArgument() and Preconditions.checkState() for Java; Apache Commons Lang provides Validate class. Both are lightweight DbC without runtime contract inheritance
• The difference between DbC assertions and input validation: DbC is for programming errors (violated contracts indicate bugs); input validation is for user errors (form validation returns errors, not exceptions). Mixing them leads to poor error handling