Design by Contract in Python

1

Contract Mindset

Why this matters

Defensive Programming asks “how do I reject bad input clearly?” Design by Contract asks a sharper question first: “whose job was this?” That single shift in framing changes how the code is structured — sometimes radically.

Bertrand Meyer, who coined Design by Contract in the 1980s, argued explicitly against defensive programming. He called blanket input-checking a methodology that “can only … cause … a decrease in reliability” because redundant checks across a large system compound into “a monster of useless complexity.” His Non-Redundancy Principle: under no circumstances shall the body of a routine ever test for its precondition. The caller’s job is to satisfy preconditions; the supplier’s job is to satisfy postconditions, assuming the preconditions held.

That’s a strong claim — and the opposite of the DP tutorial you just finished. This step makes the contrast visible by putting two versions of the same function side by side, then introduces the pragmatic Python middle ground we’ll use for the rest of the tutorial.

🎯 You will learn to

Analyze the same function as a Defensive Programming artifact vs. a Design by Contract artifact.
Distinguish caller obligations (preconditions) from supplier guarantees (postconditions).
Apply the Non-Redundancy Principle to decide where a check belongs.

Two implementations, same behavior on valid inputs

Open discounts.py. It contains two versions of discounted_price(price, discount). Their visible behavior on valid inputs is identical. Their framing of responsibility is very different.

Version A

def discounted_price_A(price, discount):
    if not isinstance(price, (int, float)):
        raise TypeError("price must be a number")
    if not isinstance(discount, (int, float)):
        raise TypeError("discount must be a number")
    if price < 0:
        raise ValueError("price must be non-negative")
    if not (0 <= discount <= 1):
        raise ValueError("discount must be between 0 and 1")
    return price * (1 - discount)

Version B

def discounted_price_B(price, discount):
    """Return price after applying a fractional discount.

    Preconditions (caller's obligation):
        - price >= 0
        - 0 <= discount <= 1

    Postcondition (supplier's guarantee, given preconditions hold):
        - result == price * (1 - discount)
        - 0 <= result <= price
    """
    return price * (1 - discount)

✏️ Predict before you read on

Commit to a letter, then open the reveal.

(a) A is Defensive Programming; B is Design by Contract.
(b) B is Defensive Programming; A is Design by Contract.
(c) They are equivalent — labels are decoration.
(d) Both are Defensive — DbC requires a different language like Eiffel.

Reveal

**(a) is correct.** Version A is **Defensive Programming**: every assumption is checked at the boundary of the routine, before any useful work happens. Version B is **Design by Contract** in the pure Meyer sense: the contract is *documented*; the body *assumes* the precondition; there are no defensive checks in the body. The other letters map to specific misconceptions worth naming: - **(b)** confuses "more code = more rigorous." DbC's claim is the opposite: contracts let you write *less* code by allocating responsibility. - **(c)** treats this as a style preference. It isn't. Labels matter because they change *who is responsible when something fails*. A failure in Version A is the function's fault for letting bad input through. A failure in Version B is the *caller's* fault for violating the documented precondition. - **(d)** DbC is a methodology, not a language. Eiffel makes it ergonomic; Python can do it with discipline and small helpers.

What each style optimizes for

Aspect	Defensive Programming (A)	Design by Contract (B)
Trust assumption	Caller may be hostile or buggy	Caller is a partner who reads the contract
Where checks live	Inside the routine body	Outside, in the caller’s context — or not at all
Scales well to	Public APIs, untrusted boundaries	Large libraries with many internal callers
Fails badly when	Internal callers pay validation cost on every call	Public APIs accept untrusted input
Performance cost	Permanent	Optional — Eiffel disables monitoring in release builds

The conclusion both Meyer and modern practice agree on: use DbC for internal module boundaries; use DP at the system boundary (user input, network, files, databases). They are complementary, not competing. The mistake is doing both for the same condition — that’s the redundancy Meyer warned about.

A pragmatic Python middle ground

Python doesn’t have a built-in contract language. For this tutorial we use two tiny helpers that make the contract visible and runtime-checked — useful for learning and for debugging, optional in production:

def require(condition: bool, message: str, *, kind: str = "value") -> None:
    """Caller obligation. kind='type' raises TypeError; default raises ValueError."""
    if not condition:
        raise (TypeError if kind == "type" else ValueError)(message)

def ensure(condition: bool, message: str) -> None:
    """Supplier guarantee. Failure is a supplier bug → AssertionError."""
    if not condition:
        raise AssertionError(message)

Two intentional design choices worth naming:

require accepts a kind="type" flag. This keeps us consistent with the DP tutorial’s TypeError/ValueError discipline. In pure DbC, every precondition violation is the same thing — a caller bug — and the exception class is a Python-pragmatic refinement, not a core concept. We use kind="type" only when distinguishing the diagnostic adds clarity.
ensure raises AssertionError instead of ValueError. A postcondition failure is the supplier’s bug, not the caller’s. Distinct exception classes make blame visible in tracebacks. We don’t use Python’s built-in assert because python -O strips it — but conceptually it’s the same thing. In Eiffel, contract monitoring is a compile flag that turns checks on or off without altering the specification itself.

Version C below is the working version we’ll build on for the rest of the tutorial — DbC framing, runtime monitoring, no inline type defense:

def discounted_price(price: float, discount: float) -> float:
    require(price >= 0, "price must be non-negative")
    require(0 <= discount <= 1, "discount must be between 0 and 1")
    result = price * (1 - discount)
    ensure(0 <= result <= price, "result must stay between 0 and original price")
    return result

Notice what’s not there: type checks. In pure DbC you would document price: REAL and let the type system or the caller’s contract handle wrong types. We will sometimes add require(isinstance(...), ..., kind="type") later when it sharpens diagnostics — but every time we do, we’re paying the same redundancy cost Meyer warned about. It’s a trade-off, not a default.

Starter files

discounts.py

# ============================================================
# Two methodologies, one function.
# Read both versions, then study Version C — the DbC framing
# we will build on for the rest of the tutorial.
# ============================================================

