design-by-contract

Files (3)

• SKILL.md
• examples.md · references/
• libraries.md · references/

SKILL.md (first lines)

# 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](references/libraries.md) for language-specific contract tools.
See [examples](references/examples.md) 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 |
|------|---------|

From OutlineDriven/odin-codex-plugin, Apache-2.0.

More from OutlineDriven/odin-codex-plugin