Design By Contract

Purpose

Formalize behavior through preconditions, postconditions, and invariants

Context

Systems where functions cross trust boundaries — between caller and callee,
between application layers (PD/MD/SI/UI), between adapter backends that share
an interface but differ in implementation. Particularly valuable in:

- Typed languages (Go, TypeScript) where type system can encode structural
  preconditions via Input structs and return types
- Domain-critical mutations where corrupt state has cascading consequences
- Multi-backend architectures where all backends must honor the same contract
- Boundary layers (SI) where external input enters the system and must be
  validated before trusted code processes it

Problem

How to make function behavior predictable and blame assignment unambiguous
when functions receive bad input, produce unexpected output, or leave
entities in corrupt state?

Forces:
(1) Implicit assumptions — callers guess what input is valid, callees guess
    what callers will send. Both guess wrong under edge cases.
(2) Blame ambiguity — when a function fails, is it the caller's fault
    (sent bad input) or the callee's fault (has a bug)? Without contracts,
    both sides add defensive checks, duplicating validation and obscuring
    the real error source.
(3) Invariant drift — entities accumulate mutations across create, update,
    and state transitions. Without explicit invariants, corrupt state
    creeps in through edge cases that individual functions don't catch.
(4) Backend substitutability — when multiple backends implement the same
    interface (FileBackend vs PostgresBackend), their contracts must match.
    If one backend silently ignores writes while another throws errors,
    callers cannot rely on consistent behavior.
(5) Layer-crossing contracts — a function validated at the SI boundary
    should not re-validate at PD. But without explicit contract layers,
    every layer adds redundant checks "just in case."

Solution

Define explicit contracts for every function using three complementary
mechanisms:

