OutlineDriven Contract-driven
Contract
| Field | Bound contract |
|---|---|
| Trigger | Crossing a public API boundary, guarding complex invariants, or hardening untrusted input or integration seams. |
| Authority | Reversible local: writes only named local types, assertions, validators, and tests at contract boundaries; rollback is undo (delete the added code or revert the boundary change). No remote mutation. |
| Side effect | Adds or refines local types, assertions, validators, and tests at contract boundaries. |
| Done | Every planned contract is implemented at the appropriate static/test/debug/runtime layer and violations fail explicitly at the boundary. |
Inputs
Required:
- The requirements or specification for the operation whose contract is being designed.
- The target source file or module containing the public API boundary, invariant, or untrusted seam.
Optional:
- Existing tests that must continue to pass.
Procedure
- Plan: extract PRE/POST/INV from the requirements. Give each contract an ID and a one-line description (e.g. PRE-1: amount > 0; POST-1: balance == old(balance) - amount; INV-1: balance >= 0). Do not begin implementation until every planned contract has an ID. Done when: every planned contract has an ID and a one-line description.
- Select verification level: choose the strongest layer that can enforce each contract, preferring static over runtime:
- Static type system or static_assert for type size, alignment, null/type safety, and exhaustiveness.
- Test assertions for expensive O(n)+ properties.
- Debug-only invariants for internal invariants.
- Runtime guards for public API input, and always for external or untrusted input. If a property can be verified statically, do not add a runtime contract. Done when: every contract has a selected verification level, static preferred over runtime.
- Create: implement every PRE, POST, INV at its chosen level in the target local code. Runtime contracts, where used, must be active and not compiled out or disabled. Done when: every contract is implemented at its chosen level and runtime contracts are active.
- Verify: run the type checker, static analysis, and build. Contracts must compile and lint. Done when: the type checker, static analysis, and build pass with all contracts.
- Test: write one violation test per PRE/POST/INV proving the contract catches bad input or bad state. Static contracts are verified by the type checker; runtime contracts by violation tests that assert the boundary fails explicitly. Done when: one violation test per contract passes, proving the boundary fails on bad input or state.
Failure and recovery
- Contract lint or build fails: fix the contract or implementation; do not disable or compile out the runtime contract to make it pass.
- A violation test does not fire: the contract is not enforced at the chosen layer; re-select the layer or strengthen the check; never delete the test to make it pass.
- A contract restates the implementation trivially (e.g. ensures(result == x - y) for subtract(x, y)): delete that contract; it is contract fatigue, not a boundary guarantee.
- Partial result: if some contracts cannot be implemented because a requirement is missing, stop and report the missing requirement; do not invent contracts or widen scope.
- Rollback: delete the added local types, assertions, validators, or tests, or revert the boundary change; no remote, credential, published, or deployed artifact is touched.
Output
Local code with every planned PRE/POST/INV contract implemented at its verification layer, plus one violation test per contract. Violations fail explicitly at the boundary. Each contract traces to a requirement by ID.