design-by-contract

---
name: design-by-contract
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.
---

# 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)
- **Postconditions**: What must be true after a function executes (callee's promise)
- **Invariants**: What must always be true about object state

---

## When to Use

Design-by-Contract is ideal for:

- **Public API boundaries**: Validate inputs at module boundaries
- **Critical business logic**: Ensure computation correctness
- **State management**: Maintain object consistency
- **Integration points**: Verify data crossing system boundaries
- **Team collaboration**: Document expected behavior formally

---

## Workflow Overview

```nomnoml
[<start>Requirements] -> [Phase 1: PLAN]
[Phase 1: PLAN|
  Identify contracts
  Design predicates
  Map obligations
] -> [Phase 2: CREATE]
[Phase 2: CREATE|
  Generate annotations
  Add to .outline/contracts/
  Wire dependencies
] -> [Phase 3: VERIFY]
[Phase 3: VERIFY|
  Enable runtime flags
  Run test suite
  Check violations
] -> [Phase 4: REMEDIATE]
[Phase 4: REMEDIATE|
  Diagnose violation type
  Fix caller/callee/state
  Re-verify
] -> [<end>Success]
```

---

## Verification Hierarchy

**Principle**: Use compile-time verification before runtime contracts. If a property can be verified statically, do NOT add a runtime contract for it.

```
Static Assertions (compile-time) > Test/Debug Contracts > Runtime Contracts
```

### When to Use Each Level

| Property | Static | Test Contract | Debug Contract | Runtime Contract |
|----------|--------|---------------|----------------|------------------|
| Type size/alignment | `static_assert` (C++), `assert_eq_size!` (Rust) | - | - | - |
| Trait/interface bounds | `assert_impl_all!` (Rust), Concepts (C++) | - | - | - |
| Const value bou

预览已截断。下载完整技能包可查看全部文件内容。