# ---- Version A: Defensive Programming ----
def discounted_price_A(price, discount):
    if not isinstance(price, (int, float)):
        raise TypeError("price must be a number")
    if not isinstance(discount, (int, float)):
        raise TypeError("discount must be a number")
    if price < 0:
        raise ValueError("price must be non-negative")
    if not (0 <= discount <= 1):
        raise ValueError("discount must be between 0 and 1")
    return price * (1 - discount)


# ---- Version B: Design by Contract (pure Meyer) ----
def discounted_price_B(price, discount):
    """Return price after applying a fractional discount.

    Preconditions (caller's obligation):
        - price >= 0
        - 0 <= discount <= 1

    Postcondition (supplier's guarantee, given preconditions hold):
        - result == price * (1 - discount)
        - 0 <= result <= price
    """
    return price * (1 - discount)


# ---- Contract helpers (used from Version C onward) ----
def require(condition: bool, message: str, *, kind: str = "value") -> None:
    """Caller obligation. kind='type' raises TypeError; default raises ValueError."""
    if not condition:
        raise (TypeError if kind == "type" else ValueError)(message)


def ensure(condition: bool, message: str) -> None:
    """Supplier guarantee. Failure is the supplier's bug → AssertionError."""
    if not condition:
        raise AssertionError(message)


# ---- Version C: DbC with runtime monitoring (our working version) ----
def discounted_price(price: float, discount: float) -> float:
    """Return price after applying a fractional discount."""
    require(price >= 0, "price must be non-negative")
    require(0 <= discount <= 1, "discount must be between 0 and 1")
    result = price * (1 - discount)
    ensure(0 <= result <= price, "result must stay between 0 and original price")
    return result

Step 1 — Knowledge Check

Min. score: 80%

1. Which statement best captures Meyer’s Non-Redundancy Principle?

A routine’s body should never test for its own precondition; the caller is responsible.
Every routine should validate every input at the top of its body.
This is the defensive programming prescription Meyer was arguing against. Non-Redundancy says the opposite.
Preconditions and postconditions should always be checked, even in production.
Meyer specifically allowed turning monitoring off in production (it’s a compile flag in Eiffel). The principle is about who is responsible, not whether checks run.
Defensive programming and Design by Contract are equivalent in practice.
They use related vocabulary (preconditions, postconditions) but reach opposite conclusions about where checks should live.

Non-Redundancy: a consistency condition belongs to one of the two parties — caller or supplier — never both. Checking on both sides is wasted complexity that scales badly.

2. discounted_price_A(-10, 0.2) raises ValueError. discounted_price_B(-10, 0.2) returns -12.0 — a negative price. Which framing is each version using?

A is Defensive (catches the bad input itself); B is DbC (relies on the caller to satisfy the precondition).
A is DbC (precise exception); B is Defensive (silent acceptance).
Raising a precise exception is a DP move, not a DbC one. DbC’s claim is that the caller should have prevented this call in the first place.
Both are Defensive — both are written in Python.
The framing is about where the check lives, not the language. Python supports both styles equally.
Both are DbC — both have meaningful behavior.
B has a docstring contract; A does not. The presence of inline checks (A) vs. a documented precondition (B) is the distinguishing mark.

A actively defends against bad input. B trusts the caller to satisfy the precondition — and exhibits ‘arbitrary behavior’ when the caller breaks it. Meyer’s view: that’s not a bug in B; it’s a bug in the caller.

3. In Version C, require raises ValueError (or TypeError with kind="type") and ensure raises AssertionError. Why two different exception classes?

To make traceback blame visible: ValueError/TypeError ⇒ caller bug; AssertionError ⇒ supplier bug.
Because AssertionError is faster to raise.
Exception cost is dominated by traceback construction, not the class. The choice is pedagogical, not performance.
Because ValueError is reserved for caller bugs by the Python language.
Python does not enforce this — ValueError is just an exception class. The convention here is ours, encoding the contract responsibility split.
It’s stylistic with no semantic meaning.
It’s stylistic in the sense Python doesn’t force it, but it’s load-bearing for the contract framing: blame should be visible at the point of failure.

The two exception classes encode the DbC responsibility split in Python’s exception system. A ValueError in a stack trace says ‘caller did wrong’; an AssertionError says ‘this routine failed to deliver on its promise.’

4. discounted_price(100, 0.25) returns 10 — clearly wrong; should be 75. The caller satisfied both preconditions. Who violated the contract?

The supplier — preconditions held, so the result must satisfy every postcondition.
The caller — 25 percent is a large discount.
0.25 is inside the documented range [0, 1]. The caller met the precondition.
Neither — the result is non-negative, which is one of the postconditions.
A weak postcondition that any result satisfies (like ‘non-negative’) is not the full contract. The formula and the upper bound are both postconditions.
Both — discount math is shared responsibility.
When the caller met every precondition, the supplier owes every postcondition. Shared blame would defeat the responsibility allocation.

Preconditions held ⇒ supplier owes every postcondition. The implementation produced 10, violating both the formula and the upper-bound postcondition — that’s a supplier bug, and ensure raises AssertionError to make it visible.

2

Good Preconditions

Why this matters

A good precondition rejects calls that the function cannot honestly handle before the algorithm starts. That keeps the body simple and makes failures point to the caller’s contract violation, not to obscure runtime errors deep inside the math.

🔗 Bridging from Defensive Programming

In DP Step 2 (repeat) you used TypeError for wrong-kind inputs and ValueError for wrong-value inputs. In Design by Contract, both are just “the caller violated a precondition” — the responsibility label is the core concept, not the exception class. We keep kind="type" on require as a Python-pragmatic refinement (it sharpens diagnostics), but Meyer’s argument is that who matters more than what.

🎯 You will learn to

Apply require to reject invalid inputs before computation.
Validate emptiness, numeric type, NaN, and infinity as separate precondition concerns.
Keep the actual mean calculation small after preconditions pass.

Your task

Implement mean_nonempty(xs).

Preconditions:

xs is non-empty.
Every element is a real number, but not bool.
Every element is finite: not NaN, not positive infinity, and not negative infinity.

Postcondition:

The result equals sum(xs) / len(xs) for the validated values.

Use require(...) for precondition checks and ensure(...) for the postcondition.

