| name | contract-driven |
| description | Design-by-Contract (DbC). Use when crossing public API boundaries, guarding complex state invariants, or hardening untrusted inputs and integration seams. |
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
- 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
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)
- PLAN -- Extract PRE/POST/INV from requirements. Formalize each with ID and description.
- 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.
- VERIFY -- Run static analysis and build. Contracts must compile and lint.
- TEST -- Write violation tests proving contracts catch bad inputs. Every PRE/POST/INV has a test.
Constitutional Rules (Non-Negotiable)
- CREATE All Contracts: Implement every PRE, POST, INV from plan at the appropriate verification level per the hierarchy
- Enforcement Enabled: Runtime contracts, where used, must be active (not compiled out or disabled)
- Violations Caught: Tests prove contracts work -- static contracts verified by type checker, runtime contracts by violation tests
- 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 |
