← ClaudeAtlas

design-by-contractlisted

Design-by-Contract (DbC) development. Use when implementing with formal preconditions, postconditions, and invariants across any language.
OutlineDriven/odin-claude-plugin · ★ 27 · AI & Automation · score 82
Install: claude install-skill OutlineDriven/odin-claude-plugin
# 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 enforcem