Starter files

means.py

import math
from collections.abc import Sequence


def require(condition: bool, message: str, *, kind: str = "value") -> None:
    """Caller obligation. kind='type' raises TypeError; default raises ValueError."""
    if not condition:
        raise (TypeError if kind == "type" else ValueError)(message)


def ensure(condition: bool, message: str) -> None:
    """Supplier guarantee. Failure raises AssertionError."""
    if not condition:
        raise AssertionError(message)


def mean_nonempty(xs: Sequence[float]) -> float:
    """Return the arithmetic mean of a non-empty finite numeric sequence."""
    # Add preconditions before computing.
    result = sum(xs) / len(xs)
    return result

test_means.py

import math
import pytest
from means import mean_nonempty


def test_valid_values_return_mean():
    assert mean_nonempty([2, 4, 6]) == pytest.approx(4)
    assert mean_nonempty([1.5, 2.5]) == pytest.approx(2.0)


def test_empty_sequence_violates_precondition():
    with pytest.raises(ValueError):
        mean_nonempty([])


def test_nonnumeric_value_violates_precondition():
    # Type predicate violated → TypeError (require with kind="type").
    with pytest.raises(TypeError):
        mean_nonempty([1, "2", 3])


def test_nan_and_infinity_violate_precondition():
    for value in [math.nan, math.inf, -math.inf]:
        with pytest.raises(ValueError):
            mean_nonempty([1, value])

Solution

means.py

import math
from collections.abc import Sequence


def require(condition: bool, message: str, *, kind: str = "value") -> None:
    """Caller obligation. kind='type' raises TypeError; default raises ValueError."""
    if not condition:
        raise (TypeError if kind == "type" else ValueError)(message)


def ensure(condition: bool, message: str) -> None:
    """Supplier guarantee. Failure raises AssertionError."""
    if not condition:
        raise AssertionError(message)


def mean_nonempty(xs: Sequence[float]) -> float:
    """Return the arithmetic mean of a non-empty finite numeric sequence."""
    require(len(xs) > 0, "xs must be non-empty")
    for value in xs:
        require(
            isinstance(value, (int, float)) and not isinstance(value, bool),
            "all values must be real numbers",
            kind="type",
        )
        require(math.isfinite(value), "all values must be finite")

    result = sum(xs) / len(xs)
    ensure(result == sum(xs) / len(xs), "result must equal the arithmetic mean")
    return result

The computation is only reached after the caller has supplied a non-empty sequence of finite numbers — the contract split: caller prepares valid inputs, supplier computes the promised result. Type predicates use kind="type" so wrong-kind inputs raise TypeError; numeric-domain checks (math.isfinite, length) stay default and raise ValueError. In pure DbC both would be the same — “caller violated precondition” — but the Python-pragmatic split keeps stack traces diagnostic.

3

Strong Postconditions

Why this matters

Weak postconditions let broken code pass. For a sequence operation, “returns a list” is not enough; the contract should say exactly what changed and what stayed untouched.

🔗 Bridging from Defensive Programming

In DP Step 4 (ClosedInterval.__post_init__) you enforced an invariant at construction: a one-time check at the start of the object’s life. Postconditions are a related but different idea — instead of “what must always be true of this object,” they say “what must be true after this call returns, given the inputs and the prior state.” The old_xs snapshot is the new tool that lets a postcondition reference the input as it was at entry, even after the function has done work.

🎯 You will learn to

Use an old-state snapshot to compare before and after behavior.
Specify a sequence transformation without mutating the input.
Apply ensure to check a strong postcondition.

Your task

Implement:

def remove_at(xs: Sequence[int], index: int) -> list[int]:
    ...

Contract:

Precondition: 0 <= index < len(xs).
The function returns a new list.
The input sequence is not mutated.
The returned list is exactly the old sequence with the element at index removed.

Create old_xs = list(xs) before making the result. Use ensure(...) to check the returned list against old_xs[:index] + old_xs[index + 1:].

Starter files

sequences.py

from collections.abc import Sequence


def require(condition: bool, message: str, *, kind: str = "value") -> None:
    """Caller obligation. kind='type' raises TypeError; default raises ValueError."""
    if not condition:
        raise (TypeError if kind == "type" else ValueError)(message)


def ensure(condition: bool, message: str) -> None:
    """Supplier guarantee. Failure raises AssertionError."""
    if not condition:
        raise AssertionError(message)


def remove_at(xs: Sequence[int], index: int) -> list[int]:
    """Return a new list with the item at index removed."""
    require(0 <= index < len(xs), "index must be in range")
    # Snapshot old state before building the result.
    old_xs = ...
    result = list(xs)
    result.pop(index)
    return result

test_sequences.py

import pytest
from sequences import remove_at


def test_removes_first_middle_and_last_items():
    assert remove_at([10, 20, 30], 0) == [20, 30]
    assert remove_at([10, 20, 30], 1) == [10, 30]
    assert remove_at([10, 20, 30], 2) == [10, 20]


def test_invalid_index_violates_precondition():
    with pytest.raises(ValueError):
        remove_at([10, 20, 30], -1)
    with pytest.raises(ValueError):
        remove_at([10, 20, 30], 3)


def test_input_list_is_not_mutated():
    xs = [10, 20, 30]
    result = remove_at(xs, 1)
    assert result == [10, 30]
    assert xs == [10, 20, 30]
    assert result is not xs

Solution

sequences.py

from collections.abc import Sequence


def require(condition: bool, message: str, *, kind: str = "value") -> None:
    """Caller obligation. kind='type' raises TypeError; default raises ValueError."""
    if not condition:
        raise (TypeError if kind == "type" else ValueError)(message)


def ensure(condition: bool, message: str) -> None:
    """Supplier guarantee. Failure raises AssertionError."""
    if not condition:
        raise AssertionError(message)


def remove_at(xs: Sequence[int], index: int) -> list[int]:
    """Return a new list with the item at index removed."""
    require(0 <= index < len(xs), "index must be in range")
    old_xs = list(xs)
    result = old_xs[:index] + old_xs[index + 1:]
    ensure(list(xs) == old_xs, "input sequence must not be mutated")
    ensure(result == old_xs[:index] + old_xs[index + 1:], "result must remove exactly one item")
    return result

