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

static_assert

assert_eq_size!

assert_impl_all!

const_assert!

static_assert

never

Never

test_ensures

test_ensures

debug_invariant

debug_requires

requires

ensures

Legend:

-

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

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

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

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__

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

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

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

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

Contract Library Matrix

Error Handling Matrix

catch_unwind

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

pip install icontract

cargo add contracts

npm i zod

CONTRACTS_DISABLE

unset CONTRACTS_DISABLE

@icontract.require(enabled=DEBUG)

NDEBUG

-O

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

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

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