outlinedriven/design-by-contract

Design-by-Contract development

Contracts (PRE/POST/INV) define behavioral specification -- design from requirements before code exists. Formalized as Hoare Triples: {P} C {Q} where P=precondition, C=code, Q=postcondition.

Modern insight (2025): DbC complements LLM-generated code by serving as safety guardrails -- contracts clarify intent and prevent AI from breaking integrations. Spec-driven development (2025) positions contracts as "executable specifications."

See libraries for language-specific contract tools. See examples for brief contract patterns per language.

---

Verification Hierarchy

Use compile-time verification before runtime contracts. If a property can be verified statically, do NOT add a runtime contract.

Static Assertions (compile-time) > Test/Debug Contracts > Runtime Contracts

| Property | Static | Test | Debug | Runtime | |----------|--------|------|-------|---------| | Type size/alignment | static_assert | - | - | - | | Null/type safety | Type checker | - | - | - | | Exhaustiveness | Pattern match | - | - | - | | Expensive O(n)+ | - | test_ensures | - | - | | Internal invariants | - | - | debug_invariant | - | | Public API input | - | - | - | requires | | External/untrusted | - | - | - | Always required |

---

When to Apply

• Public API boundaries -- callers need clear contracts
• Complex state invariants -- balance >= 0, capacity limits
• Financial/business rule enforcement -- regulatory compliance
• Untrusted external data -- always validate at boundaries
• Multi-component integration points -- service contracts
• AI-generated code -- contracts serve as guardrails for LLM output

When NOT to Apply

• Internal helpers with obvious behavior
• Simple getters/setters, trivial pure functions
• Performance-critical hot paths (runtime contract overhead)
• Prototyping -- contracts add ceremony
• When the type system already enforces the property (prefer static)

---

Anti-patterns

• Contracts duplicating type system: If types enforce it, don't add a runtime check
• Runtime checks for compile-time properties: Wrong verification level
• Contracts without violation tests: Untested contracts are untrusted
• Contract fatigue: Decorating everything -- focus on boundaries and invariants
• Postconditions restating implementation: ensures(result == x - y) for subtract(x, y) adds nothing
• Forgetting old() semantics: Postconditions often need the pre-state value
• Ignoring contract inheritance: Preconditions weaken in subtypes (contravariance), postconditions strengthen (covariance) -- Liskov Substitution Principle

---

Contract Inheritance Rules

• Preconditions: Can be weakened (loosened) in subtypes -- accept more
• Postconditions: Can be strengthened (tightened) in subtypes -- guarantee more
• Invariants: Strengthened in subtypes; never weakened
• This enforces Liskov Substitution automatically.

DbC vs Defensive Programming (decision guidance)

| Approach | Philosophy | When | |----------|-----------|------| | Defensive | Don't trust caller; always check | Unknown callers, legacy APIs, untrusted input | | DbC | Clear contract; caller handles pre, method handles post | Internal APIs, well-scoped teams, correctness-critical | | Hybrid | Defensive at boundary; DbC internally | Best practice for modern systems |

---

Contract Formalization

Operation: withdraw(amount)

Preconditions:
  PRE-1: amount > 0
  PRE-2: amount <= balance
  PRE-3: account.status == Active

Postconditions:
  POST-1: balance == old(balance) - amount
  POST-2: result == amount

Invariants:
  INV-1: balance >= 0

---

Workflow (language-neutral)

1. PLAN -- Extract PRE/POST/INV from requirements. Formalize each with ID and description.
2. CREATE -- Enforce contracts at the appropriate verification level per the hierarchy: static proof, test assertion, debug check, or runtime guard. Reserve runtime contracts for public API boundaries and untrusted input.
3. VERIFY -- Run static analysis and build. Contracts must compile and lint.
4. TEST -- Write violation tests proving contracts catch bad inputs. Every PRE/POST/INV has a test.

---

Constitutional Rules (Non-Negotiable)

1. CREATE All Contracts: Implement every PRE, POST, INV from plan at the appropriate verification level per the hierarchy
2. Enforcement Enabled: Runtime contracts, where used, must be active (not compiled out or disabled)
3. Violations Caught: Tests prove contracts work -- static contracts verified by type checker, runtime contracts by violation tests
4. Documentation: Each contract traces to requirement

Exit Codes

| Code | Meaning | |------|---------| | 0 | All contracts enforced and tested | | 1 | Precondition violation in production code | | 2 | Postcondition violation in production code | | 3 | Invariant violation in production code | | 11 | Contract library not installed | | 13 | Runtime assertions disabled | | 14 | Contract lint failed |