The old-state snapshot lets the postcondition say exactly what changed. Without old_xs, a postcondition can easily become a weak check against whatever the current state happens to be.

4

Class Invariants

Why this matters

An invariant is a fact that should be true after construction and after every public method call. Once an object promises an invariant, every method can rely on it instead of re-validating the whole object from scratch.

🔗 Bridging from Defensive Programming

In DP Step 4 (ClosedInterval.__post_init__) you protected the object by validating at construction — one stable time, at the start of the object’s life. DbC’s invariant idea extends this: there are many stable times — after construction, and before and after every public method call. The invariant must hold at every one of them. Meyer’s diagram (an object lifecycle as S1 → S2 → S3 → … with INV true at each S_i) makes this visible. The constructor check is the first guardrail in a longer chain.

🎯 You will learn to

Define a _check_invariant method for object state.
Use preconditions for invalid caller requests.
Use postconditions and invariant checks after mutation.

Your task

Implement BankAccount.

Invariant:

owner is a non-empty string after stripping whitespace.
balance is a non-negative integer.

Method contracts:

deposit(amount) requires a positive integer amount and increases balance by exactly that amount.
withdraw(amount) requires a positive integer amount and sufficient funds, then decreases balance by exactly that amount.
Both methods preserve the invariant.

Starter files

accounts.py

def require(condition: bool, message: str, *, kind: str = "value") -> None:
    """Caller obligation. kind='type' raises TypeError; default raises ValueError."""
    if not condition:
        raise (TypeError if kind == "type" else ValueError)(message)


def ensure(condition: bool, message: str) -> None:
    """Supplier guarantee. Failure raises AssertionError."""
    if not condition:
        raise AssertionError(message)


class BankAccount:
    def __init__(self, owner: str, balance: int = 0) -> None:
        self.owner = owner
        self.balance = balance
        # Check the invariant after construction.

    def _check_invariant(self) -> None:
        # owner must be a non-empty string; balance must be a non-negative int.
        pass

    def deposit(self, amount: int) -> None:
        # Increase balance by exactly amount.
        pass

    def withdraw(self, amount: int) -> None:
        # Decrease balance by exactly amount without overdrawing.
        pass

test_accounts.py

import pytest
from accounts import BankAccount


def test_valid_construction_sets_owner_and_balance():
    account = BankAccount("Maya", 25)
    assert account.owner == "Maya"
    assert account.balance == 25


def test_construction_requires_valid_invariant_values():
    with pytest.raises(ValueError):
        BankAccount("", 0)
    with pytest.raises(ValueError):
        BankAccount("Maya", -1)


def test_deposit_increases_balance_exactly():
    account = BankAccount("Maya", 25)
    account.deposit(10)
    assert account.balance == 35


def test_withdraw_decreases_balance_exactly():
    account = BankAccount("Maya", 25)
    account.withdraw(10)
    assert account.balance == 15


def test_overdraft_is_rejected():
    account = BankAccount("Maya", 25)
    with pytest.raises(ValueError):
        account.withdraw(26)
    assert account.balance == 25

Solution

accounts.py

def require(condition: bool, message: str, *, kind: str = "value") -> None:
    """Caller obligation. kind='type' raises TypeError; default raises ValueError."""
    if not condition:
        raise (TypeError if kind == "type" else ValueError)(message)


def ensure(condition: bool, message: str) -> None:
    """Supplier guarantee. Failure raises AssertionError."""
    if not condition:
        raise AssertionError(message)


def _ensure_positive_int(value: object, name: str = "amount") -> None:
    """Combined precondition: a strictly positive integer (not bool).

    Splits the type predicate (TypeError) from the value predicate (ValueError)
    so callers see precise diagnostics. In pure DbC both would be 'caller bug'.
    """
    require(
        isinstance(value, int) and not isinstance(value, bool),
        f"{name} must be an integer",
        kind="type",
    )
    require(value > 0, f"{name} must be positive")


class BankAccount:
    def __init__(self, owner: str, balance: int = 0) -> None:
        require(isinstance(owner, str), "owner must be a string", kind="type")
        require(owner.strip() != "", "owner must be non-empty")
        require(
            isinstance(balance, int) and not isinstance(balance, bool),
            "balance must be an integer",
            kind="type",
        )
        require(balance >= 0, "balance must be non-negative")
        self.owner = owner
        self.balance = balance
        self._check_invariant()

    def _check_invariant(self) -> None:
        ensure(isinstance(self.owner, str) and self.owner.strip() != "", "owner invariant failed")
        ensure(isinstance(self.balance, int) and not isinstance(self.balance, bool), "balance type invariant failed")
        ensure(self.balance >= 0, "balance invariant failed")

    def deposit(self, amount: int) -> None:
        _ensure_positive_int(amount)
        old_balance = self.balance
        self.balance += amount
        self._check_invariant()
        ensure(self.balance == old_balance + amount, "deposit must increase balance exactly")

    def withdraw(self, amount: int) -> None:
        _ensure_positive_int(amount)
        require(amount <= self.balance, "insufficient funds")
        old_balance = self.balance
        self.balance -= amount
        self._check_invariant()
        ensure(self.balance == old_balance - amount, "withdraw must decrease balance exactly")

The constructor uses preconditions for caller-provided values, splitting type predicates (kind="type" → TypeError) from value predicates (default → ValueError). _check_invariant then records the object’s stable-time promise: it must hold right after construction, and before and after every public method call. Each mutating method checks its own preconditions, changes state once, and verifies both the invariant and the exact balance change via ensure.

5

Multi-Object Contracts

Why this matters

Contracts become more useful when an operation coordinates multiple objects. The preconditions say when the operation is allowed; the postconditions say what changed across the whole collaboration.

🔗 Bridging from Defensive Programming

In DP Step 6 (the port-range parser) you combined input validation, postcondition reasoning, and exact exception types in a single function. transfer does the same combination, but now across two objects: preconditions guard caller mistakes, postconditions specify the exact change, and each object’s invariant must still hold afterward. The mechanics are familiar; the framing is responsibility allocation across multiple parties — Meyer’s metaphor is a contract between a client and two suppliers cooperating.

