design-by-contract — Skillopedia

Design-by-Contract Development Skill Capability Design-by-Contract (DbC) is a programming methodology that uses formal specifications (contracts) to define component behavior. This skill enables: - Contract Design : Plan preconditions, postconditions, and invariants before implementation - Artifact Generation : Create contract annotations across 8+ languages - Verification : Run contract validation with appropriate runtime flags - Remediation : Fix contract violations with targeted debugging Core Contract Types: - Preconditions : What must be true before a function executes (caller's duty) -…

-l python | \\\n rg -v '@pre|@post|@invariant' --files-without-match\n```\n\n**Remediation template**:\n```python\n@pre(lambda $PARAMS: $CONDITION)\n@post(lambda result: $POSTCONDITION)\ndef $NAME($PARAMS) -> $RET:\n \"\"\"$DOCSTRING\"\"\"\n $BODY\n```\n\n**Runtime flags**: Check `__debug__` is True (not `python -O`)\n\n### Java Detection\n```bash\n# Find contracts\nrg 'checkArgument|checkState|validate\\(|Preconditions\\.' --type java\n\n# Find methods without contracts\nast-grep -p 'public $RET $NAME($$) { $$ }' -l java | \\\n rg -v 'checkArgument|validate' --files-without-match\n```\n\n**Remediation template**:\n```java\npublic $RET $NAME($PARAMS) {\n checkArgument($CONDITION, \"$ERROR_MSG\");\n $BODY\n validate($POSTCONDITION, \"$POST_ERROR\");\n return $RESULT;\n}\n```\n\n**Runtime flags**: Check assertions enabled with `-ea` flag\n\n### Kotlin Detection\n```bash\n# Find contracts\nrg 'contract \\{|Either\u003c|Validated|require\\(|check\\(' --type kotlin\n\n# Find functions without contracts\nast-grep -p 'fun $NAME($$): $$ { $$ }' -l kotlin | \\\n rg -v 'contract|require|check' --files-without-match\n```\n\n**Remediation template**:\n```kotlin\nfun $NAME($PARAMS): Either\u003c$ERR, $RET> {\n contract {\n returns() implies ($CONDITION)\n }\n return if (!$CONDITION) \"$ERROR\".left()\n else { $BODY }.right()\n}\n```\n\n**Runtime flags**: Check `-ea` for JVM assertions\n\n### C# Detection\n```bash\n# Find contracts\nrg 'Guard\\.Against|Contract\\.Requires|Contract\\.Ensures|Debug\\.Assert' --type cs\n\n# Find methods without contracts\nast-grep -p 'public $RET $NAME($$) { $$ }' -l csharp | \\\n rg -v 'Guard\\.|Contract\\.' --files-without-match\n```\n\n**Remediation template**:\n```csharp\npublic $RET $NAME($PARAMS) {\n Guard.Against.Null($PARAM, nameof($PARAM));\n Contract.Ensures(Contract.Result\u003c$RET>() $POSTCONDITION);\n $BODY\n}\n```\n\n**Runtime flags**: Check Debug configuration\n\n### C++ Detection\n```bash\n# Find contracts\nrg 'Expects\\(|Ensures\\(|boost::contract|gsl::' --type cpp\n\n# Find functions without contracts\nast-grep -p '$RET $NAME($$) { $$ }' -l cpp | \\\n rg -v 'Expects|Ensures' --files-without-match\n```\n\n**Remediation template**:\n```cpp\n$RET $NAME($PARAMS) {\n Expects($PRECONDITION);\n $BODY\n Ensures($POSTCONDITION);\n return $RESULT;\n}\n```\n\n**Runtime flags**: Check `NDEBUG` not defined\n\n### C Detection\n```bash\n# Find contracts\nrg 'assert\\(|static_assert' --type c\n\n# Find functions without asserts\nast-grep -p '$RET $NAME($$) { $$ }' -l c | \\\n rg -v 'assert\\(' --files-without-match\n```\n\n**Remediation template**:\n```c\n$RET $NAME($PARAMS) {\n assert($PRECONDITION && \"$ERROR_MSG\");\n $BODY\n assert($POSTCONDITION && \"$POST_ERROR\");\n return $RESULT;\n}\n```\n\n**Runtime flags**: Check `NDEBUG` not defined\n\n---\n\n## Contract Library Matrix\n\n| Language | Library | Runtime Flag |\n|----------|---------|--------------|\n| Rust | contracts | CONTRACTS_DISABLE |\n| TypeScript | Zod | (always active) |\n| Python | icontract | ICONTRACT_SLOW |\n| Java | Guava | (always active) |\n| Kotlin | native | (always active) |\n| C# | Guard | (always active) |\n| C++ | GSL/Boost | NDEBUG |\n\n---\n\n## Error Handling Matrix\n\n| Language | Contract Library | Error Type | Error Handling | Recovery Strategy |\n|----------|-----------------|------------|----------------|-------------------|\n| **Rust** | contracts, prusti | panic! | `catch_unwind` (discouraged) | Result/Option types |\n| **TypeScript** | zod, io-ts | ZodError, thrown | try/catch | Either/Result pattern |\n| **Python** | dpcontracts, icontract | AssertionError | try/except | Optional/Result |\n| **Java** | Guava, Bean Validation | IllegalArgumentException | try/catch | Optional/Either |\n| **Kotlin** | Arrow, require/check | IllegalArgumentException | try/catch | Either\u003cE, A> |\n| **C#** | Code Contracts, Guard | ArgumentException | try/catch | Result\u003cT> |\n| **C++** | GSL, Boost.Contract | std::terminate | noexcept | std::expected |\n| **C** | assert.h | abort() | Signal handler | Return codes |\n\n### Error Message Best Practices\n\n```\nContract Type: [PRECONDITION|POSTCONDITION|INVARIANT]\nLocation: file.rs:42 in function_name()\nCondition: x > 0 && x \u003c 100\nActual Value: x = -5\nExpected: Positive integer less than 100\nContext: Processing user input for order ID\n```\n\n---\n\n## Troubleshooting Guide\n\n### Common Issues\n\n| Symptom | Cause | Resolution |\n|---------|-------|------------|\n| Exit 1 | Precondition violation | Caller must provide valid input (fix call site) |\n| Exit 2 | Postcondition violation | Implementation doesn't meet guarantee (fix function) |\n| Exit 3 | Invariant violation | Object state became invalid (fix state mutation) |\n| Exit 11 | Contract library missing | Install: `pip install icontract`, `cargo add contracts`, `npm i zod` |\n| Exit 12 | No contract annotations | Run plan phase first |\n| Exit 13 | Tests failed with contracts | Debug violation type |\n| `CONTRACTS_DISABLE` set | Contracts silently skipped | `unset CONTRACTS_DISABLE` |\n| No error but wrong behavior | Contract too weak | Strengthen pre/post conditions |\n| Performance impact | Contracts in hot path | Use `@icontract.require(enabled=DEBUG)` |\n| Contract not firing | Debug assertions disabled | Check `NDEBUG`, `-O` flags |\n| False positive | Contract too strict | Review expected vs actual |\n| False negative | Contract too weak | Add edge case tests |\n| Stack overflow | Recursive contract | Check for cycles |\n| Flaky failures | Race condition in contract | Add synchronization |\n\n### Quick Diagnostics\n\n```bash\n# Check if contracts are enabled (Rust)\ncargo build && rg 'debug_assert' target/debug/*.d\n\n# Check if contracts are enabled (Node.js)\nnode -e \"console.log(process.env.NODE_ENV)\"\n\n# Check if assertions enabled (Java)\njava -ea -version 2>&1 | head -1\n\n# Check if assertions enabled (C/C++)\ncpp -dM /dev/null | grep NDEBUG\n```\n\n### Debugging Commands\n\n```bash\n# Python - Verbose contract errors\nICONTRACT_SLOW=true pytest -v --tb=long\n\n# Python - Find contract decorators\nrg '@icontract\\.(require|ensure|invariant)' src/\n\n# Rust - Enable backtrace\nRUST_BACKTRACE=1 cargo test\n\n# Rust - Find contract attributes\nrg '#\\[(pre|post|invariant)\\(' src/\n\n# TypeScript - Verbose Zod errors\nDEBUG=zod:* npm test\n\n# TypeScript - Find Zod schemas\nrg 'z\\.(object|refine|string|number)' src/\n\n# General - Check contracts not disabled\nenv | rg -i 'contract|ndebug'\n```\n\n### Debugging Contract Violation Workflows\n\n#### Precondition Violation Debugging\n\n1. **Identify the violation location**:\n ```bash\n # Run with debug symbols\n RUST_BACKTRACE=1 cargo run # Rust\n node --enable-source-maps # Node.js\n python -c \"import traceback\" # Python\n ```\n\n2. **Examine the call stack**:\n - Find the caller that provided invalid input\n - Check intermediate transformations that corrupted data\n\n3. **Add tracing at contract boundary**:\n ```rust\n // Rust example\n #[pre(x > 0)]\n fn process(x: i32) {\n tracing::debug!(\"process called with x = {}\", x);\n // ...\n }\n ```\n\n4. **Common causes**:\n - Unvalidated user input\n - Null/None propagation\n - Integer overflow in computation\n - Incorrect API usage\n\n#### Postcondition Violation Debugging\n\n1. **Instrument the function exit**:\n ```typescript\n // TypeScript example\n function calculate(x: number): number {\n const result = /* computation */;\n console.log(`calculate returning: ${result}`);\n invariant(result > 0, `Expected positive, got ${result}`);\n return result;\n }\n ```\n\n2. **Check intermediate state**:\n - Add assertions at each computation step\n - Verify loop invariants maintained\n\n3. **Common causes**:\n - Logic error in computation\n - Incorrect formula\n - Edge case not handled\n - Floating point precision loss\n\n#### Invariant Violation Debugging\n\n1. **Track state transitions**:\n ```python\n # Python example with dpcontracts\n @invariant(lambda self: self.balance >= 0)\n class Account:\n def __init__(self):\n self._log_state(\"init\")\n\n def withdraw(self, amount):\n self._log_state(f\"before withdraw {amount}\")\n self.balance -= amount\n self._log_state(f\"after withdraw {amount}\")\n ```\n\n2. **Find mutation that breaks invariant**:\n - Identify all state-mutating methods\n - Check each mutation point\n\n3. **Common causes**:\n - Missing validation in setter\n - Concurrent modification\n - Deserialization bypassing constructor\n\n---\n\n## Common Pitfalls and Solutions\n\n### Pitfall 1: Contracts with Side Effects\n\n**Problem:** Contract check modifies program state.\n\n**Solution:**\n```rust\n// WRONG: Contract has side effect\n#[pre(counter.increment() > 0)] // Modifies counter!\nfn process() { ... }\n\n// RIGHT: Contract is pure\n#[pre(counter.value() > 0)] // Only reads counter\nfn process() { ... }\n```\n\n### Pitfall 2: Expensive Contract Checks\n\n**Problem:** Contract check is O(n) or worse, causing performance issues.\n\n**Solution:**\n```typescript\n// WRONG: O(n) check on every call\nfunction process(items: Item[]) {\n invariant(items.every(i => isValid(i)), \"All items must be valid\");\n // Called millions of times...\n}\n\n// RIGHT: Check once at boundary, trust internally\nfunction publicApi(items: Item[]) {\n const validated = items.filter(isValid); // Validate at boundary\n processInternal(validated); // Internal trusts input\n}\n```\n\n### Pitfall 3: Incomplete Error Context\n\n**Problem:** Contract failure message doesn't help debugging.\n\n**Solution:**\n```python\n# WRONG: No context\nassert x > 0\n\n# RIGHT: Full context\nassert x > 0, f\"Expected positive x, got {x} (type={type(x).__name__}, caller={inspect.stack()[1].function})\"\n```\n\n### Pitfall 4: Contracts Disabled in Production\n\n**Problem:** Critical contracts disabled, bugs reach production.\n\n**Solution:**\n```rust\n// Separate debug-only from critical contracts\n#[cfg(debug_assertions)]\ndebug_assert!(validation_heavy_check()); // Debug only\n\n// Critical contracts always enabled\nassert!(user_id.is_valid(), \"Invalid user ID\"); // Always runs\n```\n\n### Pitfall 5: Circular Contract Dependencies\n\n**Problem:** Contract A checks contract B which checks contract A.\n\n**Solution:**\n```java\n// WRONG: Circular dependency\nclass A {\n @Requires(\"b.isValid()\") // Calls B\n void process(B b) { ... }\n}\nclass B {\n @Requires(\"a.isValid()\") // Calls A, which calls B...\n void validate(A a) { ... }\n}\n\n// RIGHT: Break cycle with primitive checks\nclass A {\n @Requires(\"b.id != null && b.state == State.READY\")\n void process(B b) { ... }\n}\n```\n\n---\n\n## Contract Strength Guidelines\n\n**Too Weak (misses bugs)**\n```python\[email protected](lambda x: True) # Useless\ndef divide(x, y):\n return x / y # Will crash on y=0\n```\n\n**Appropriate Strength**\n```python\[email protected](lambda y: y != 0, \"Divisor must be non-zero\")\[email protected](lambda x, y, result: abs(result * y - x) \u003c 1e-10)\ndef divide(x, y):\n return x / y\n```\n\n**Too Strong (rejects valid inputs)**\n```python\[email protected](lambda x: x > 0 and x \u003c 100) # Overly restrictive\ndef process(x):\n return x * 2 # Works for any number\n```\n\n---\n\n## Contract Composition Patterns\n\n### Layered Contracts\n\n```\nPublic API Layer: [Strong Preconditions]\n |\nService Layer: [Moderate Preconditions]\n |\nDomain Layer: [Minimal Preconditions + Strong Invariants]\n |\nInfrastructure: [Postconditions on I/O]\n```\n\n### Contract Inheritance\n\n```java\n// Base contract\ninterface Processor {\n @Requires(\"input != null\")\n @Ensures(\"result != null\")\n Result process(Input input);\n}\n\n// Subtype strengthens postcondition (allowed)\n// Subtype weakens precondition (allowed)\nclass SafeProcessor implements Processor {\n @Requires(\"true\") // Weaker: accepts any input\n @Ensures(\"result != null && result.isValid()\") // Stronger: guarantees validity\n Result process(Input input) { ... }\n}\n```\n\n### Contract Refinement\n\n```kotlin\n// Start with weak contract, refine as understanding grows\n// Version 1: Basic\nfun process(x: Int): Int {\n require(true) { \"No constraints yet\" }\n // ...\n}\n\n// Version 2: After discovering constraints\nfun process(x: Int): Int {\n require(x > 0) { \"x must be positive\" }\n // ...\n}\n\n// Version 3: After discovering more constraints\nfun process(x: Int): Int {\n require(x in 1..1000) { \"x must be between 1 and 1000\" }\n // ...\n}\n```\n\n---\n\n## When NOT to Use Design-by-Contract\n\n| Scenario | Better Alternative |\n|----------|-------------------|\n| Proving mathematical properties | Proof-driven (Lean 4) |\n| Compile-time guarantees | Type-driven (Idris 2) |\n| Complex state machine correctness | Validation-first (Quint) |\n| Performance-critical inner loops | Disable in release, use types |\n| Third-party library integration | Wrapper with contracts at boundary |\n| Already have strong types | Contracts may be redundant |\n\n---\n\n## Complementary Approaches\n\n- **Contract + Type-driven**: Types encode structure, contracts encode behavior\n- **Contract + Test-driven**: Contracts as executable specs, tests for coverage\n- **Contract + Property-based**: Contracts define valid space, property tests explore it\n\n---\n\n## Safety Requirements\n\n1. **No side effects**: Contract checks must not modify state\n2. **Performance**: Disable expensive checks in release builds\n3. **Thread safety**: Contracts must be thread-safe\n4. **Memory safety**: No allocations in hot paths\n5. **Determinism**: Same inputs produce same contract evaluation\n\n---\n\n## Best Practices\n\n1. **Boundary validation**: Add preconditions at all public API boundaries\n2. **Critical postconditions**: Use postconditions for guarantees that affect downstream code\n3. **State invariants**: Add invariants at construction and after state mutations\n4. **Fail fast**: Include clear error messages with context\n5. **Graduated deployment**: Disable expensive contracts in production (when safe)\n6. **Type composition**: Combine contracts with type system for compile-time checks\n7. **Documentation**: Document contract rationale in comments\n8. **Testing**: Test contract violations explicitly in unit tests\n\n---\n\n## Performance Considerations\n\n| Aspect | Development | Production |\n|--------|-------------|------------|\n| Preconditions | Always enabled | Critical only |\n| Postconditions | Always enabled | Disabled |\n| Invariants | Full checking | Disabled |\n| Logging | Verbose | Minimal |\n| Cost per check | O(1) acceptable | O(1) required |\n\n### Optimization Strategies\n\n```rust\n// Conditional compilation\n#[cfg(debug_assertions)]\nfn expensive_check() { ... }\n\n// Feature flags\n#[cfg(feature = \"contracts\")]\nfn contract_check() { ... }\n\n// Inline for hot paths\n#[inline(always)]\nfn fast_precondition() { ... }\n```\n\n---\n\n## Integration Workflow\n\n```nomnoml\n[\u003cstart>Start] -> [dbc-detect]\n[dbc-detect] found contracts -> [dbc-verify]\n[dbc-detect] no contracts -> [dbc-remediate --add-missing]\n[dbc-verify] pass -> [\u003cend>Success]\n[dbc-verify] fail -> [dbc-remediate --fix-violations]\n[dbc-remediate --add-missing] -> [dbc-verify]\n[dbc-remediate --fix-violations] -> [dbc-verify]\n```\n\n---\n\n## Resources\n\n- [Design by Contract (Meyer)](https://en.wikipedia.org/wiki/Design_by_contract)\n- [Eiffel: Birthplace of DbC](https://www.eiffel.com/values/design-by-contract/)\n- [Microsoft Code Contracts](https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts)\n- [Rust contracts crate](https://crates.io/crates/contracts)\n- [Python icontract](https://github.com/Parquery/icontract)\n- [TypeScript zod](https://github.com/colinhacks/zod)\n---","attachment_filenames":["metadata.json"],"attachments":[{"filename":"metadata.json","content":"{\n \"id\": \"outlinedriven-odin-claude-plugin-skills-design-by-contract-skill-md\",\n \"name\": \"design-by-contract\",\n \"author\": \"OutlineDriven\",\n \"authorAvatar\": \"https://avatars.githubusercontent.com/u/244415305?v=4\",\n \"description\": \"Automated contract verification, detection, and remediation across multiple languages using formal preconditions, postconditions, and invariants. This skill provides both reference documentation AND execution capabilities for the full PLAN -> CREATE -> VERIFY -> REMEDIATE workflow.\",\n \"githubUrl\": \"https://github.com/OutlineDriven/odin-claude-plugin/tree/main/skills/design-by-contract\",\n \"stars\": 2,\n \"forks\": 0,\n \"updatedAt\": 1764377455,\n \"hasMarketplace\": true,\n \"path\": \"SKILL.md\",\n \"branch\": \"main\"\n}","content_type":"application/json; charset=utf-8","language":"json","size":749,"content_sha256":"fc63222abb88feb6ce4f49f78960ea778d4372e8799db4241e8669255a8ac3a7"}],"content_json":{"type":"doc","content":[{"type":"heading","attrs":{"level":1},"content":[{"text":"Design-by-Contract Development Skill","type":"text"}]},{"type":"heading","attrs":{"level":2},"content":[{"text":"Capability","type":"text"}]},{"type":"paragraph","content":[{"text":"Design-by-Contract (DbC) is a programming methodology that uses formal specifications (contracts) to define component behavior. This skill enables:","type":"text"}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Contract Design","type":"text","marks":[{"type":"strong"}]},{"text":": Plan preconditions, postconditions, and invariants before implementation","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Artifact Generation","type":"text","marks":[{"type":"strong"}]},{"text":": Create contract annotations across 8+ languages","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Verification","type":"text","marks":[{"type":"strong"}]},{"text":": Run contract validation with appropriate runtime flags","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Remediation","type":"text","marks":[{"type":"strong"}]},{"text":": Fix contract violations with targeted debugging","type":"text"}]}]}]},{"type":"paragraph","content":[{"text":"Core Contract Types:","type":"text","marks":[{"type":"strong"}]}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Preconditions","type":"text","marks":[{"type":"strong"}]},{"text":": What must be true before a function executes (caller's duty)","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Postconditions","type":"text","marks":[{"type":"strong"}]},{"text":": What must be true after a function executes (callee's promise)","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Invariants","type":"text","marks":[{"type":"strong"}]},{"text":": What must always be true about object state","type":"text"}]}]}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"When to Use","type":"text"}]},{"type":"paragraph","content":[{"text":"Design-by-Contract is ideal for:","type":"text"}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Public API boundaries","type":"text","marks":[{"type":"strong"}]},{"text":": Validate inputs at module boundaries","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Critical business logic","type":"text","marks":[{"type":"strong"}]},{"text":": Ensure computation correctness","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"State management","type":"text","marks":[{"type":"strong"}]},{"text":": Maintain object consistency","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Integration points","type":"text","marks":[{"type":"strong"}]},{"text":": Verify data crossing system boundaries","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Team collaboration","type":"text","marks":[{"type":"strong"}]},{"text":": Document expected behavior formally","type":"text"}]}]}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Workflow Overview","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"nomnoml"},"content":[{"text":"[\u003cstart>Requirements] -> [Phase 1: PLAN]\n[Phase 1: PLAN|\n Identify contracts\n Design predicates\n Map obligations\n] -> [Phase 2: CREATE]\n[Phase 2: CREATE|\n Generate annotations\n Add to .outline/contracts/\n Wire dependencies\n] -> [Phase 3: VERIFY]\n[Phase 3: VERIFY|\n Enable runtime flags\n Run test suite\n Check violations\n] -> [Phase 4: REMEDIATE]\n[Phase 4: REMEDIATE|\n Diagnose violation type\n Fix caller/callee/state\n Re-verify\n] -> [\u003cend>Success]","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Verification Hierarchy","type":"text"}]},{"type":"paragraph","content":[{"text":"Principle","type":"text","marks":[{"type":"strong"}]},{"text":": Use compile-time verification before runtime contracts. If a property can be verified statically, do NOT add a runtime contract for it.","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":""},"content":[{"text":"Static Assertions (compile-time) > Test/Debug Contracts > Runtime Contracts","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"When to Use Each Level","type":"text"}]},{"type":"table","attrs":{"layout":null},"content":[{"type":"tr","content":[{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Property","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Static","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Test Contract","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Debug Contract","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Runtime Contract","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Type size/alignment","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"static_assert","type":"text","marks":[{"type":"code_inline"}]},{"text":" (C++), ","type":"text"},{"text":"assert_eq_size!","type":"text","marks":[{"type":"code_inline"}]},{"text":" (Rust)","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Trait/interface bounds","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"assert_impl_all!","type":"text","marks":[{"type":"code_inline"}]},{"text":" (Rust), Concepts (C++)","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Const value bounds","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"const_assert!","type":"text","marks":[{"type":"code_inline"}]},{"text":", ","type":"text"},{"text":"static_assert","type":"text","marks":[{"type":"code_inline"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Null/type safety","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Type checker (tsc/pyright/kotlinc)","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Exhaustiveness","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Pattern matching + ","type":"text"},{"text":"never","type":"text","marks":[{"type":"code_inline"}]},{"text":"/","type":"text"},{"text":"Never","type":"text","marks":[{"type":"code_inline"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Expensive O(n)+ checks","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"test_ensures","type":"text","marks":[{"type":"code_inline"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Reference impl equivalence","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"test_ensures","type":"text","marks":[{"type":"code_inline"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Internal state invariants","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"debug_invariant","type":"text","marks":[{"type":"code_inline"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Development preconditions","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"debug_requires","type":"text","marks":[{"type":"code_inline"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Public API input validation","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"requires","type":"text","marks":[{"type":"code_inline"}]}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Safety-critical postconditions","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"ensures","type":"text","marks":[{"type":"code_inline"}]}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"External/untrusted data","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"-","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Required (Zod/icontract)","type":"text"}]}]}]}]},{"type":"paragraph","content":[{"text":"Legend","type":"text","marks":[{"type":"strong"}]},{"text":": ","type":"text"},{"text":"-","type":"text","marks":[{"type":"code_inline"}]},{"text":" = Do not use for this property","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Decision Flow","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":""},"content":[{"text":"Can type system encode it? ──yes──> Use types (typestate, newtype)\n │no\n v\nVerifiable at compile-time? ──yes──> static_assertions / const_assert!\n │no\n v\nExpensive O(n)+ check? ──yes──> test_* (test builds only)\n │no\n v\nInternal development aid? ──yes──> debug_* (debug builds only)\n │no\n v\nMust enforce in production? ──yes──> Runtime contracts\n │no\n v\nConsider if check is needed at all","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Phase 1: PLAN (Contract Design)","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Process","type":"text"}]},{"type":"ordered_list","attrs":{"order":1,"listStyle":"number"},"content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Understand Requirements","type":"text","marks":[{"type":"strong"}]}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Parse user's task/requirement","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Identify preconditions, postconditions, invariants","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Use sequential-thinking to decompose contract obligations","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Map requirements to contract types","type":"text"}]}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Artifact Detection (Conditional)","type":"text","marks":[{"type":"strong"}]}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Check for existing contract artifacts by language:","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Rust (contracts crate)\nrg '#\\[pre\\(|#\\[post\\(|#\\[invariant\\(' $ARGUMENTS\n# TypeScript (Zod)\nrg 'z\\.object|z\\.string|\\.refine\\(' $ARGUMENTS\n# Python (icontract)\nrg '@pre\\(|@post\\(|@invariant\\(' $ARGUMENTS\n# Java/Kotlin\nrg 'checkArgument|checkState|require\\s*\\{' $ARGUMENTS","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"If artifacts exist: analyze coverage gaps, plan extensions","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"If no artifacts: proceed to design contract architecture","type":"text"}]}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Design Contract Architecture","type":"text","marks":[{"type":"strong"}]}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Design precondition predicates","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Plan postcondition guarantees","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Define class/module invariants","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Output: Contract design with annotation signatures","type":"text"}]}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Prepare Run Phase","type":"text","marks":[{"type":"strong"}]}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Define target: ","type":"text"},{"text":".outline/contracts/","type":"text","marks":[{"type":"code_inline"}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Specify verification: language-specific contract checking","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Create traceability: requirement -> contract -> enforcement","type":"text"}]}]}]}]}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Thinking Tool Integration","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":""},"content":[{"text":"Use sequential-thinking for:\n- Contract decomposition\n- Obligation ordering\n- Inheritance chain planning\n\nUse actor-critic-thinking for:\n- Contract strength evaluation\n- Precondition completeness\n- Postcondition sufficiency\n\nUse shannon-thinking for:\n- Contract coverage gaps\n- Runtime verification costs\n- Weakest precondition analysis","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Contract Design Templates","type":"text"}]},{"type":"heading","attrs":{"level":4},"content":[{"text":"Rust (contracts crate)","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"rust"},"content":[{"text":"// Target: .outline/contracts/{module}_contracts.rs\n\n// From requirement: {requirement text}\n#[pre(input > 0, \"Input must be positive\")]\n#[post(ret.is_some() => ret.unwrap() > input)]\nfn process(input: i32) -> Option\u003ci32> {\n // Implementation in run phase\n}\n\n// Class invariant\n#[invariant(self.balance >= 0)]\nimpl Account {\n // Methods maintain invariant\n}","type":"text"}]},{"type":"heading","attrs":{"level":4},"content":[{"text":"TypeScript (Zod)","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"typescript"},"content":[{"text":"// Target: .outline/contracts/{module}.contracts.ts\n\n// From requirement: {requirement text}\nconst InputSchema = z.object({\n value: z.number().positive(\"Value must be positive\"),\n}).refine(\n (data) => /* precondition */,\n { message: \"Precondition: {description}\" }\n);\n\n// Postcondition validator\nconst OutputSchema = z.object({\n result: z.number(),\n}).refine(\n (data) => /* postcondition */,\n { message: \"Postcondition: {description}\" }\n);","type":"text"}]},{"type":"heading","attrs":{"level":4},"content":[{"text":"Python (icontract)","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"python"},"content":[{"text":"# Target: .outline/contracts/{module}_contracts.py\n\n# From requirement: {requirement text}\[email protected](lambda x: x > 0, \"Input must be positive\")\[email protected](lambda result: result is not None)\ndef process(x: int) -> Optional[int]:\n # Implementation in run phase\n pass","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Plan Output","type":"text"}]},{"type":"ordered_list","attrs":{"order":1,"listStyle":"number"},"content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Requirements Analysis","type":"text","marks":[{"type":"strong"}]}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Preconditions identified","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Postconditions guaranteed","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Invariants to maintain","type":"text"}]}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Contract Architecture","type":"text","marks":[{"type":"strong"}]}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Contract signatures per function/method","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Invariant definitions per class/module","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Inheritance contract chains","type":"text"}]}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Target Artifacts","type":"text","marks":[{"type":"strong"}]}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":".outline/contracts/*","type":"text","marks":[{"type":"code_inline"}]},{"text":" file list","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Contract library dependencies","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Runtime flag configuration","type":"text"}]}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Verification Commands","type":"text","marks":[{"type":"strong"}]}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Build with contracts enabled","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Test suite exercising contracts","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Success criteria: no contract violations","type":"text"}]}]}]}]}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Phase 2: CREATE (Generate Artifacts)","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Setup","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Create .outline/contracts directory\nmkdir -p .outline/contracts","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Generate Contract Files by Language","type":"text"}]},{"type":"heading","attrs":{"level":4},"content":[{"text":"Rust (contracts crate)","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"rust"},"content":[{"text":"// .outline/contracts/{module}_contracts.rs\n// Generated from plan design\n\nuse contracts::*;\n\n// Source Requirement: {traceability from plan}\n\n// Precondition: {from plan design}\n// Postcondition: {from plan design}\n#[pre(input > 0, \"Input must be positive\")]\n#[post(ret.is_some() => ret.unwrap() > input, \"Output must exceed input\")]\npub fn process(input: i32) -> Option\u003ci32> {\n // Implementation\n Some(input + 1)\n}\n\n// Class invariant: {from plan design}\n#[invariant(self.balance >= 0, \"Balance must be non-negative\")]\nimpl Account {\n #[post(self.balance == old(self.balance) + amount)]\n pub fn deposit(&mut self, amount: u64) {\n self.balance += amount;\n }\n}","type":"text"}]},{"type":"heading","attrs":{"level":4},"content":[{"text":"TypeScript (Zod)","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"typescript"},"content":[{"text":"// .outline/contracts/{module}.contracts.ts\n// Generated from plan design\n\nimport { z } from 'zod';\n\n// Source Requirement: {traceability from plan}\n\n// Precondition schema: {from plan design}\nexport const InputSchema = z.object({\n value: z.number().positive(\"Value must be positive\"),\n name: z.string().min(1, \"Name required\"),\n}).refine(\n (data) => data.value \u003c 1000,\n { message: \"Precondition: value must be under 1000\" }\n);\n\n// Postcondition schema: {from plan design}\nexport const OutputSchema = z.object({\n result: z.number(),\n success: z.boolean(),\n}).refine(\n (data) => data.success || data.result === 0,\n { message: \"Postcondition: failed operations must return 0\" }\n);\n\n// Validation wrapper\nexport function withContracts\u003cI, O>(\n inputSchema: z.ZodType\u003cI>,\n outputSchema: z.ZodType\u003cO>,\n fn: (input: I) => O\n): (input: I) => O {\n return (input: I) => {\n const validInput = inputSchema.parse(input);\n const output = fn(validInput);\n return outputSchema.parse(output);\n };\n}","type":"text"}]},{"type":"heading","attrs":{"level":4},"content":[{"text":"Python (icontract)","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"python"},"content":[{"text":"# .outline/contracts/{module}_contracts.py\n# Generated from plan design\n\nimport icontract\n\n# Source Requirement: {traceability from plan}\n\n# Precondition: {from plan design}\n# Postcondition: {from plan design}\[email protected](lambda x: x > 0, \"Input must be positive\")\[email protected](lambda result: result is not None, \"Must return value\")\[email protected](lambda x, result: result > x, \"Output must exceed input\")\ndef process(x: int) -> int:\n return x + 1\n\n\n# Class invariant: {from plan design}\[email protected](lambda self: self.balance >= 0)\nclass Account:\n def __init__(self):\n self.balance = 0\n\n @icontract.require(lambda amount: amount > 0)\n @icontract.ensure(lambda self, amount, OLD: self.balance == OLD.balance + amount)\n def deposit(self, amount: int) -> None:\n self.balance += amount","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Phase 3: VERIFY (Contract Validation)","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Rust","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Ensure contracts are enabled (not disabled)\nunset CONTRACTS_DISABLE\n\n# Verify contracts exist\nrg '#\\[pre\\(|#\\[post\\(|#\\[invariant\\(' .outline/contracts/ || exit 12\n\n# Run tests with contracts\ncargo test || exit 13","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"TypeScript","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Verify Zod schemas exist\nrg 'z\\.object|\\.refine\\(' .outline/contracts/ || exit 12\n\n# Run tests (Zod validates at runtime)\nnpx vitest run || exit 13","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Python","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Enable thorough contract checking\nexport ICONTRACT_SLOW=true\n\n# Verify decorators exist\nrg '@icontract\\.(require|ensure|invariant)' .outline/contracts/ || exit 12\n\n# Run tests\npytest || exit 13","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Java (Guava)","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Verify Guava preconditions exist\nrg 'checkArgument|checkState|checkNotNull' .outline/contracts/ || exit 12\n\n# Run tests\nmvn test || exit 13","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"C++ (GSL/Boost)","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Ensure NDEBUG is NOT set for contract checking\nunset NDEBUG\n\n# Verify contracts exist\nrg 'Expects\\(|Ensures\\(' .outline/contracts/ || exit 12\n\n# Build and test\ncmake --build build && ./build/tests || exit 13","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Phase 4: REMEDIATE (Fix Violations)","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Contract Violation Types","type":"text"}]},{"type":"table","attrs":{"layout":null},"content":[{"type":"tr","content":[{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Violation","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Exit Code","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Fix Strategy","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Precondition","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"1","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Fix caller to meet requirements","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Postcondition","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"2","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Fix implementation to meet guarantee","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Invariant","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"3","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Fix state management logic","type":"text"}]}]}]}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Debugging by Violation Type","type":"text"}]},{"type":"paragraph","content":[{"text":"Precondition Violation (Caller's fault)","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":"python"},"content":[{"text":"# Error: icontract.ViolationError: Pre: x > 0\n# The CALLER passed invalid input\n\n# Debug: Check call site\n# Before:\nresult = process(-5) # WRONG: violates x > 0\n\n# After:\nif x > 0:\n result = process(x)\nelse:\n handle_invalid_input(x)","type":"text"}]},{"type":"paragraph","content":[{"text":"Postcondition Violation (Callee's fault)","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":"python"},"content":[{"text":"# Error: icontract.ViolationError: Post: result > x\n# The IMPLEMENTATION doesn't meet its guarantee\n\n# Debug: Fix the function\n# Before:\[email protected](lambda x, result: result > x)\ndef process(x: int) -> int:\n return x # WRONG: not > x\n\n# After:\[email protected](lambda x, result: result > x)\ndef process(x: int) -> int:\n return x + 1 # Correct","type":"text"}]},{"type":"paragraph","content":[{"text":"Invariant Violation (State corruption)","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":"python"},"content":[{"text":"# Error: icontract.ViolationError: Inv: self.balance >= 0\n# Object state became invalid after operation\n\n# Debug: Find state mutation that breaks invariant\n# Before:\[email protected](lambda self: self.balance >= 0)\nclass Account:\n def withdraw(self, amount):\n self.balance -= amount # WRONG: can go negative\n\n# After:\n @icontract.require(lambda self, amount: amount \u003c= self.balance)\n def withdraw(self, amount):\n self.balance -= amount # Now protected by precondition","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Contract Patterns","type":"text"}]},{"type":"paragraph","content":[{"text":"Precondition (Caller's Duty)","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":""},"content":[{"text":"INPUT --> VALIDATE --> PROCESS\n |\n v\n FAIL FAST if invalid","type":"text"}]},{"type":"paragraph","content":[{"text":"Postcondition (Callee's Promise)","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":""},"content":[{"text":"PROCESS --> OUTPUT --> VALIDATE\n |\n v\n ASSERT guarantee met","type":"text"}]},{"type":"paragraph","content":[{"text":"Invariant (Always True)","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":""},"content":[{"text":"OPERATION --> STATE CHANGE --> CHECK INVARIANT\n |\n v\n ASSERT still valid","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Commands Reference","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"dbc-verify","type":"text"}]},{"type":"paragraph","content":[{"text":"Verify all contracts satisfied in codebase.","type":"text"}]},{"type":"paragraph","content":[{"text":"Usage","type":"text","marks":[{"type":"strong"}]},{"text":": ","type":"text"},{"text":"dbc-verify [--lang LANG] [--path PATH] [--runtime-flags]","type":"text","marks":[{"type":"code_inline"}]}]},{"type":"paragraph","content":[{"text":"Algorithm","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":""},"content":[{"text":"1. Detect language(s) in scope (fd file extensions)\n2. Check runtime flags enabled per language\n3. Scan for contract library usage (rg patterns)\n4. Execute language-specific verification\n5. Report violations with exit codes","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"dbc-detect","type":"text"}]},{"type":"paragraph","content":[{"text":"Detect contract usage and missing contracts.","type":"text"}]},{"type":"paragraph","content":[{"text":"Usage","type":"text","marks":[{"type":"strong"}]},{"text":": ","type":"text"},{"text":"dbc-detect [--lang LANG] [--missing] [--violations]","type":"text","marks":[{"type":"code_inline"}]}]},{"type":"paragraph","content":[{"text":"Algorithm","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":""},"content":[{"text":"1. Scan for contract library imports (rg)\n2. Find functions without contracts (ast-grep negative match)\n3. Identify contract violations (pattern analysis)\n4. Generate coverage report","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"dbc-remediate","type":"text"}]},{"type":"paragraph","content":[{"text":"Auto-fix violations or add missing contracts.","type":"text"}]},{"type":"paragraph","content":[{"text":"Usage","type":"text","marks":[{"type":"strong"}]},{"text":": ","type":"text"},{"text":"dbc-remediate [--add-missing] [--fix-violations] [--dry-run]","type":"text","marks":[{"type":"code_inline"}]}]},{"type":"paragraph","content":[{"text":"Algorithm","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":""},"content":[{"text":"1. Identify remediation targets (missing/violated contracts)\n2. Generate contract code per language\n3. Apply fixes via ast-grep or native-patch\n4. Verify fixes with dbc-verify","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Exit Codes","type":"text"}]},{"type":"table","attrs":{"layout":null},"content":[{"type":"tr","content":[{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Code","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Meaning","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Action","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"0","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"All contracts pass","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Ready for deployment","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"1","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Precondition fail","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Fix caller to meet requirements","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"2","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Postcondition fail","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Fix implementation","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"3","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Invariant fail","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Fix state management","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"11","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Library missing","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Install contract library","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"12","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"No contracts","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Run plan phase, create contracts","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"13","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Verification failed","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Debug and fix violations","type":"text"}]}]}]}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Language-Specific Implementations","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Rust Detection","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Find contracts\nrg '#\\[pre\\(|#\\[post\\(|#\\[invariant\\(|debug_assert!' --type rust\n\n# Find functions without contracts\nast-grep -p 'fn $NAME($$) { $$ }' -l rust | \\\n rg -v '#\\[pre\\(|debug_assert!' --files-without-match","type":"text"}]},{"type":"paragraph","content":[{"text":"Remediation template","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"rust"},"content":[{"text":"#[pre($CONDITION)]\n#[post(ret $POSTCONDITION)]\nfn $NAME($PARAMS) -> $RET {\n debug_assert!($CONDITION, \"$ERROR_MSG\");\n $BODY\n}","type":"text"}]},{"type":"paragraph","content":[{"text":"Runtime flags","type":"text","marks":[{"type":"strong"}]},{"text":": Check ","type":"text"},{"text":"CARGO_BUILD_TYPE != release","type":"text","marks":[{"type":"code_inline"}]},{"text":" or ","type":"text"},{"text":"cfg(debug_assertions)","type":"text","marks":[{"type":"code_inline"}]}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"TypeScript Detection","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Find contracts\nrg 'z\\.object|invariant\\(|\\.parse\\(|\\.safeParse\\(' --type ts\n\n# Find functions without validation\nast-grep -p 'function $NAME($$): $$ { $$ }' -l typescript | \\\n rg -v 'z\\.|invariant' --files-without-match","type":"text"}]},{"type":"paragraph","content":[{"text":"Remediation template","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"typescript"},"content":[{"text":"const ${NAME}Schema = z.object({\n $FIELDS\n});\n\nfunction $NAME(params: unknown): $RET {\n const validated = ${NAME}Schema.parse(params);\n invariant($CONDITION, \"$ERROR_MSG\");\n $BODY\n}","type":"text"}]},{"type":"paragraph","content":[{"text":"Runtime flags","type":"text","marks":[{"type":"strong"}]},{"text":": Check ","type":"text"},{"text":"process.env.NODE_ENV === 'development'","type":"text","marks":[{"type":"code_inline"}]}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Python Detection","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Find contracts\nrg '@pre\\(|@post\\(|@invariant|@require|@ensure' --type python\n\n# Find functions without contracts\nast-grep -p 'def $NAME($$): $

Important: agents should read /llm.txt, /llms.txt, or /.well-known/skills.json to discover the public Skillopedia API.

-l python | \\\n rg -v '@pre|@post|@invariant' --files-without-match","type":"text"}]},{"type":"paragraph","content":[{"text":"Remediation template","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"python"},"content":[{"text":"@pre(lambda $PARAMS: $CONDITION)\n@post(lambda result: $POSTCONDITION)\ndef $NAME($PARAMS) -> $RET:\n \"\"\"$DOCSTRING\"\"\"\n $BODY","type":"text"}]},{"type":"paragraph","content":[{"text":"Runtime flags","type":"text","marks":[{"type":"strong"}]},{"text":": Check ","type":"text"},{"text":"__debug__","type":"text","marks":[{"type":"code_inline"}]},{"text":" is True (not ","type":"text"},{"text":"python -O","type":"text","marks":[{"type":"code_inline"}]},{"text":")","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Java Detection","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Find contracts\nrg 'checkArgument|checkState|validate\\(|Preconditions\\.' --type java\n\n# Find methods without contracts\nast-grep -p 'public $RET $NAME($$) { $$ }' -l java | \\\n rg -v 'checkArgument|validate' --files-without-match","type":"text"}]},{"type":"paragraph","content":[{"text":"Remediation template","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"java"},"content":[{"text":"public $RET $NAME($PARAMS) {\n checkArgument($CONDITION, \"$ERROR_MSG\");\n $BODY\n validate($POSTCONDITION, \"$POST_ERROR\");\n return $RESULT;\n}","type":"text"}]},{"type":"paragraph","content":[{"text":"Runtime flags","type":"text","marks":[{"type":"strong"}]},{"text":": Check assertions enabled with ","type":"text"},{"text":"-ea","type":"text","marks":[{"type":"code_inline"}]},{"text":" flag","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Kotlin Detection","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Find contracts\nrg 'contract \\{|Either\u003c|Validated|require\\(|check\\(' --type kotlin\n\n# Find functions without contracts\nast-grep -p 'fun $NAME($$): $$ { $$ }' -l kotlin | \\\n rg -v 'contract|require|check' --files-without-match","type":"text"}]},{"type":"paragraph","content":[{"text":"Remediation template","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"kotlin"},"content":[{"text":"fun $NAME($PARAMS): Either\u003c$ERR, $RET> {\n contract {\n returns() implies ($CONDITION)\n }\n return if (!$CONDITION) \"$ERROR\".left()\n else { $BODY }.right()\n}","type":"text"}]},{"type":"paragraph","content":[{"text":"Runtime flags","type":"text","marks":[{"type":"strong"}]},{"text":": Check ","type":"text"},{"text":"-ea","type":"text","marks":[{"type":"code_inline"}]},{"text":" for JVM assertions","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"C# Detection","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Find contracts\nrg 'Guard\\.Against|Contract\\.Requires|Contract\\.Ensures|Debug\\.Assert' --type cs\n\n# Find methods without contracts\nast-grep -p 'public $RET $NAME($$) { $$ }' -l csharp | \\\n rg -v 'Guard\\.|Contract\\.' --files-without-match","type":"text"}]},{"type":"paragraph","content":[{"text":"Remediation template","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"csharp"},"content":[{"text":"public $RET $NAME($PARAMS) {\n Guard.Against.Null($PARAM, nameof($PARAM));\n Contract.Ensures(Contract.Result\u003c$RET>() $POSTCONDITION);\n $BODY\n}","type":"text"}]},{"type":"paragraph","content":[{"text":"Runtime flags","type":"text","marks":[{"type":"strong"}]},{"text":": Check Debug configuration","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"C++ Detection","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Find contracts\nrg 'Expects\\(|Ensures\\(|boost::contract|gsl::' --type cpp\n\n# Find functions without contracts\nast-grep -p '$RET $NAME($$) { $$ }' -l cpp | \\\n rg -v 'Expects|Ensures' --files-without-match","type":"text"}]},{"type":"paragraph","content":[{"text":"Remediation template","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"cpp"},"content":[{"text":"$RET $NAME($PARAMS) {\n Expects($PRECONDITION);\n $BODY\n Ensures($POSTCONDITION);\n return $RESULT;\n}","type":"text"}]},{"type":"paragraph","content":[{"text":"Runtime flags","type":"text","marks":[{"type":"strong"}]},{"text":": Check ","type":"text"},{"text":"NDEBUG","type":"text","marks":[{"type":"code_inline"}]},{"text":" not defined","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"C Detection","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Find contracts\nrg 'assert\\(|static_assert' --type c\n\n# Find functions without asserts\nast-grep -p '$RET $NAME($$) { $$ }' -l c | \\\n rg -v 'assert\\(' --files-without-match","type":"text"}]},{"type":"paragraph","content":[{"text":"Remediation template","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"c"},"content":[{"text":"$RET $NAME($PARAMS) {\n assert($PRECONDITION && \"$ERROR_MSG\");\n $BODY\n assert($POSTCONDITION && \"$POST_ERROR\");\n return $RESULT;\n}","type":"text"}]},{"type":"paragraph","content":[{"text":"Runtime flags","type":"text","marks":[{"type":"strong"}]},{"text":": Check ","type":"text"},{"text":"NDEBUG","type":"text","marks":[{"type":"code_inline"}]},{"text":" not defined","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Contract Library Matrix","type":"text"}]},{"type":"table","attrs":{"layout":null},"content":[{"type":"tr","content":[{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Language","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Library","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Runtime Flag","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Rust","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"contracts","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"CONTRACTS_DISABLE","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"TypeScript","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Zod","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"(always active)","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Python","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"icontract","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"ICONTRACT_SLOW","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Java","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Guava","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"(always active)","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Kotlin","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"native","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"(always active)","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"C#","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Guard","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"(always active)","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"C++","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"GSL/Boost","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"NDEBUG","type":"text"}]}]}]}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Error Handling Matrix","type":"text"}]},{"type":"table","attrs":{"layout":null},"content":[{"type":"tr","content":[{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Language","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Contract Library","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Error Type","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Error Handling","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Recovery Strategy","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Rust","type":"text","marks":[{"type":"strong"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"contracts, prusti","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"panic!","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"catch_unwind","type":"text","marks":[{"type":"code_inline"}]},{"text":" (discouraged)","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Result/Option types","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"TypeScript","type":"text","marks":[{"type":"strong"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"zod, io-ts","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"ZodError, thrown","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"try/catch","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Either/Result pattern","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Python","type":"text","marks":[{"type":"strong"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"dpcontracts, icontract","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"AssertionError","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"try/except","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Optional/Result","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Java","type":"text","marks":[{"type":"strong"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Guava, Bean Validation","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"IllegalArgumentException","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"try/catch","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Optional/Either","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Kotlin","type":"text","marks":[{"type":"strong"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Arrow, require/check","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"IllegalArgumentException","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"try/catch","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Either\u003cE, A>","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"C#","type":"text","marks":[{"type":"strong"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Code Contracts, Guard","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"ArgumentException","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"try/catch","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Result\u003cT>","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"C++","type":"text","marks":[{"type":"strong"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"GSL, Boost.Contract","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"std::terminate","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"noexcept","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"std::expected","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"C","type":"text","marks":[{"type":"strong"}]}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"assert.h","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"abort()","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Signal handler","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Return codes","type":"text"}]}]}]}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Error Message Best Practices","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":""},"content":[{"text":"Contract Type: [PRECONDITION|POSTCONDITION|INVARIANT]\nLocation: file.rs:42 in function_name()\nCondition: x > 0 && x \u003c 100\nActual Value: x = -5\nExpected: Positive integer less than 100\nContext: Processing user input for order ID","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Troubleshooting Guide","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Common Issues","type":"text"}]},{"type":"table","attrs":{"layout":null},"content":[{"type":"tr","content":[{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Symptom","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Cause","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Resolution","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Exit 1","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Precondition violation","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Caller must provide valid input (fix call site)","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Exit 2","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Postcondition violation","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Implementation doesn't meet guarantee (fix function)","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Exit 3","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Invariant violation","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Object state became invalid (fix state mutation)","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Exit 11","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Contract library missing","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Install: ","type":"text"},{"text":"pip install icontract","type":"text","marks":[{"type":"code_inline"}]},{"text":", ","type":"text"},{"text":"cargo add contracts","type":"text","marks":[{"type":"code_inline"}]},{"text":", ","type":"text"},{"text":"npm i zod","type":"text","marks":[{"type":"code_inline"}]}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Exit 12","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"No contract annotations","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Run plan phase first","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Exit 13","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Tests failed with contracts","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Debug violation type","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"CONTRACTS_DISABLE","type":"text","marks":[{"type":"code_inline"}]},{"text":" set","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Contracts silently skipped","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"unset CONTRACTS_DISABLE","type":"text","marks":[{"type":"code_inline"}]}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"No error but wrong behavior","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Contract too weak","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Strengthen pre/post conditions","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Performance impact","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Contracts in hot path","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Use ","type":"text"},{"text":"@icontract.require(enabled=DEBUG)","type":"text","marks":[{"type":"code_inline"}]}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Contract not firing","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Debug assertions disabled","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Check ","type":"text"},{"text":"NDEBUG","type":"text","marks":[{"type":"code_inline"}]},{"text":", ","type":"text"},{"text":"-O","type":"text","marks":[{"type":"code_inline"}]},{"text":" flags","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"False positive","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Contract too strict","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Review expected vs actual","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"False negative","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Contract too weak","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Add edge case tests","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Stack overflow","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Recursive contract","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Check for cycles","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Flaky failures","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Race condition in contract","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Add synchronization","type":"text"}]}]}]}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Quick Diagnostics","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Check if contracts are enabled (Rust)\ncargo build && rg 'debug_assert' target/debug/*.d\n\n# Check if contracts are enabled (Node.js)\nnode -e \"console.log(process.env.NODE_ENV)\"\n\n# Check if assertions enabled (Java)\njava -ea -version 2>&1 | head -1\n\n# Check if assertions enabled (C/C++)\ncpp -dM /dev/null | grep NDEBUG","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Debugging Commands","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Python - Verbose contract errors\nICONTRACT_SLOW=true pytest -v --tb=long\n\n# Python - Find contract decorators\nrg '@icontract\\.(require|ensure|invariant)' src/\n\n# Rust - Enable backtrace\nRUST_BACKTRACE=1 cargo test\n\n# Rust - Find contract attributes\nrg '#\\[(pre|post|invariant)\\(' src/\n\n# TypeScript - Verbose Zod errors\nDEBUG=zod:* npm test\n\n# TypeScript - Find Zod schemas\nrg 'z\\.(object|refine|string|number)' src/\n\n# General - Check contracts not disabled\nenv | rg -i 'contract|ndebug'","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Debugging Contract Violation Workflows","type":"text"}]},{"type":"heading","attrs":{"level":4},"content":[{"text":"Precondition Violation Debugging","type":"text"}]},{"type":"ordered_list","attrs":{"order":1,"listStyle":"number"},"content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Identify the violation location","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"bash"},"content":[{"text":"# Run with debug symbols\nRUST_BACKTRACE=1 cargo run # Rust\nnode --enable-source-maps # Node.js\npython -c \"import traceback\" # Python","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Examine the call stack","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Find the caller that provided invalid input","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Check intermediate transformations that corrupted data","type":"text"}]}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Add tracing at contract boundary","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"rust"},"content":[{"text":"// Rust example\n#[pre(x > 0)]\nfn process(x: i32) {\n tracing::debug!(\"process called with x = {}\", x);\n // ...\n}","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Common causes","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Unvalidated user input","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Null/None propagation","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Integer overflow in computation","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Incorrect API usage","type":"text"}]}]}]}]}]},{"type":"heading","attrs":{"level":4},"content":[{"text":"Postcondition Violation Debugging","type":"text"}]},{"type":"ordered_list","attrs":{"order":1,"listStyle":"number"},"content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Instrument the function exit","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"typescript"},"content":[{"text":"// TypeScript example\nfunction calculate(x: number): number {\n const result = /* computation */;\n console.log(`calculate returning: ${result}`);\n invariant(result > 0, `Expected positive, got ${result}`);\n return result;\n}","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Check intermediate state","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Add assertions at each computation step","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Verify loop invariants maintained","type":"text"}]}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Common causes","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Logic error in computation","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Incorrect formula","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Edge case not handled","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Floating point precision loss","type":"text"}]}]}]}]}]},{"type":"heading","attrs":{"level":4},"content":[{"text":"Invariant Violation Debugging","type":"text"}]},{"type":"ordered_list","attrs":{"order":1,"listStyle":"number"},"content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Track state transitions","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"python"},"content":[{"text":"# Python example with dpcontracts\n@invariant(lambda self: self.balance >= 0)\nclass Account:\n def __init__(self):\n self._log_state(\"init\")\n\n def withdraw(self, amount):\n self._log_state(f\"before withdraw {amount}\")\n self.balance -= amount\n self._log_state(f\"after withdraw {amount}\")","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Find mutation that breaks invariant","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Identify all state-mutating methods","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Check each mutation point","type":"text"}]}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Common causes","type":"text","marks":[{"type":"strong"}]},{"text":":","type":"text"}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Missing validation in setter","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Concurrent modification","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Deserialization bypassing constructor","type":"text"}]}]}]}]}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Common Pitfalls and Solutions","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Pitfall 1: Contracts with Side Effects","type":"text"}]},{"type":"paragraph","content":[{"text":"Problem:","type":"text","marks":[{"type":"strong"}]},{"text":" Contract check modifies program state.","type":"text"}]},{"type":"paragraph","content":[{"text":"Solution:","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":"rust"},"content":[{"text":"// WRONG: Contract has side effect\n#[pre(counter.increment() > 0)] // Modifies counter!\nfn process() { ... }\n\n// RIGHT: Contract is pure\n#[pre(counter.value() > 0)] // Only reads counter\nfn process() { ... }","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Pitfall 2: Expensive Contract Checks","type":"text"}]},{"type":"paragraph","content":[{"text":"Problem:","type":"text","marks":[{"type":"strong"}]},{"text":" Contract check is O(n) or worse, causing performance issues.","type":"text"}]},{"type":"paragraph","content":[{"text":"Solution:","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":"typescript"},"content":[{"text":"// WRONG: O(n) check on every call\nfunction process(items: Item[]) {\n invariant(items.every(i => isValid(i)), \"All items must be valid\");\n // Called millions of times...\n}\n\n// RIGHT: Check once at boundary, trust internally\nfunction publicApi(items: Item[]) {\n const validated = items.filter(isValid); // Validate at boundary\n processInternal(validated); // Internal trusts input\n}","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Pitfall 3: Incomplete Error Context","type":"text"}]},{"type":"paragraph","content":[{"text":"Problem:","type":"text","marks":[{"type":"strong"}]},{"text":" Contract failure message doesn't help debugging.","type":"text"}]},{"type":"paragraph","content":[{"text":"Solution:","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":"python"},"content":[{"text":"# WRONG: No context\nassert x > 0\n\n# RIGHT: Full context\nassert x > 0, f\"Expected positive x, got {x} (type={type(x).__name__}, caller={inspect.stack()[1].function})\"","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Pitfall 4: Contracts Disabled in Production","type":"text"}]},{"type":"paragraph","content":[{"text":"Problem:","type":"text","marks":[{"type":"strong"}]},{"text":" Critical contracts disabled, bugs reach production.","type":"text"}]},{"type":"paragraph","content":[{"text":"Solution:","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":"rust"},"content":[{"text":"// Separate debug-only from critical contracts\n#[cfg(debug_assertions)]\ndebug_assert!(validation_heavy_check()); // Debug only\n\n// Critical contracts always enabled\nassert!(user_id.is_valid(), \"Invalid user ID\"); // Always runs","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Pitfall 5: Circular Contract Dependencies","type":"text"}]},{"type":"paragraph","content":[{"text":"Problem:","type":"text","marks":[{"type":"strong"}]},{"text":" Contract A checks contract B which checks contract A.","type":"text"}]},{"type":"paragraph","content":[{"text":"Solution:","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":"java"},"content":[{"text":"// WRONG: Circular dependency\nclass A {\n @Requires(\"b.isValid()\") // Calls B\n void process(B b) { ... }\n}\nclass B {\n @Requires(\"a.isValid()\") // Calls A, which calls B...\n void validate(A a) { ... }\n}\n\n// RIGHT: Break cycle with primitive checks\nclass A {\n @Requires(\"b.id != null && b.state == State.READY\")\n void process(B b) { ... }\n}","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Contract Strength Guidelines","type":"text"}]},{"type":"paragraph","content":[{"text":"Too Weak (misses bugs)","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":"python"},"content":[{"text":"@icontract.require(lambda x: True) # Useless\ndef divide(x, y):\n return x / y # Will crash on y=0","type":"text"}]},{"type":"paragraph","content":[{"text":"Appropriate Strength","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":"python"},"content":[{"text":"@icontract.require(lambda y: y != 0, \"Divisor must be non-zero\")\[email protected](lambda x, y, result: abs(result * y - x) \u003c 1e-10)\ndef divide(x, y):\n return x / y","type":"text"}]},{"type":"paragraph","content":[{"text":"Too Strong (rejects valid inputs)","type":"text","marks":[{"type":"strong"}]}]},{"type":"code_block","attrs":{"wrap":false,"language":"python"},"content":[{"text":"@icontract.require(lambda x: x > 0 and x \u003c 100) # Overly restrictive\ndef process(x):\n return x * 2 # Works for any number","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Contract Composition Patterns","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Layered Contracts","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":""},"content":[{"text":"Public API Layer: [Strong Preconditions]\n |\nService Layer: [Moderate Preconditions]\n |\nDomain Layer: [Minimal Preconditions + Strong Invariants]\n |\nInfrastructure: [Postconditions on I/O]","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Contract Inheritance","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"java"},"content":[{"text":"// Base contract\ninterface Processor {\n @Requires(\"input != null\")\n @Ensures(\"result != null\")\n Result process(Input input);\n}\n\n// Subtype strengthens postcondition (allowed)\n// Subtype weakens precondition (allowed)\nclass SafeProcessor implements Processor {\n @Requires(\"true\") // Weaker: accepts any input\n @Ensures(\"result != null && result.isValid()\") // Stronger: guarantees validity\n Result process(Input input) { ... }\n}","type":"text"}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Contract Refinement","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"kotlin"},"content":[{"text":"// Start with weak contract, refine as understanding grows\n// Version 1: Basic\nfun process(x: Int): Int {\n require(true) { \"No constraints yet\" }\n // ...\n}\n\n// Version 2: After discovering constraints\nfun process(x: Int): Int {\n require(x > 0) { \"x must be positive\" }\n // ...\n}\n\n// Version 3: After discovering more constraints\nfun process(x: Int): Int {\n require(x in 1..1000) { \"x must be between 1 and 1000\" }\n // ...\n}","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"When NOT to Use Design-by-Contract","type":"text"}]},{"type":"table","attrs":{"layout":null},"content":[{"type":"tr","content":[{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Scenario","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Better Alternative","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Proving mathematical properties","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Proof-driven (Lean 4)","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Compile-time guarantees","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Type-driven (Idris 2)","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Complex state machine correctness","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Validation-first (Quint)","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Performance-critical inner loops","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Disable in release, use types","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Third-party library integration","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Wrapper with contracts at boundary","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Already have strong types","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Contracts may be redundant","type":"text"}]}]}]}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Complementary Approaches","type":"text"}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Contract + Type-driven","type":"text","marks":[{"type":"strong"}]},{"text":": Types encode structure, contracts encode behavior","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Contract + Test-driven","type":"text","marks":[{"type":"strong"}]},{"text":": Contracts as executable specs, tests for coverage","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Contract + Property-based","type":"text","marks":[{"type":"strong"}]},{"text":": Contracts define valid space, property tests explore it","type":"text"}]}]}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Safety Requirements","type":"text"}]},{"type":"ordered_list","attrs":{"order":1,"listStyle":"number"},"content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"No side effects","type":"text","marks":[{"type":"strong"}]},{"text":": Contract checks must not modify state","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Performance","type":"text","marks":[{"type":"strong"}]},{"text":": Disable expensive checks in release builds","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Thread safety","type":"text","marks":[{"type":"strong"}]},{"text":": Contracts must be thread-safe","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Memory safety","type":"text","marks":[{"type":"strong"}]},{"text":": No allocations in hot paths","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Determinism","type":"text","marks":[{"type":"strong"}]},{"text":": Same inputs produce same contract evaluation","type":"text"}]}]}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Best Practices","type":"text"}]},{"type":"ordered_list","attrs":{"order":1,"listStyle":"number"},"content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Boundary validation","type":"text","marks":[{"type":"strong"}]},{"text":": Add preconditions at all public API boundaries","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Critical postconditions","type":"text","marks":[{"type":"strong"}]},{"text":": Use postconditions for guarantees that affect downstream code","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"State invariants","type":"text","marks":[{"type":"strong"}]},{"text":": Add invariants at construction and after state mutations","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Fail fast","type":"text","marks":[{"type":"strong"}]},{"text":": Include clear error messages with context","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Graduated deployment","type":"text","marks":[{"type":"strong"}]},{"text":": Disable expensive contracts in production (when safe)","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Type composition","type":"text","marks":[{"type":"strong"}]},{"text":": Combine contracts with type system for compile-time checks","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Documentation","type":"text","marks":[{"type":"strong"}]},{"text":": Document contract rationale in comments","type":"text"}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Testing","type":"text","marks":[{"type":"strong"}]},{"text":": Test contract violations explicitly in unit tests","type":"text"}]}]}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Performance Considerations","type":"text"}]},{"type":"table","attrs":{"layout":null},"content":[{"type":"tr","content":[{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Aspect","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Development","type":"text"}]}]},{"type":"th","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Production","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Preconditions","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Always enabled","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Critical only","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Postconditions","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Always enabled","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Disabled","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Invariants","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Full checking","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Disabled","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Logging","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Verbose","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Minimal","type":"text"}]}]}]},{"type":"tr","content":[{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"Cost per check","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"O(1) acceptable","type":"text"}]}]},{"type":"td","attrs":{"colspan":1,"rowspan":1,"colwidth":null,"alignment":""},"content":[{"type":"paragraph","content":[{"text":"O(1) required","type":"text"}]}]}]}]},{"type":"heading","attrs":{"level":3},"content":[{"text":"Optimization Strategies","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"rust"},"content":[{"text":"// Conditional compilation\n#[cfg(debug_assertions)]\nfn expensive_check() { ... }\n\n// Feature flags\n#[cfg(feature = \"contracts\")]\nfn contract_check() { ... }\n\n// Inline for hot paths\n#[inline(always)]\nfn fast_precondition() { ... }","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Integration Workflow","type":"text"}]},{"type":"code_block","attrs":{"wrap":false,"language":"nomnoml"},"content":[{"text":"[\u003cstart>Start] -> [dbc-detect]\n[dbc-detect] found contracts -> [dbc-verify]\n[dbc-detect] no contracts -> [dbc-remediate --add-missing]\n[dbc-verify] pass -> [\u003cend>Success]\n[dbc-verify] fail -> [dbc-remediate --fix-violations]\n[dbc-remediate --add-missing] -> [dbc-verify]\n[dbc-remediate --fix-violations] -> [dbc-verify]","type":"text"}]},{"type":"hr","attrs":{"markup":"---"}},{"type":"heading","attrs":{"level":2},"content":[{"text":"Resources","type":"text"}]},{"type":"bullet_list","content":[{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Design by Contract (Meyer)","type":"text","marks":[{"type":"link","attrs":{"href":"https://en.wikipedia.org/wiki/Design_by_contract","title":null}}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Eiffel: Birthplace of DbC","type":"text","marks":[{"type":"link","attrs":{"href":"https://www.eiffel.com/values/design-by-contract/","title":null}}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Microsoft Code Contracts","type":"text","marks":[{"type":"link","attrs":{"href":"https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts","title":null}}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Rust contracts crate","type":"text","marks":[{"type":"link","attrs":{"href":"https://crates.io/crates/contracts","title":null}}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"Python icontract","type":"text","marks":[{"type":"link","attrs":{"href":"https://github.com/Parquery/icontract","title":null}}]}]}]},{"type":"list_item","content":[{"type":"paragraph","content":[{"text":"TypeScript zod","type":"text","marks":[{"type":"link","attrs":{"href":"https://github.com/colinhacks/zod","title":null}}]}]}]}]},{"type":"hr","attrs":{"markup":"---"}}]},"metadata":{"date":"2026-06-05","name":"design-by-contract","author":"@skillopedia","source":{"stars":231,"repo_name":"ordinary-claude-skills","origin_url":"https://github.com/microck/ordinary-claude-skills/blob/HEAD/skills_all/design-by-contract/SKILL.md","repo_owner":"microck","body_sha256":"6bd1830f11fc052bf2c3f83087d8edd412b79796608392099f0c97ea44236f2e","cluster_key":"825ebd19fc2d6ae619bc55c1bef48b84df0eea43248c050e7fa3f470e8217147","clean_bundle":{"format":"clean-skill-bundle-v1","source":"microck/ordinary-claude-skills/skills_all/design-by-contract/SKILL.md","attachments":[{"id":"1bf52d22-be10-5eef-8971-d5c541bbaad8","key":"uploads/10433ee7-ad12-4ae0-b34e-97553e46c6c8/1bf52d22-be10-5eef-8971-d5c541bbaad8/attachment.json","path":"metadata.json","size":749,"sha256":"fc63222abb88feb6ce4f49f78960ea778d4372e8799db4241e8669255a8ac3a7","contentType":"application/json; charset=utf-8"}],"bundle_sha256":"7e02f280bc1f58426340cd14a1ed35a98844f514003819965202de61ef0912bb","attachment_count":1,"text_attachments":1,"attachment_storage":"skillopedia-attachments-v1","binary_attachments":0,"excluded_attachments":[]},"cluster_size":4,"skill_md_path":"skills_all/design-by-contract/SKILL.md","import_metadata":{"date":"2026-06-05","author":"@skillopedia","version":"v1","category":"documents-office","category_label":"Documents"},"exact_dupes_collapsed_into_this":3},"version":"v1","category":"documents-office","import_tag":"clean-skills-v1","description":"Automated contract verification, detection, and remediation across multiple languages using formal preconditions, postconditions, and invariants. This skill provides both reference documentation AND execution capabilities for the full PLAN -> CREATE -> VERIFY -> REMEDIATE workflow."}},"renderedAt":1782981078039}

Important: agents should read /llm.txt, /llms.txt, or /.well-known/skills.json to discover the public Skillopedia API.