DESIGN BY CONTRACT

How Design by Contract Works

The code tells you what it guarantees. The runtime enforces those guarantees. Automatically.

The Core Idea

Every feature (method) is a contract between caller and implementation:

PRECONDITIONS (`require`)

What must be true before the feature runs

"I require these conditions to do my job."

POSTCONDITIONS (`ensure`)

What will be true after the feature runs

"I guarantee these results when I'm done."

INVARIANTS (`invariant`)

What's always true about an object

"This is always true about me, before and after every call."

A Real Example

Let's build a bank account:


class BANK_ACCOUNT

feature -- Access

    balance: DECIMAL
        -- Current account balance

feature -- Operations

    withdraw (amount: DECIMAL)
        -- Withdraw amount from account
        require
            positive_amount: amount > 0
            sufficient_funds: amount <= balance
        do
            balance := balance - amount
        ensure
            balance_reduced: balance = old balance - amount
        end

invariant
    non_negative_balance: balance >= 0

end

Create: account.balance := 100.00
Call: account.withdraw(30.00)
Check: amount > 0 → 30 > 0 ✓
Check: amount <= balance → 30 <= 100 ✓
Execute: balance := 100 - 30
Verify: balance = old balance - amount → 70 = 100 - 30 ✓
Invariant: balance >= 0 → 70 >= 0 ✓
Call: account.withdraw(100.00)
Check: amount > 0 → 100 > 0 ✓
⚠ PRECONDITION VIOLATION: sufficient_funds
100 > 70 (current balance) — overdraft prevented!
Call: account.withdraw(-50.00)
⚠ PRECONDITION VIOLATION: positive_amount
-50 is not > 0 — deposit disguised as withdrawal blocked!


Click Step to explore the bank account contracts
A simple bank account class
The balance attribute stores current funds
Preconditions: amount must be positive AND within available balance
The actual work — subtract amount from balance
Postcondition: balance is exactly reduced by the amount
Invariant: balance can NEVER go negative — checked after every call
Let's create an account with $100...
Valid withdrawal: all contracts satisfied!
Overdraft attempt? Blocked by precondition!
Sneaky negative withdrawal? Also blocked!

What this guarantees:

You can't withdraw zero or negative amounts
You can't withdraw more than you have
After withdrawal, balance is exactly what you expect
Balance can never go negative, ever

Try to violate any of these? Runtime exception with exact location.

What Happens When AI Writes Code

Without Contracts

• AI writes withdraw function
• Maybe it checks for sufficient funds, maybe not
• Maybe there's a bug in the calculation
• You find out in production. Or you don't.

With Contracts

• AI writes withdraw function with contracts
• First test run: "POSTCONDITION VIOLATION: balance_reduced"
• Bug found instantly. Exact location. Exact expectation.
• AI fixes it. Contracts pass. Ship with confidence.

The contracts are the specification. The runtime is the verifier. AI mistakes don't reach production.

Types of Contracts

Preconditions (require)

Guard inputs before execution. The caller's responsibility.

require
    positive_amount: amount > 0
    sufficient_funds: amount <= balance

Postconditions (ensure)

Verify outputs after execution. The feature's promise.

ensure
    balance_reduced: balance = old balance - amount
    non_negative: balance >= 0

Class Invariants (invariant)

Always true for the object. Checked after every public call.

invariant
    non_negative_balance: balance >= 0
    valid_account_number: account_number.count = 10

Check Assertions

Mid-execution checks for debugging and documentation.

check
    valid_state: is_initialized
end

The "old" Keyword

One of the most powerful features: comparing before and after.

ensure
    count_increased: items.count = old items.count + 1

old items.count captures the value BEFORE the feature ran. This lets you specify exactly how state should change.

Contracts vs. Tests

Tests

"Here are some examples that should work."

Check specific cases.

Contracts

"Here is what must ALWAYS be true."

Check every execution.

Tests are valuable. Contracts are comprehensive. Use both. But contracts catch what tests miss.

Why This Matters for AI

AI generates statistically likely code. "Likely" isn't "correct."

Contracts turn "I hope this works" into "This is proven to work."

That's the unlock.

Get Started See the Evidence