🎯 You will learn to

Write preconditions that involve more than one object.
Use old-state snapshots for two-object postconditions.
Preserve local invariants and a global total in one operation.

Your task

Implement:

def transfer(src: BankAccount, dst: BankAccount, amount: int) -> None:
    ...

Preconditions:

src and dst are distinct BankAccount objects.
amount is a positive integer.
src.balance >= amount.

Postconditions:

source balance decreases by exactly amount
destination balance increases by exactly amount
total money across the two accounts is preserved
both account invariants still hold

Starter files

accounts.py

def require(condition: bool, message: str, *, kind: str = "value") -> None:
    """Caller obligation. kind='type' raises TypeError; default raises ValueError."""
    if not condition:
        raise (TypeError if kind == "type" else ValueError)(message)


def ensure(condition: bool, message: str) -> None:
    """Supplier guarantee. Failure raises AssertionError."""
    if not condition:
        raise AssertionError(message)


def _ensure_positive_int(value: object, name: str = "amount") -> None:
    """Combined precondition: a strictly positive integer (not bool)."""
    require(
        isinstance(value, int) and not isinstance(value, bool),
        f"{name} must be an integer",
        kind="type",
    )
    require(value > 0, f"{name} must be positive")


class BankAccount:
    def __init__(self, owner: str, balance: int = 0) -> None:
        require(isinstance(owner, str), "owner must be a string", kind="type")
        require(owner.strip() != "", "owner must be non-empty")
        require(
            isinstance(balance, int) and not isinstance(balance, bool),
            "balance must be an integer",
            kind="type",
        )
        require(balance >= 0, "balance must be non-negative")
        self.owner = owner
        self.balance = balance
        self._check_invariant()

    def _check_invariant(self) -> None:
        ensure(isinstance(self.owner, str) and self.owner.strip() != "", "owner invariant failed")
        ensure(isinstance(self.balance, int) and not isinstance(self.balance, bool), "balance type invariant failed")
        ensure(self.balance >= 0, "balance invariant failed")

    def deposit(self, amount: int) -> None:
        _ensure_positive_int(amount)
        old_balance = self.balance
        self.balance += amount
        self._check_invariant()
        ensure(self.balance == old_balance + amount, "deposit must increase balance exactly")

    def withdraw(self, amount: int) -> None:
        _ensure_positive_int(amount)
        require(amount <= self.balance, "insufficient funds")
        old_balance = self.balance
        self.balance -= amount
        self._check_invariant()
        ensure(self.balance == old_balance - amount, "withdraw must decrease balance exactly")


def transfer(src: BankAccount, dst: BankAccount, amount: int) -> None:
    """Move amount from src to dst."""
    # Add preconditions, old-state snapshots, the transfer, and postconditions.
    pass

test_transfer.py

import pytest
from accounts import BankAccount, transfer


def test_valid_transfer_moves_money_exactly():
    src = BankAccount("Maya", 100)
    dst = BankAccount("Noor", 25)
    transfer(src, dst, 40)
    assert src.balance == 60
    assert dst.balance == 65


def test_transfer_preserves_total_money():
    src = BankAccount("Maya", 100)
    dst = BankAccount("Noor", 25)
    before = src.balance + dst.balance
    transfer(src, dst, 40)
    assert src.balance + dst.balance == before


def test_self_transfer_is_rejected():
    src = BankAccount("Maya", 100)
    with pytest.raises(ValueError):
        transfer(src, src, 10)
    assert src.balance == 100


def test_overspend_is_rejected_without_mutation():
    src = BankAccount("Maya", 30)
    dst = BankAccount("Noor", 25)
    with pytest.raises(ValueError):
        transfer(src, dst, 40)
    assert src.balance == 30
    assert dst.balance == 25

Solution

accounts.py

def require(condition: bool, message: str, *, kind: str = "value") -> None:
    """Caller obligation. kind='type' raises TypeError; default raises ValueError."""
    if not condition:
        raise (TypeError if kind == "type" else ValueError)(message)


def ensure(condition: bool, message: str) -> None:
    """Supplier guarantee. Failure raises AssertionError."""
    if not condition:
        raise AssertionError(message)


def _ensure_positive_int(value: object, name: str = "amount") -> None:
    """Combined precondition: a strictly positive integer (not bool)."""
    require(
        isinstance(value, int) and not isinstance(value, bool),
        f"{name} must be an integer",
        kind="type",
    )
    require(value > 0, f"{name} must be positive")


class BankAccount:
    def __init__(self, owner: str, balance: int = 0) -> None:
        require(isinstance(owner, str), "owner must be a string", kind="type")
        require(owner.strip() != "", "owner must be non-empty")
        require(
            isinstance(balance, int) and not isinstance(balance, bool),
            "balance must be an integer",
            kind="type",
        )
        require(balance >= 0, "balance must be non-negative")
        self.owner = owner
        self.balance = balance
        self._check_invariant()

    def _check_invariant(self) -> None:
        ensure(isinstance(self.owner, str) and self.owner.strip() != "", "owner invariant failed")
        ensure(isinstance(self.balance, int) and not isinstance(self.balance, bool), "balance type invariant failed")
        ensure(self.balance >= 0, "balance invariant failed")

    def deposit(self, amount: int) -> None:
        _ensure_positive_int(amount)
        old_balance = self.balance
        self.balance += amount
        self._check_invariant()
        ensure(self.balance == old_balance + amount, "deposit must increase balance exactly")

    def withdraw(self, amount: int) -> None:
        _ensure_positive_int(amount)
        require(amount <= self.balance, "insufficient funds")
        old_balance = self.balance
        self.balance -= amount
        self._check_invariant()
        ensure(self.balance == old_balance - amount, "withdraw must decrease balance exactly")