PRECONDITIONS (caller's obligation):
What must be true before the function executes. If preconditions are not met,
the function returns an error immediately — the caller violated the contract.
In Go, preconditions are encoded in Input struct types (structural) and guard
clauses at function entry (semantic).

POSTCONDITIONS (callee's obligation):
What is guaranteed after successful return. If the function returns without
error, all postconditions hold — the caller may rely on them. In Go, the
return type (T, error) is the postcondition: non-nil T + nil error means all
guarantees fulfilled.

INVARIANTS (preserved by all mutations):
What must be true for all entity instances at all observable times. Every
public function that mutates state must leave invariants intact. In SBX,
invariants are modeled in rule.yml (category: invariant) and mirrored as
SQL CHECK constraints in the MD layer.

CONTRACT INHERITANCE (for multi-backend architectures):
When a function has multiple implementations (adapter backends), all
implementations must honor the same contract. Subtypes may weaken
preconditions (accept more) and strengthen postconditions (guarantee more),
but never the reverse. This is the Liskov Substitution Principle applied
to function contracts.

The caller ensures preconditions. The callee ensures postconditions given
preconditions hold. Both sides maintain invariants. Blame is unambiguous:
precondition violation = caller's fault, postcondition violation = callee's bug.

Consequences

Gained:
- Blame is unambiguous: precondition failure = caller fault, postcondition
  failure = callee bug. No more "who should have validated this?" debates.
- Functions are independently testable: test precondition rejection, test
  postcondition fulfillment, test invariant preservation separately.
- Redundant validation eliminated: SI layer validates (barricade), PD layer
  trusts typed data. No defensive checks duplicated across layers.
- Backend substitutability guaranteed: all implementations of an interface
  honor the same contract per Liskov/DBC-004.
- Invariants are explicit and discoverable: rule.yml category: invariant
  documents what must always be true, not hidden in scattered checks.

Accepted:
- Verbosity: every function needs contract documentation (mitigated by type
  system encoding — Input struct IS the precondition documentation).
- Upfront design cost: contracts must be designed before implementation.
  This is the MODEL BEFORE CODE principle applied to function boundaries.
- Runtime overhead for semantic preconditions: guard clause checks add
  branching cost (negligible in practice, significant in hot loops).
- Contract evolution: changing a precondition (accepting less) is a breaking
  change. Weakening preconditions (accepting more) is always safe.

Collaborations

The Caller constructs an Input struct encoding structural preconditions and
calls the Callee. The Callee checks semantic preconditions via guard clauses
(early return on violation). If preconditions hold, the Callee performs the
operation and returns (result, nil) fulfilling the postcondition Contract.
On precondition violation, the Callee returns (zero, error) without side effects.
The InvariantMonitor (SQL CHECK constraints, test assertions) verifies that
entity state remains consistent after every mutation. Backend substitutability
is maintained by all ConcreteCallees (FileBackend, PostgresBackend) honoring
the same Contract interface.

Structure

Participants:
- Caller: the code invoking the function (handler, service, test)
- Callee: the function being invoked (service method, repository, adapter)
- Contract: the agreement (Input struct type + return type + invariant rules)
- InvariantMonitor: enforcement mechanism (SQL CHECK, test assertions)

Relationships:
- Caller depends on Contract (must satisfy preconditions)
- Callee depends on Contract (must fulfill postconditions)
- InvariantMonitor validates entity state against invariant rules
- Multiple Callees (backends) share the same Contract interface

Structure:
  Caller                Contract              Callee
  ------                --------              ------
  create Input struct   Input type = pre      check guards (semantic pre)
  call Callee(input)    Return type = post    perform operation
  use result            Invariants = rules    return (result, nil)
                              |
                        InvariantMonitor
                        (SQL CHECK / test assert)

Implementation

// Contract encoded in Go types — Input struct IS the precondition
type CreatePropertyInput struct {
    Name   string  // required: structural precondition (non-zero-value)
    Price  int64   // required: semantic precondition (must be > 0)
    TypeID string  // required: must reference existing dictionary entry
}

// Callee: guard clauses enforce semantic preconditions
func (s *PropertyService) Create(ctx context.Context, input CreatePropertyInput) (Property, error) {
    // Precondition checks (caller's obligation, verified here as safety net)
    if input.Name == "" {
        return Property{}, fmt.Errorf("create property: %w", ErrNameRequired)
    }
    if input.Price <= 0 {
        return Property{}, fmt.Errorf("create property: %w", ErrPricePositive)
    }

    // Operation (preconditions satisfied)
    prop := Property{
        ID:    generateID(),
        Name:  input.Name,
        Price: input.Price,
    }

    if err := s.repo.Save(ctx, prop); err != nil {
        return Property{}, fmt.Errorf("create property %s: %w", prop.ID, err)
    }

    // Postcondition: non-nil Property with valid ID + nil error
    return prop, nil
}

// Invariant enforced at MD layer (SQL CHECK constraint)
// CREATE TABLE properties (
//     id    TEXT PRIMARY KEY,
//     name  TEXT NOT NULL CHECK (name != ''),
//     price BIGINT NOT NULL CHECK (price > 0)
// );

// Backend contract — interface IS the postcondition contract
type Backend interface {
    List(ctx context.Context, entity string) ([]Entry, error)
    Get(ctx context.Context, entity, code string) (Entry, error)
    Create(ctx context.Context, entity string, entry Entry) error
}

// Compile-time interface compliance (DBC-004: all backends honor contract)
var _ Backend = (*FileBackend)(nil)
var _ Backend = (*PostgresBackend)(nil)

Example

Consider the SBX dictionary package. A dictionary stores enum-like entries
(e.g., property_type: ["apartment", "villa", "studio"]) with two storage
backends: FileBackend reads from entity.yml fixtures (read-only, always
available), PostgresBackend reads/writes from a lookup table (read-write,
requires database).

The Store.Create function accepts a new entry and persists it. But what
happens when: the entry code is empty? The entry duplicates an existing
code? The backend is FileBackend (read-only)? Currently, behavior varies
unpredictably — FileBackend silently ignores writes, PostgresBackend throws
a constraint violation on duplicates, and empty codes produce corrupt data
that surfaces later as "entry not found" errors far from the original call.

The caller cannot predict what will happen because the function's assumptions
are implicit. The callee cannot trust its input because no contract defines
what valid input looks like. Invariants (codes are unique, entries are non-empty)
are enforced by accident rather than by design.

Resolution

Applying Design by Contract to the SBX dictionary package: the Backend
interface declares the contract (List, Get, Create with typed signatures).
CreatePropertyInput struct encodes structural preconditions — the type system
prevents passing raw strings. Guard clauses at function entry encode semantic
preconditions (price > 0, name non-empty). Return types (Entry, error) encode
postconditions — non-nil Entry + nil error means the entry exists and is valid.

SQL CHECK constraints (price > 0, name NOT NULL) mirror PD invariants at the
MD layer — belt and suspenders. FileBackend returns ErrReadOnly on Create
(documented contract limitation, not a silent failure). PostgresBackend returns
constraint violation on duplicate codes (postcondition: codes are unique).

Blame is now unambiguous: empty name → caller violated precondition. Duplicate
code on insert → caller should have checked existence first. Corrupt entity
state → callee has a bug (invariant not preserved). No more "who should have
validated this?" investigations.

Known Uses

Eiffel programming language — native require/ensure/invariant keywords (Meyer's original implementation)
Go standard library — io.Reader contract: Read returns (n, err) where n <= len(p), err == io.EOF at end
Java Contracts (JML, Cofoja) — annotation-based preconditions/postconditions for Java methods
TypeScript branded types — type UserId = string & { __brand: 'UserId' } prevents mixing ID types (type-level contract)
SQL CHECK constraints — database-level invariant enforcement independent of application code

Tags

Overview

Purpose

Context

Problem

Solution

Consequences

Collaborations

Structure

Implementation

Example

Resolution

Known Uses

See Also