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

   • Parse user's task/requirement
   • Identify preconditions, postconditions, invariants
   • Use sequential-thinking to decompose contract obligations
   • Map requirements to contract types

2. Artifact Detection (Conditional)

   • Check for existing contract artifacts by language:

     # 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

3. Design Contract Architecture

   • Design precondition predicates
   • Plan postcondition guarantees
   • Define class/module invariants
   • Output: Contract design with annotation signatures

4. Prepare Run Phase

   • Define target: .outline/contracts/
   • Specify verification: language-specific contract checking
   • 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

   • Preconditions identified
   • Postconditions guaranteed
   • Invariants to maintain

2. Contract Architecture

   • Contract signatures per function/method
   • Invariant definitions per class/module
   • Inheritance contract chains

3. Target Artifacts

   • .outline/contracts/* file list
   • Contract library dependencies
   • Runtime flag configuration

4. Verification Commands

   • Build with contracts enabled
   • Test suite exercising contracts
   • 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 InputSchema = z.object({
  value: z.number().positive("Value must be positive"),
  name: z.string().min(1, "Name required"),
}).refine(
  (data) => data.value < 1000,
  { message: "Precondition: value must be under 1000" }
);

// Postcondition schema: {from plan design}
export const OutputSchema = z.object({
  result: z.number(),
  success: z.boolean(),
}).refine(
  (data) => data.success || data.result === 0,
  { message: "Postcondition: failed operations must return 0" }
);

// Validation wrapper
export function withContracts<I, O>(
  inputSchema: z.ZodType<I>,
  outputSchema: z.ZodType<O>,
  fn: (input: I) => O
): (input: I) => O {
  return (input: I) => {
    const validInput = inputSchema.parse(input);
    const output = fn(validInput);
    return outputSchema.parse(output);
  };
}

Python (icontract)

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

import icontract

# Source Requirement: {traceability from plan}

# Precondition: {from plan design}
# Postcondition: {from plan design}
@icontract.require(lambda x: x > 0, "Input must be positive")
@icontract.ensure(lambda result: result is not None, "Must return value")
@icontract.ensure(lambda x, result: result > x, "Output must exceed input")
def process(x: int) -> int:
    return x + 1


# Class invariant: {from plan design}
@icontract.invariant(lambda self: self.balance >= 0)
class Account:
    def __init__(self):
        self.balance = 0

    @icontract.require(lambda amount: amount > 0)
    @icontract.ensure(lambda self, amount, OLD: self.balance == OLD.balance + amount)
    def deposit(self, amount: int) -> None:
        self.balance += amount

---

Phase 3: VERIFY (Contract Validation)

Rust

# Ensure contracts are enabled (not disabled)
unset CONTRACTS_DISABLE

# Verify contracts exist
rg '#\[pre\(|#\[post\(|#\[invariant\(' .outline/contracts/ || exit 12

# Run tests with contracts
cargo test || exit 13

TypeScript

# Verify Zod schemas exist
rg 'z\.object|\.refine\(' .outline/contracts/ || exit 12

# Run tests (Zod validates at runtime)
npx vitest run || exit 13

Python

# Enable thorough contract checking
export ICONTRACT_SLOW=true

# Verify decorators exist
rg '@icontract\.(require|ensure|invariant)' .outline/contracts/ || exit 12

# Run tests
pytest || exit 13

Java (Guava)

# Verify Guava preconditions exist
rg 'checkArgument|checkState|checkNotNull' .outline/contracts/ || exit 12

# Run tests
mvn test || exit 13

C++ (GSL/Boost)

# Ensure NDEBUG is NOT set for contract checking
unset NDEBUG

# Verify contracts exist
rg 'Expects\(|Ensures\(' .outline/contracts/ || exit 12

# Build and test
cmake --build build && ./build/tests || exit 13

---

Phase 4: REMEDIATE (Fix Violations)

Contract Violation Types

Violation	Exit Code	Fix Strategy
Precondition	1	Fix caller to meet requirements
Postcondition	2	Fix implementation to meet guarantee
Invariant	3	Fix state management logic

Debugging by Violation Type

Precondition Violation (Caller's fault)

# Error: icontract.ViolationError: Pre: x > 0
# The CALLER passed invalid input

# Debug: Check call site
# Before:
result = process(-5)  # WRONG: violates x > 0

# After:
if x > 0:
    result = process(x)
else:
    handle_invalid_input(x)

Postcondition Violation (Callee's fault)

# Error: icontract.ViolationError: Post: result > x
# The IMPLEMENTATION doesn't meet its guarantee

# Debug: Fix the function
# Before:
@icontract.ensure(lambda x, result: result > x)
def process(x: int) -> int:
    return x  # WRONG: not > x

# After:
@icontract.ensure(lambda x, result: result > x)
def process(x: int) -> int:
    return x + 1  # Correct

Invariant Violation (State corruption)

# Error: icontract.ViolationError: Inv: self.balance >= 0
# Object state became invalid after operation

# Debug: Find state mutation that breaks invariant
# Before:
@icontract.invariant(lambda self: self.balance >= 0)
class Account:
    def withdraw(self, amount):
        self.balance -= amount  # WRONG: can go negative

# After:
    @icontract.require(lambda self, amount: amount <= self.balance)
    def withdraw(self, amount):
        self.balance -= amount  # Now protected by precondition

Contract Patterns

Precondition (Caller's Duty)

INPUT --> VALIDATE --> PROCESS
            |
            v
         FAIL FAST if invalid

Postcondition (Callee's Promise)

PROCESS --> OUTPUT --> VALIDATE
                          |
                          v
                       ASSERT guarantee met

Invariant (Always True)

OPERATION --> STATE CHANGE --> CHECK INVARIANT
                                  |
                                  v
                               ASSERT still valid

---

Commands Reference

dbc-verify

Verify all contracts satisfied in codebase.

Usage: dbc-verify [--lang LANG] [--path PATH] [--runtime-flags]

Algorithm:

1. Detect language(s) in scope (fd file extensions)
2. Check runtime flags enabled per language
3. Scan for contract library usage (rg patterns)
4. Execute language-specific verification
5. Report violations with exit codes

dbc-detect

Detect contract usage and missing contracts.

Usage: dbc-detect [--lang LANG] [--missing] [--violations]

Algorithm:

1. Scan for contract library imports (rg)
2. Find functions without contracts (ast-grep negative match)
3. Identify contract violations (pattern analysis)
4. Generate coverage report

dbc-remediate

Auto-fix violations or add missing contracts.

Usage: dbc-remediate [--add-missing] [--fix-violations] [--dry-run]

Algorithm:

1. Identify remediation targets (missing/violated contracts)
2. Generate contract code per language
3. Apply fixes via ast-grep or native-patch
4. Verify fixes with dbc-verify

---

Exit Codes

Code	Meaning	Action
0	All contracts pass	Ready for deployment
1	Precondition fail	Fix caller to meet requirements
2	Postcondition fail	Fix implementation
3	Invariant fail	Fix state management
11	Library missing	Install contract library
12	No contracts	Run plan phase, create contracts
13	Verification failed	Debug and fix violations

---

Language-Specific Implementations

Rust Detection

# Find contracts
rg '#\[pre\(|#\[post\(|#\[invariant\(|debug_assert!' --type rust

# Find functions without contracts
ast-grep -p 'fn $NAME($$$) { $$$ }' -l rust | \
  rg -v '#\[pre\(|debug_assert!' --files-without-match

Remediation template:

#[pre($CONDITION)]
#[post(ret $POSTCONDITION)]
fn $NAME($PARAMS) -> $RET {
    debug_assert!($CONDITION, "$ERROR_MSG");
    $BODY
}

Runtime flags: Check CARGO_BUILD_TYPE != release or cfg(debug_assertions)

TypeScript Detection

# Find contracts
rg 'z\.object|invariant\(|\.parse\(|\.safeParse\(' --type ts

# Find functions without validation
ast-grep -p 'function $NAME($$$): $$$ { $$$ }' -l typescript | \
  rg -v 'z\.|invariant' --files-without-match

Remediation template:

const ${NAME}Schema = z.object({
  $FIELDS
});

function $NAME(params: unknown): $RET {
  const validated = ${NAME}Schema.parse(params);
  invariant($CONDITION, "$ERROR_MSG");
  $BODY
}

Runtime flags: Check process.env.NODE_ENV === 'development'

Python Detection

# Find contracts
rg '@pre\(|@post\(|@invariant|@require|@ensure' --type python

# Find functions without contracts
ast-grep -p 'def $NAME($$$): $$$' -l python | \
  rg -v '@pre|@post|@invariant' --files-without-match

Remediation template:

@pre(lambda $PARAMS: $CONDITION)
@post(lambda result: $POSTCONDITION)
def $NAME($PARAMS) -> $RET:
    """$DOCSTRING"""
    $BODY

Runtime flags: Check __debug__ is True (not python -O)

Java Detection

# Find contracts
rg 'checkArgument|checkState|validate\(|Preconditions\.' --type java

# Find methods without contracts
ast-grep -p 'public $RET $NAME($$$) { $$$ }' -l java | \
  rg -v 'checkArgument|validate' --files-without-match

Remediation template:

public $RET $NAME($PARAMS) {
    checkArgument($CONDITION, "$ERROR_MSG");
    $BODY
    validate($POSTCONDITION, "$POST_ERROR");
    return $RESULT;
}

Runtime flags: Check assertions enabled with -ea flag

Kotlin Detection

# Find contracts
rg 'contract \{|Either<|Validated|require\(|check\(' --type kotlin

# Find functions without contracts
ast-grep -p 'fun $NAME($$$): $$$ { $$$ }' -l kotlin | \
  rg -v 'contract|require|check' --files-without-match

Remediation template:

fun $NAME($PARAMS): Either<$ERR, $RET> {
    contract {
        returns() implies ($CONDITION)
    }
    return if (!$CONDITION) "$ERROR".left()
           else { $BODY }.right()
}

Runtime flags: Check -ea for JVM assertions

C# Detection

# Find contracts
rg 'Guard\.Against|Contract\.Requires|Contract\.Ensures|Debug\.Assert' --type cs

# Find methods without contracts
ast-grep -p 'public $RET $NAME($$$) { $$$ }' -l csharp | \
  rg -v 'Guard\.|Contract\.' --files-without-match

Remediation template:

public $RET $NAME($PARAMS) {
    Guard.Against.Null($PARAM, nameof($PARAM));
    Contract.Ensures(Contract.Result<$RET>() $POSTCONDITION);
    $BODY
}

Runtime flags: Check Debug configuration

C++ Detection

# Find contracts
rg 'Expects\(|Ensures\(|boost::contract|gsl::' --type cpp

# Find functions without contracts
ast-grep -p '$RET $NAME($$$) { $$$ }' -l cpp | \
  rg -v 'Expects|Ensures' --files-without-match

Remediation template:

$RET $NAME($PARAMS) {
    Expects($PRECONDITION);
    $BODY
    Ensures($POSTCONDITION);
    return $RESULT;
}

Runtime flags: Check NDEBUG not defined

C Detection

# Find contracts
rg 'assert\(|static_assert' --type c

# Find functions without asserts
ast-grep -p '$RET $NAME($$$) { $$$ }' -l c | \
  rg -v 'assert\(' --files-without-match

Remediation template:

$RET $NAME($PARAMS) {
    assert($PRECONDITION && "$ERROR_MSG");
    $BODY
    assert($POSTCONDITION && "$POST_ERROR");
    return $RESULT;
}

Runtime flags: Check NDEBUG not defined

---

Contract Library Matrix

Language	Library	Runtime Flag
Rust	contracts	CONTRACTS_DISABLE
TypeScript	Zod	(always active)
Python	icontract	ICONTRACT_SLOW
Java	Guava	(always active)
Kotlin	native	(always active)
C#	Guard	(always active)
C++	GSL/Boost	NDEBUG

---

Error Handling Matrix

Language	Contract Library	Error Type	Error Handling	Recovery Strategy
Rust	contracts, prusti	panic!	catch_unwind (discouraged)	Result/Option types
TypeScript	zod, io-ts	ZodError, thrown	try/catch	Either/Result pattern
Python	dpcontracts, icontract	AssertionError	try/except	Optional/Result
Java	Guava, Bean Validation	IllegalArgumentException	try/catch	Optional/Either
Kotlin	Arrow, require/check	IllegalArgumentException	try/catch	Either<E, A>
C#	Code Contracts, Guard	ArgumentException	try/catch	Result
C++	GSL, Boost.Contract	std::terminate	noexcept	std::expected
C	assert.h	abort()	Signal handler	Return codes

Error Message Best Practices

Contract Type: [PRECONDITION|POSTCONDITION|INVARIANT]
Location: file.rs:42 in function_name()
Condition: x > 0 && x < 100
Actual Value: x = -5
Expected: Positive integer less than 100
Context: Processing user input for order ID

---

Troubleshooting Guide

Common Issues

Symptom	Cause	Resolution
Exit 1	Precondition violation	Caller must provide valid input (fix call site)
Exit 2	Postcondition violation	Implementation doesn't meet guarantee (fix function)
Exit 3	Invariant violation	Object state became invalid (fix state mutation)
Exit 11	Contract library missing	Install: pip install icontract, cargo add contracts, npm i zod
Exit 12	No contract annotations	Run plan phase first
Exit 13	Tests failed with contracts	Debug violation type
CONTRACTS_DISABLE set	Contracts silently skipped	unset CONTRACTS_DISABLE
No error but wrong behavior	Contract too weak	Strengthen pre/post conditions
Performance impact	Contracts in hot path	Use @icontract.require(enabled=DEBUG)
Contract not firing	Debug assertions disabled	Check NDEBUG, -O flags
False positive	Contract too strict	Review expected vs actual
False negative	Contract too weak	Add edge case tests
Stack overflow	Recursive contract	Check for cycles
Flaky failures	Race condition in contract	Add synchronization

Quick Diagnostics

# Check if contracts are enabled (Rust)
cargo build && rg 'debug_assert' target/debug/*.d

# Check if contracts are enabled (Node.js)
node -e "console.log(process.env.NODE_ENV)"

# Check if assertions enabled (Java)
java -ea -version 2>&1 | head -1

# Check if assertions enabled (C/C++)
cpp -dM /dev/null | grep NDEBUG

Debugging Commands

# Python - Verbose contract errors
ICONTRACT_SLOW=true pytest -v --tb=long

# Python - Find contract decorators
rg '@icontract\.(require|ensure|invariant)' src/

# Rust - Enable backtrace
RUST_BACKTRACE=1 cargo test

# Rust - Find contract attributes
rg '#\[(pre|post|invariant)\(' src/

# TypeScript - Verbose Zod errors
DEBUG=zod:* npm test

# TypeScript - Find Zod schemas
rg 'z\.(object|refine|string|number)' src/

# General - Check contracts not disabled
env | rg -i 'contract|ndebug'

Debugging Contract Violation Workflows

Precondition Violation Debugging

1. Identify the violation location:

   # Run with debug symbols
   RUST_BACKTRACE=1 cargo run   # Rust
   node --enable-source-maps    # Node.js
   python -c "import traceback" # Python
   

2. Examine the call stack:

   • Find the caller that provided invalid input
   • Check intermediate transformations that corrupted data

3. Add tracing at contract boundary:

   // Rust example
   #[pre(x > 0)]
   fn process(x: i32) {
       tracing::debug!("process called with x = {}", x);
       // ...
   }
   

4. Common causes:

   • Unvalidated user input
   • Null/None propagation
   • Integer overflow in computation
   • Incorrect API usage

Postcondition Violation Debugging

1. Instrument the function exit:

   // TypeScript example
   function calculate(x: number): number {
     const result = /* computation */;
     console.log(`calculate returning: ${result}`);
     invariant(result > 0, `Expected positive, got ${result}`);
     return result;
   }
   

2. Check intermediate state:

   • Add assertions at each computation step
   • Verify loop invariants maintained

3. Common causes:

   • Logic error in computation
   • Incorrect formula
   • Edge case not handled
   • Floating point precision loss

Invariant Violation Debugging

1. Track state transitions:

   # Python example with dpcontracts
   @invariant(lambda self: self.balance >= 0)
   class Account:
       def __init__(self):
           self._log_state("init")
   
       def withdraw(self, amount):
           self._log_state(f"before withdraw {amount}")
           self.balance -= amount
           self._log_state(f"after withdraw {amount}")
   

2. Find mutation that breaks invariant:

   • Identify all state-mutating methods
   • Check each mutation point