def transfer(src: BankAccount, dst: BankAccount, amount: int) -> None:
    """Move amount from src to dst."""
    require(isinstance(src, BankAccount), "src must be a BankAccount", kind="type")
    require(isinstance(dst, BankAccount), "dst must be a BankAccount", kind="type")
    require(src is not dst, "source and destination must be distinct accounts")
    _ensure_positive_int(amount)
    require(src.balance >= amount, "source has insufficient funds")

    old_src_balance = src.balance
    old_dst_balance = dst.balance
    old_total = old_src_balance + old_dst_balance

    src.withdraw(amount)
    dst.deposit(amount)

    src._check_invariant()
    dst._check_invariant()
    ensure(src.balance == old_src_balance - amount, "source must be debited exactly once")
    ensure(dst.balance == old_dst_balance + amount, "destination must be credited exactly once")
    ensure(src.balance + dst.balance == old_total, "total money must be preserved")

The transfer contract coordinates two local objects and one global property. Preconditions reject invalid operations before mutation (type predicates raise TypeError; value predicates raise ValueError); postconditions verify the exact debit, exact credit, and preserved total. The isinstance(src, BankAccount) guards are language-level pragmatism, not core DbC — in Eiffel the type system would handle this at compile time.

Step 5 — Knowledge Check

Min. score: 80%

1. Suppose transfer is exposed as a public REST endpoint receiving JSON like {"src": "acct-1", "dst": "acct-2", "amount": "40"}. Which Defensive Programming techniques from the DP tutorial re-enter the picture, and where?

All of: parse and validate JSON shape at the boundary, raise TypeError for non-strings, raise ValueError for malformed amounts, look up BankAccount instances from validated IDs, then call transfer with already-validated arguments.
None — transfer’s preconditions already cover it, so DbC is sufficient end-to-end.
DbC works between trusting parties. JSON over HTTP arrives from an untrusting boundary — every field could be anything. Preconditions presume the input is already a BankAccount and an int; that presumption is what the boundary layer must establish.
Only the postcondition check matters; type validation is the framework’s job.
Type validation belongs at the trust boundary, not deferred. If amount arrives as the string "40", no postcondition can save the day — the function will fail or silently produce garbage before any ensure runs.
Wrap the call in except Exception: so the endpoint can return generic 400s.
Broad exception catching is the DP anti-pattern from DP Step 5 (load_json_config). It hides the cause — exactly the opposite of what DbC’s blame allocation is trying to make visible.

At the system boundary (network, files, user input), DP is the right tool — validate aggressively, raise precise exceptions, translate failures into domain errors. Inside the system, between trusted modules, DbC takes over. Meyer endorses this exact split: filter modules at the boundary, contract-based modules in the interior.

2. Your transfer solution uses require(isinstance(src, BankAccount), ..., kind="type"). In pure Meyer DbC, this would be considered redundant. Why do we keep it in Python?

In statically-typed DbC (Eiffel), the type system enforces it at compile time. Python is dynamic, so this isinstance is the lightweight equivalent — a language pragmatism, not a DbC concept.
Because isinstance is faster than the alternatives.
Performance isn’t the issue. Contract responsibility doesn’t change based on speed; the question is whether the type system can already enforce the precondition.
Because transfer should validate every argument as defensively as possible.
DbC does not recommend defensive maximalism. It recommends precise responsibility allocation. We add this check only because Python can’t enforce it for us at compile time.
Because BankAccount instances might be corrupted between calls.
Object integrity is what invariants protect — and _check_invariant already does that work. The isinstance guard is about the variable src (could be None, a string, etc.), not the BankAccount instance.

Pure DbC assumes static types. Python doesn’t have static type enforcement at runtime, so we add a small isinstance guard as a language-level necessity. It’s a DP-style check, but we’re using it specifically to compensate for what static typing would otherwise provide for free.

6

Substitution: Subclass Contracts

Why this matters

Contracts matter most when code is reused through an interface or subclass. The Liskov Substitution Principle says a subclass must be usable anywhere the base class was expected — which means it must accept everything the base accepted, and guarantee everything the base guaranteed. Violating substitutability silently breaks every caller written against the base.

The rules sound simple but trap students every time: most learners’ intuition is “a subclass is more specific, so it can demand more.” The opposite is true. This step makes the rules executable — you’ll implement a subclass, and a test harness will run every base-class test against your subclass to verify substitutability holds. Then property-based testing will explore the substitution space with hundreds of generated operation sequences.

🔗 Bridging from Defensive Programming

In DP Step 3 (clamp) you saw why silent repair is dangerous: swapping reversed bounds hid the caller’s mistake. The Liskov rule is the inheritance-time version of the same idea — a subclass that demands more (stronger precondition) or promises less (weaker postcondition) silently breaks every caller written against the base. Same harm, different layer. Substitutability protects callers from invisible contract changes the way clamp’s explicit rejection protected callers from invisible argument swaps.

🎯 You will learn to

Apply the weaker-precondition / stronger-postcondition rule to subclass contracts.
Create a subclass that legally strengthens a postcondition.
Evaluate substitutability with both example-based and property-based tests.

The rule

A safe replacement may:

Weaken preconditions — accept everything the base accepted, and maybe more.
Strengthen postconditions — guarantee everything the base guaranteed, and maybe more.

It may not:

Strengthen preconditions — old callers might now be rejected.
Weaken postconditions — old callers might no longer get what they relied on.

Mnemonic: a subclass can be more accepting on the way in and more generous on the way out — never the reverse.

Your task

Implement SavingsAccount(BankAccount) with a strengthened postcondition: every successful deposit and withdraw is recorded in a transactions list. The list contains tuples of (kind, amount, balance_after), where kind is "deposit" or "withdraw".

Concretely, SavingsAccount must:

Inherit from BankAccount.
Maintain a transactions attribute (a list[tuple[str, int, int]]).
Override deposit and withdraw to record the transaction after the base operation succeeds.
Not strengthen any precondition — every call that worked on a BankAccount must still work on a SavingsAccount.
Not weaken any postcondition — balance changes must still be exactly as the base specified.

This is a legal contract change: postconditions strengthen (the new transactions guarantee), preconditions stay equal, and the existing balance invariant is preserved.

How substitutability is tested

Two layers, both visible in test_savings.py:

