design-by-contract

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

[<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 bounds | const_assert!, static_assert | - | - | - | | Null/type safety | Type checker (tsc/pyright/kotlinc) | - | - | - | | Exhaustiveness | Pattern matching + never/Never | - | - | - | | Expensive O(n)+ checks | - | test_ensures | - | - | | Reference impl equivalence | - | test_ensures | - | - | | Internal state invariants | - | - | debug_invariant | - | | Development preconditions | - | - | debug_requires | - | | Public API input validation | - | - | - | requires | | Safety-critical postconditions | - | - | - | ensures | | External/untrusted data | - | - | - | Required (Zod/icontract) |

Legend: - = Do not use for this property

Decision Flow

Can type system encode it? ──yes──> Use types (typestate, newtype)
         │no
         v
Verifiable at compile-time? ──yes──> static_assertions / const_assert!
         │no
         v
Expensive O(n)+ check? ──yes──> test_* (test builds only)
         │no
         v
Internal development aid? ──yes──> debug_* (debug builds only)
         │no
         v
Must enforce in production? ──yes──> Runtime contracts
         │no
         v
Consider if check is needed at all

Phase 1: PLAN (Contract Design)

Process

1. Understand Requirements
2. Parse user's task/requirement
3. Identify preconditions, postconditions, invariants
4. Use sequential-thinking to decompose contract obligations
5. Map requirements to contract types

1. Artifact Detection (Conditional)
2. Check for existing contract artifacts by language:

``bash # Rust (contracts crate) rg '#\[pre\(|#\[post\(|#\[invariant\(' $ARGUMENTS # TypeScript (Zod) rg 'z\.object|z\.string|\.refine\(' $ARGUMENTS # Python (icontract) rg '@pre\(|@post\(|@invariant\(' $ARGUMENTS # Java/Kotlin rg 'checkArgument|checkState|require\s*\{' $ARGUMENTS ``

• If artifacts exist: analyze coverage gaps, plan extensions
• If no artifacts: proceed to design contract architecture

1. Design Contract Architecture
2. Design precondition predicates
3. Plan postcondition guarantees
4. Define class/module invariants
5. Output: Contract design with annotation signatures

1. Prepare Run Phase
2. Define target: .outline/contracts/
3. Specify verification: language-specific contract checking
4. Create traceability: requirement -> contract -> enforcement

Thinking Tool Integration

Use sequential-thinking for:
- Contract decomposition
- Obligation ordering
- Inheritance chain planning

Use actor-critic-thinking for:
- Contract strength evaluation
- Precondition completeness
- Postcondition sufficiency

Use shannon-thinking for:
- Contract coverage gaps
- Runtime verification costs
- Weakest precondition analysis

Contract Design Templates

Rust (contracts crate)

// Target: .outline/contracts/{module}_contracts.rs

// From requirement: {requirement text}
#[pre(input > 0, "Input must be positive")]
#[post(ret.is_some() => ret.unwrap() > input)]
fn process(input: i32) -> Option<i32> {
    // Implementation in run phase
}

// Class invariant
#[invariant(self.balance >= 0)]
impl Account {
    // Methods maintain invariant
}

TypeScript (Zod)

// Target: .outline/contracts/{module}.contracts.ts

// From requirement: {requirement text}
const InputSchema = z.object({
  value: z.number().positive("Value must be positive"),
}).refine(
  (data) => /* precondition */,
  { message: "Precondition: {description}" }
);

// Postcondition validator
const OutputSchema = z.object({
  result: z.number(),
}).refine(
  (data) => /* postcondition */,
  { message: "Postcondition: {description}" }
);

Python (icontract)

# Target: .outline/contracts/{module}_contracts.py

# From requirement: {requirement text}
@icontract.require(lambda x: x > 0, "Input must be positive")
@icontract.ensure(lambda result: result is not None)
def process(x: int) -> Optional[int]:
    # Implementation in run phase
    pass

Plan Output

1. Requirements Analysis
2. Preconditions identified
3. Postconditions guaranteed
4. Invariants to maintain

1. Contract Architecture
2. Contract signatures per function/method
3. Invariant definitions per class/module
4. Inheritance contract chains

1. Target Artifacts
2. .outline/contracts/* file list
3. Contract library dependencies
4. Runtime flag configuration

1. Verification Commands
2. Build with contracts enabled
3. Test suite exercising contracts
4. Success criteria: no contract violations

Phase 2: CREATE (Generate Artifacts)

Setup

# Create .outline/contracts directory
mkdir -p .outline/contracts

Generate Contract Files by Language

Rust (contracts crate)

// .outline/contracts/{module}_contracts.rs
// Generated from plan design

use contracts::*;

// Source Requirement: {traceability from plan}

// Precondition: {from plan design}
// Postcondition: {from plan design}
#[pre(input > 0, "Input must be positive")]
#[post(ret.is_some() => ret.unwrap() > input, "Output must exceed input")]
pub fn process(input: i32) -> Option<i32> {
    // Implementation
    Some(input + 1)
}

// Class invariant: {from plan design}
#[invariant(self.balance >= 0, "Balance must be non-negative")]
impl Account {
    #[post(self.balance == old(self.balance) + amount)]
    pub fn deposit(&mut self, amount: u64) {
        self.balance += amount;
    }
}

TypeScript (Zod)

// .outline/contracts/{module}.contracts.ts
// Generated from plan design

import { z } from 'zod';

// Source Requirement: {traceability from plan}

// Precondition schema: {from plan design}
export const In