---

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

[<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

3. Common causes:

   • Missing validation in setter
   • Concurrent modification
   • Deserialization bypassing constructor

---

Common Pitfalls and Solutions

Pitfall 1: Contracts with Side Effects

Problem: Contract check modifies program state.

Solution:

// WRONG: Contract has side effect
#[pre(counter.increment() > 0)]  // Modifies counter!
fn process() { ... }

// RIGHT: Contract is pure
#[pre(counter.value() > 0)]  // Only reads counter
fn process() { ... }

Pitfall 2: Expensive Contract Checks

Problem: Contract check is O(n) or worse, causing performance issues.

Solution:

// WRONG: O(n) check on every call
function process(items: Item[]) {
  invariant(items.every(i => isValid(i)), "All items must be valid");
  // Called millions of times...
}

// RIGHT: Check once at boundary, trust internally
function publicApi(items: Item[]) {
  const validated = items.filter(isValid);  // Validate at boundary
  processInternal(validated);  // Internal trusts input
}

Pitfall 3: Incomplete Error Context

Problem: Contract failure message doesn't help debugging.

Solution:

# WRONG: No context
assert x > 0

# RIGHT: Full context
assert x > 0, f"Expected positive x, got {x} (type={type(x).__name__}, caller={inspect.stack()[1].function})"

Pitfall 4: Contracts Disabled in Production

Problem: Critical contracts disabled, bugs reach production.

Solution:

// Separate debug-only from critical contracts
#[cfg(debug_assertions)]
debug_assert!(validation_heavy_check());  // Debug only

// Critical contracts always enabled
assert!(user_id.is_valid(), "Invalid user ID");  // Always runs

Pitfall 5: Circular Contract Dependencies

Problem: Contract A checks contract B which checks contract A.

Solution:

// WRONG: Circular dependency
class A {
    @Requires("b.isValid()")  // Calls B
    void process(B b) { ... }
}
class B {
    @Requires("a.isValid()")  // Calls A, which calls B...
    void validate(A a) { ... }
}

// RIGHT: Break cycle with primitive checks
class A {
    @Requires("b.id != null && b.state == State.READY")
    void process(B b) { ... }
}

---

Contract Strength Guidelines

Too Weak (misses bugs)

@icontract.require(lambda x: True)  # Useless
def divide(x, y):
    return x / y  # Will crash on y=0

Appropriate Strength

@icontract.require(lambda y: y != 0, "Divisor must be non-zero")
@icontract.ensure(lambda x, y, result: abs(result * y - x) < 1e-10)
def divide(x, y):
    return x / y

Too Strong (rejects valid inputs)

@icontract.require(lambda x: x > 0 and x < 100)  # Overly restrictive
def process(x):
    return x * 2  # Works for any number

---

Contract Composition Patterns

Layered Contracts

Public API Layer:    [Strong Preconditions]
                            |
Service Layer:       [Moderate Preconditions]
                            |
Domain Layer:        [Minimal Preconditions + Strong Invariants]
                            |
Infrastructure:      [Postconditions on I/O]

Contract Inheritance

// Base contract
interface Processor {
    @Requires("input != null")
    @Ensures("result != null")
    Result process(Input input);
}

// Subtype strengthens postcondition (allowed)
// Subtype weakens precondition (allowed)
class SafeProcessor implements Processor {
    @Requires("true")  // Weaker: accepts any input
    @Ensures("result != null && result.isValid()")  // Stronger: guarantees validity
    Result process(Input input) { ... }
}

Contract Refinement

// Start with weak contract, refine as understanding grows
// Version 1: Basic
fun process(x: Int): Int {
    require(true) { "No constraints yet" }
    // ...
}

// Version 2: After discovering constraints
fun process(x: Int): Int {
    require(x > 0) { "x must be positive" }
    // ...
}

// Version 3: After discovering more constraints
fun process(x: Int): Int {
    require(x in 1..1000) { "x must be between 1 and 1000" }
    // ...
}

---

When NOT to Use Design-by-Contract

Scenario	Better Alternative
Proving mathematical properties	Proof-driven (Lean 4)
Compile-time guarantees	Type-driven (Idris 2)
Complex state machine correctness	Validation-first (Quint)
Performance-critical inner loops	Disable in release, use types
Third-party library integration	Wrapper with contracts at boundary
Already have strong types	Contracts may be redundant

---

Complementary Approaches

• Contract + Type-driven: Types encode structure, contracts encode behavior
• Contract + Test-driven: Contracts as executable specs, tests for coverage
• Contract + Property-based: Contracts define valid space, property tests explore it

---

Safety Requirements

1. No side effects: Contract checks must not modify state
2. Performance: Disable expensive checks in release builds
3. Thread safety: Contracts must be thread-safe
4. Memory safety: No allocations in hot paths
5. Determinism: Same inputs produce same contract evaluation

---

Best Practices

1. Boundary validation: Add preconditions at all public API boundaries
2. Critical postconditions: Use postconditions for guarantees that affect downstream code
3. State invariants: Add invariants at construction and after state mutations
4. Fail fast: Include clear error messages with context
5. Graduated deployment: Disable expensive contracts in production (when safe)
6. Type composition: Combine contracts with type system for compile-time checks
7. Documentation: Document contract rationale in comments
8. Testing: Test contract violations explicitly in unit tests

---

Performance Considerations

Aspect	Development	Production
Preconditions	Always enabled	Critical only
Postconditions	Always enabled	Disabled
Invariants	Full checking	Disabled
Logging	Verbose	Minimal
Cost per check	O(1) acceptable	O(1) required

Optimization Strategies

// Conditional compilation
#[cfg(debug_assertions)]
fn expensive_check() { ... }

// Feature flags
#[cfg(feature = "contracts")]
fn contract_check() { ... }

// Inline for hot paths
#[inline(always)]
fn fast_precondition() { ... }

---

Integration Workflow

[<start>Start] -> [dbc-detect]
[dbc-detect] found contracts -> [dbc-verify]
[dbc-detect] no contracts -> [dbc-remediate --add-missing]
[dbc-verify] pass -> [<end>Success]
[dbc-verify] fail -> [dbc-remediate --fix-violations]
[dbc-remediate --add-missing] -> [dbc-verify]
[dbc-remediate --fix-violations] -> [dbc-verify]

---

Resources

• Design by Contract (Meyer)
• Eiffel: Birthplace of DbC
• Microsoft Code Contracts
• Rust contracts crate
• Python icontract
• TypeScript zod