Parametrized fixture (AccountCls): every base-class test runs against both BankAccount and SavingsAccount. If the subclass narrowed the contract in any way, at least one base test fails on it.
Hypothesis property test: generates random valid sequences of deposit/withdraw operations and asserts the two classes agree on final balance across the whole sequence. This catches contract narrowing that example tests miss.

Property-based testing is evidence, not proof — it samples many inputs, not all. But for substitutability it’s an excellent fit because the property (“base and subclass agree”) is straightforward to state and surprisingly hard to game.

Starter files

accounts.py

def require(condition: bool, message: str, *, kind: str = "value") -> None:
    """Caller obligation. kind='type' raises TypeError; default raises ValueError."""
    if not condition:
        raise (TypeError if kind == "type" else ValueError)(message)


def ensure(condition: bool, message: str) -> None:
    """Supplier guarantee. Failure raises AssertionError."""
    if not condition:
        raise AssertionError(message)


def _ensure_positive_int(value: object, name: str = "amount") -> None:
    """Combined precondition: a strictly positive integer (not bool)."""
    require(
        isinstance(value, int) and not isinstance(value, bool),
        f"{name} must be an integer",
        kind="type",
    )
    require(value > 0, f"{name} must be positive")


class BankAccount:
    def __init__(self, owner: str, balance: int = 0) -> None:
        require(isinstance(owner, str), "owner must be a string", kind="type")
        require(owner.strip() != "", "owner must be non-empty")
        require(
            isinstance(balance, int) and not isinstance(balance, bool),
            "balance must be an integer",
            kind="type",
        )
        require(balance >= 0, "balance must be non-negative")
        self.owner = owner
        self.balance = balance
        self._check_invariant()

    def _check_invariant(self) -> None:
        ensure(isinstance(self.owner, str) and self.owner.strip() != "", "owner invariant failed")
        ensure(isinstance(self.balance, int) and not isinstance(self.balance, bool), "balance type invariant failed")
        ensure(self.balance >= 0, "balance invariant failed")

    def deposit(self, amount: int) -> None:
        _ensure_positive_int(amount)
        old_balance = self.balance
        self.balance += amount
        self._check_invariant()
        ensure(self.balance == old_balance + amount, "deposit must increase balance exactly")

    def withdraw(self, amount: int) -> None:
        _ensure_positive_int(amount)
        require(amount <= self.balance, "insufficient funds")
        old_balance = self.balance
        self.balance -= amount
        self._check_invariant()
        ensure(self.balance == old_balance - amount, "withdraw must decrease balance exactly")

savings.py

from accounts import BankAccount, ensure


class SavingsAccount(BankAccount):
    """A BankAccount that additionally records every transaction.

    Contract strengthening:
      - Same preconditions as BankAccount.deposit / withdraw (do not narrow).
      - Same balance-change postconditions as BankAccount (do not weaken).
      - ADDITIONAL postcondition: after a successful deposit/withdraw,
        the last element of self.transactions describes that operation.
    """

    def __init__(self, owner: str, balance: int = 0) -> None:
        # Initialize subclass state BEFORE super().__init__ so that any
        # invariant check that touches transactions sees a valid list.
        self.transactions: list[tuple[str, int, int]] = []
        # TODO: delegate to BankAccount.__init__.

    def deposit(self, amount: int) -> None:
        # TODO: call the base deposit, then record ("deposit", amount, self.balance).
        pass

    def withdraw(self, amount: int) -> None:
        # TODO: call the base withdraw, then record ("withdraw", amount, self.balance).
        pass

test_savings.py

import pytest
from accounts import BankAccount
from savings import SavingsAccount


# =====================================================================
# Substitutability layer 1 — every BankAccount test runs against both
# BankAccount and SavingsAccount via a parametrized fixture.
# =====================================================================

@pytest.fixture(params=[BankAccount, SavingsAccount])
def AccountCls(request):
    return request.param


def test_valid_construction(AccountCls):
    account = AccountCls("Maya", 25)
    assert account.owner == "Maya"
    assert account.balance == 25


def test_construction_rejects_invalid_invariants(AccountCls):
    with pytest.raises(ValueError):
        AccountCls("", 0)
    with pytest.raises(ValueError):
        AccountCls("Maya", -1)


def test_deposit_changes_balance_exactly(AccountCls):
    account = AccountCls("Maya", 25)
    account.deposit(10)
    assert account.balance == 35


def test_withdraw_changes_balance_exactly(AccountCls):
    account = AccountCls("Maya", 25)
    account.withdraw(10)
    assert account.balance == 15


def test_overdraft_rejected(AccountCls):
    account = AccountCls("Maya", 25)
    with pytest.raises(ValueError):
        account.withdraw(26)
    assert account.balance == 25


def test_subclass_does_not_narrow_amount(AccountCls):
    # A single-cent deposit is valid for BankAccount; SavingsAccount must accept it too.
    account = AccountCls("Maya", 0)
    account.deposit(1)
    assert account.balance == 1


# =====================================================================
# Strengthened postcondition — unique to SavingsAccount.
# =====================================================================

def test_savings_records_each_transaction():
    account = SavingsAccount("Maya", 100)
    account.deposit(20)
    account.withdraw(50)
    assert account.transactions == [
        ("deposit", 20, 120),
        ("withdraw", 50, 70),
    ]


def test_savings_does_not_record_failed_operations():
    account = SavingsAccount("Maya", 10)
    with pytest.raises(ValueError):
        account.withdraw(99)
    # The failed withdraw must not appear in the ledger.
    assert account.transactions == []


# =====================================================================
# Substitutability layer 2 — Hypothesis explores hundreds of valid
# operation sequences and asserts the two classes agree on balance.
# =====================================================================

from hypothesis import given, settings, strategies as st


operation = st.tuples(
    st.sampled_from(["deposit", "withdraw"]),
    st.integers(min_value=1, max_value=1_000),
)


@settings(max_examples=100, deadline=None)
@given(start=st.integers(min_value=0, max_value=10_000),
       ops=st.lists(operation, max_size=20))
