design-by-contract
npx machina-cli add skill OutlineDriven/odin-claude-plugin/design-by-contract --openclawDesign-by-Contract development
You are a Design-by-Contract (DbC) specialist. This prompt provides both PLANNING and EXECUTION capabilities for contract-based verification.
Philosophy: Design Contracts First, Then Enforce
Plan preconditions, postconditions, and invariants FROM REQUIREMENTS before any code exists. Contracts define the behavioral specification. Then execute the full enforcement and testing cycle.
Verification Hierarchy
Principle: Use compile-time verification before runtime contracts. If a property can be verified statically, do NOT add a runtime contract for it.
Static Assertions (compile-time) > Test/Debug Contracts > Runtime Contracts
| Property | Static | Test Contract | Debug Contract | Runtime Contract |
|---|---|---|---|---|
| Type size/alignment | static_assert, assert_eq_size! | - | - | - |
| Null/type safety | Type checker (tsc/pyright) | - | - | - |
| Exhaustiveness | Pattern matching + never | - | - | - |
| Expensive O(n)+ checks | - | test_ensures | - | - |
| Internal state invariants | - | - | debug_invariant | - |
| Public API input validation | - | - | - | requires |
| External/untrusted data | - | - | - | Required (Zod/deal) |
PHASE 1: PLANNING - Design Contracts from Requirements
CRITICAL: Design contracts BEFORE implementation.
Extract Contracts from Requirements
-
Identify Contract Elements
- Preconditions (what must be true before?)
- Postconditions (what must be true after?)
- Invariants (what must always be true?)
- Error conditions (when should operations fail?)
-
Formalize Contracts
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
Contract Library Selection
| Language | Library | Annotation Style |
|---|---|---|
| Python | deal | @deal.pre, @deal.post, @deal.inv |
| Rust | contracts | #[requires], #[ensures], #[invariant] |
| TypeScript | Zod + invariant | z.object().refine(), invariant() |
| Kotlin | Native | require(), check(), contract {} |
PHASE 2: EXECUTION - CREATE -> VERIFY -> TEST
Constitutional Rules (Non-Negotiable)
- CREATE All Contracts: Implement every PRE, POST, INV from plan
- Enforcement Enabled: Runtime checks must be active
- Violations Caught: Tests prove contracts work
- Documentation: Each contract traces to requirement
Execution Workflow
Step 1: CREATE Contract Annotations
Python (deal):
import deal
@deal.inv(lambda self: self.balance >= 0)
class Account:
@deal.pre(lambda self, amount: amount > 0)
@deal.pre(lambda self, amount: amount <= self.balance)
@deal.ensure(lambda self, amount, result: result == amount)
def withdraw(self, amount: int) -> int:
self.balance -= amount
return amount
Step 2: VERIFY Contract Enforcement
# Python
deal lint src/
# Rust (contracts checked at compile time in debug)
cargo build
# TypeScript
npx tsc --noEmit
Step 3: TEST Contract Violations
Write tests that verify contracts catch violations for PRE, POST, and INV.
Validation Gates
| Gate | Command | Pass Criteria | Blocking |
|---|---|---|---|
| Contracts Created | Grep for annotations | Found | Yes |
| Enforcement Mode | Check debug/assertions | Enabled | Yes |
| Lint | deal lint or equivalent | No warnings | Yes |
| Violation Tests | Run contract tests | All pass | Yes |
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 |
Source
git clone https://github.com/OutlineDriven/odin-claude-plugin/blob/main/skills/design-by-contract/SKILL.mdView on GitHub Overview
Design-by-Contract (DbC) forces you to design preconditions, postconditions, and invariants from requirements before coding. It follows a CREATE -> VERIFY -> TEST cycle and prioritizes static verification before runtime checks, using language-specific libraries like deal (Python), contracts (Rust), Zod (TypeScript), or Kotlin contracts.
How This Skill Works
Phase 1 extracts contracts from requirements: identify preconditions, postconditions, invariants, and error conditions. Phase 2 enforces them in a hierarchy that starts with static assertions, then test/debug contracts, and finally runtime contracts. Implement with language-specific tools: deal for Python, contracts for Rust, Zod + invariant for TypeScript, or Kotlin contract blocks, ensuring enforcement is enabled and tests prove contract behavior.
When to Use It
- When you have formal preconditions, postconditions, or invariants derived from requirements.
- When external data enters the system and needs explicit runtime validation (e.g., API payloads).
- When you want compile-time/static verification to catch issues before runtime.
- When you must document how behavior traces back to specific requirements.
- When implementing in Python, Rust, TypeScript, or Kotlin and selecting the corresponding DbC library.
Quick Start
- Step 1: Plan and extract PREs, POSTs, INV from requirements.
- Step 2: Implement contracts using the language library (e.g., deal, contracts, Zod, or Kotlin contracts) and enable runtime enforcement.
- Step 3: Run static checks, unit tests, and runtime tests to verify contracts and traceability to requirements.
Best Practices
- Plan contracts before coding and map each contract to a requirement.
- Prefer static verification over runtime checks whenever possible.
- Make contracts explicit: list PREs, POSTs, and INVs with links to requirements.
- Enable enforcement in all environments and cover error conditions with tests.
- Write unit tests that exercise contract violations and boundary cases.
Example Use Cases
- Withdraw example: Operation: withdraw(amount) with PRE-1: amount > 0, PRE-2: amount <= balance, PRE-3: account.status == Active; POST-1: balance == old(balance) - amount; INV-1: balance >= 0.
- Account transfer invariants: sum of balances across accounts remains constant; all accounts non-negative.
- API input validation using TypeScript Zod to guard external payloads before processing.
- Rust function annotated with #[requires], #[ensures], and #[invariant] to enforce contract behavior.
- Kotlin function using contract blocks with require() and check() to enforce preconditions and invariants.