def test_savings_substitutes_for_bank_account(start, ops):
    base = BankAccount("base", start)
    sub = SavingsAccount("sub", start)

    for kind, amount in ops:
        try:
            getattr(base, kind)(amount)
        except ValueError:
            # If base rejects, subclass MUST reject too (no narrowing).
            with pytest.raises(ValueError):
                getattr(sub, kind)(amount)
            continue
        # Base accepted — subclass must also accept and reach the same balance.
        getattr(sub, kind)(amount)
        assert base.balance == sub.balance

Solution

savings.py

from accounts import BankAccount, ensure


class SavingsAccount(BankAccount):
    """A BankAccount that additionally records every transaction.

    Contract strengthening:
      - Same preconditions as BankAccount.deposit / withdraw (do not narrow).
      - Same balance-change postconditions as BankAccount (do not weaken).
      - ADDITIONAL postcondition: after a successful deposit/withdraw,
        the last element of self.transactions describes that operation.
    """

    def __init__(self, owner: str, balance: int = 0) -> None:
        self.transactions: list[tuple[str, int, int]] = []
        super().__init__(owner, balance)

    def deposit(self, amount: int) -> None:
        super().deposit(amount)
        self.transactions.append(("deposit", amount, self.balance))
        ensure(self.transactions[-1] == ("deposit", amount, self.balance),
               "transactions ledger must reflect the deposit")

    def withdraw(self, amount: int) -> None:
        super().withdraw(amount)
        self.transactions.append(("withdraw", amount, self.balance))
        ensure(self.transactions[-1] == ("withdraw", amount, self.balance),
               "transactions ledger must reflect the withdrawal")

The subclass legally strengthens the postcondition (adds the transactions guarantee) without touching preconditions. By delegating to super() first, the base precondition checks fire — failed operations raise before transactions.append runs, so the ledger stays clean. The parametrized fixture confirms the subclass passes every base-class behavioral test; the Hypothesis property confirms substitutability across hundreds of random valid operation sequences. Together they make Liskov substitutability executable rather than aspirational.

Step 6 — Knowledge Check

Min. score: 80%

1. A teammate proposes PremiumSavingsAccount.withdraw that requires amount >= 100. The base withdraw accepted any positive integer. Which Liskov rule did the proposal violate, and what’s the visible harm?

It strengthened a precondition — every caller that withdrew small amounts (e.g., a $20 ATM fee) now fails when handed a PremiumSavingsAccount.
It weakened a precondition — callers gain valid calls, which is always safe.
Rejecting more calls is a stronger precondition, not a weaker one. The set of accepted inputs shrinks.
It strengthened a postcondition — that’s always safe and substitutable.
The scenario changes which calls are allowed, not what’s guaranteed after success — that’s a precondition change, not a postcondition change.
Nothing — subclasses may always demand more, since they are ‘more specific.’
This is the canonical Liskov misconception. ‘More specific’ in vocabulary does not mean ‘demands more’ in contract terms — quite the opposite. Behavioral subtyping requires weaker-or-equal preconditions.

Strengthened preconditions break substitutability. Any caller that withdrew $20 from a BankAccount will fail when handed a PremiumSavingsAccount — the subclass has narrowed the contract.

2. Your SavingsAccount adds a transactions list — a field that BankAccount doesn’t have. Why does this still preserve substitutability?

Adding a guarantee (every successful operation is recorded) strengthens the postcondition; the base guarantees are still intact, and the new guarantee gives callers more.
It violates substitutability — adding fields is forbidden.
Subclasses adding new state is standard OO and explicitly allowed by Liskov’s rule — provided the new state does not weaken any existing guarantee.
It only works because Python allows attribute access without declaration.
Subclasses routinely add fields. The question is whether they preserve the visible-from-base contract.
It violates substitutability — only base-class fields may be touched.
Adding state is allowed in statically-typed languages too. The substitutability question is about contract, not language ergonomics.

A subclass may add fields, methods, and stronger postconditions. As long as every guarantee of the base still holds, the subclass remains substitutable. Our parametrized fixture verifies the base guarantees; the new ledger guarantee strengthens, doesn’t weaken.

3. The Hypothesis property test runs ~100 random operation sequences and checks that BankAccount and SavingsAccount agree on final balance. What does this prove, and what does it not?

Strong evidence of substitutability on the observed property (balance after operations) across the explored input space — not a proof across all inputs or all unobserved properties.
Proof of substitutability for all possible inputs, since Hypothesis explores all inputs.
Hypothesis explores many inputs intelligently, not all of them. It is a sampling tool with smart shrinking, not a proof tool. CrossHair or formal verification would be needed for full proof.
Nothing — property-based tests are no better than example tests.
Property tests are dramatically better than examples at finding edge cases (Hypothesis is excellent at counter-example shrinking), but they sample, not exhaust.
Proof that the implementations are byte-for-byte identical.
Two different classes can have identical observable behavior on the tested slice while differing internally — that’s fine. Substitutability is about observable behavior, not implementation.

Property tests are evidence, not proof. They cover far more inputs than examples and excel at finding contract violations, but for full substitutability across every possible input and observable property you’d need formal verification. The pragmatic combination — parametrized examples + property tests + mutation testing — is the strongest practical evidence available.

4. Suppose someone implements transfer(savings_src, savings_dst, amount) where savings_src.balance decreases twice after the call. The caller satisfied every documented precondition. Who violated the contract, and what role do SavingsAccount’s extra guarantees play?

The supplier — the postcondition specified exactly one debit. The transactions ledger now also shows the bug as two recorded withdrawals, making the violation easier to detect.
The caller — they should have re-checked the balance afterward.
Callers are not required to re-verify postconditions. That’s what postconditions are for — guarantees the caller can rely on without re-checking.
Both — multi-object operations have shared responsibility.
Shared blame defeats the responsibility allocation. Either the preconditions held (supplier owes) or they didn’t (caller owes).
Neither — total money may still be preserved across the two accounts.
Total preservation is one postcondition; the ‘exactly one debit’ postcondition is another — and it failed.

Valid preconditions shift responsibility to the supplier. A double debit violates the postcondition that source is debited by exactly amount, once. The transactions ledger SavingsAccount adds is also a debugging asset here — it materializes the violation as two recorded withdrawals, where a plain BankAccount would only show the wrong final balance.