Function Contracts & Invariants — State input/output contracts and invariants for functions - Python

SECTION 1

Historical Context & Motivation

Have you ever used a function written by someone else and had no idea what values you were supposed to pass in, or what you'd get back? Maybe you passed a string where the function expected a number, and the whole program crashed. This frustrating experience is exactly the problem that function contracts were designed to solve. The idea of formally specifying what a function requires and what it guarantees has roots stretching back decades in computer science.

1969 • Hoare Logic

Tony Hoare published a landmark paper introducing Hoare triples, which describe a program's behavior using a precondition, a command, and a postcondition. This laid the mathematical groundwork for reasoning about code correctness.

1986 • Design by Contract

Bertrand Meyer coined the term Design by Contract while creating the Eiffel programming language. He treated the relationship between a function and its caller like a legal agreement—each side has obligations and benefits.

2000s • Assertions in Python

Python adopted the assert statement and docstrings as lightweight tools for expressing contracts. Libraries like icontract later added decorator-based contract enforcement.

2014+ • Type Hints & Modern Contracts

Python 3.5 introduced type hints (PEP 484), giving developers a way to annotate expected input and output types. Combined with docstrings and assertions, modern Python supports expressive contracts without leaving the language.

The core question these milestones address is simple yet powerful: How can we make functions self-documenting so that anyone—including our future selves—knows exactly how to use them correctly? Function contracts and invariants answer that question by turning informal expectations into explicit, checkable agreements.

SECTION 2

Core Principles & Definitions

A function contract is an agreement between the function and its caller. The caller promises to provide valid inputs, and the function promises to return a correct result. If either side breaks the agreement, we know exactly where the bug lives. This idea breaks down into three key parts: preconditions, postconditions, and invariants.

Precondition

A precondition states what must be true before the function runs. It's the caller's responsibility. For example, a square-root function might require that the input is non-negative.

Postcondition

A postcondition states what must be true after the function finishes. It's the function's responsibility. The square-root function guarantees that its result squared equals the original input (within rounding).

Invariant

An invariant is a condition that stays true throughout execution—before, during, and after the function runs. For instance, a bank account's balance should never go negative, no matter which function modifies it.

Type Contract

A type contract specifies the data types a function expects and returns. Python type hints like def add(a: int, b: int) -> int serve as a lightweight type contract.

✦

KEY TAKEAWAY

Think of a function contract like ordering food at a restaurant. You (the caller) must order from the menu (precondition). The kitchen (the function) promises to deliver what you ordered, cooked properly (postcondition). The restaurant's health code (invariant) must hold true the entire time—before, during, and after your meal is prepared. If you order something not on the menu, that's your mistake. If they serve you raw chicken, that's theirs.

SECTION 3

Visual Explanation

The diagram shows the three-part contract: the caller satisfies preconditions (left), the function maintains invariants during execution (center), and the result satisfies postconditions (right). Below, the Python code shows how type hints, assertions, and comments express each part.

Notice how the diagram separates responsibilities. The caller box on the left holds the preconditions—these are promises the caller must keep. The function box in the center is where work happens, and the dashed pink border represents the invariant that must remain true throughout execution. The result box on the right lists postconditions that the function guarantees upon completion. This visual pattern applies to every function you'll ever write.

SECTION 4

How Contracts Work in Python

Three Tools for Expressing Contracts

Python gives you three main tools to express function contracts: type hints, docstrings, and assert statements. Each serves a different purpose, but they work best together. Type hints state the data types expected and returned. Docstrings describe the contract in human-readable language. Assert statements enforce the contract at runtime, crashing the program with a helpful message if something goes wrong.

Type Hints as Contracts

Type hints appear in the function signature and communicate what types the function expects and returns. While Python does not enforce these at runtime by default, tools like mypy can check them before your code runs. The syntax follows a straightforward pattern.

TYPE HINT SYNTAX

def function_name(param₁: Type₁, param₂: Type₂) → ReturnType:

Each parameter is annotated with its expected type using a colon. The return type follows the -> arrow. Common types include int, float, str, bool, and list[int].

Assert Statements for Runtime Checking

An assert statement evaluates a condition, and if that condition is False, it raises an AssertionError with an optional message. You place precondition asserts at the top of the function and postcondition asserts just before the return statement. This gives you a safety net that catches contract violations while your code runs.

ASSERT SYNTAX

assert condition, "Error message describing the violated contract"

If condition evaluates to True, execution continues normally. If False, the program halts and prints the error message, immediately telling you which contract was broken.

Docstrings for Human-Readable Contracts

A docstring is a triple-quoted string placed as the first line inside a function. It describes what the function does, what it expects (preconditions), what it returns (postconditions), and any invariants. The widely-used Google style includes sections for Args, Returns, and Raises. Docstrings don't enforce anything automatically, but they communicate your contract to every developer who reads your code—and you can view them with help(function_name).

SECTION 5

Types of Contracts & Invariants

Not all contracts are created equal. Some are simple type checks, while others express complex relationships between inputs and outputs. Understanding the different categories helps you choose the right level of specificity for each function you write.

The three columns classify contract types: preconditions (what the caller must provide), postconditions (what the function guarantees), and invariants (what remains true throughout). Each row shows a specific sub-type with a Python expression example.

A loop invariant is especially useful when writing loops inside a function. It describes a condition that is true at the start of every iteration. For example, in a function that sums a list, the invariant might be "the variable total holds the sum of all elements processed so far." If you can prove the invariant holds before the loop starts, is maintained by each iteration, and implies correctness when the loop ends, then you've essentially proven your function works.

💡

PRO TIP

Start by writing your contracts in a docstring before you write any code. This forces you to think clearly about what your function should do. Then add assert statements to enforce the most critical conditions. Finally, add type hints to the signature. This "contract-first" approach often prevents bugs before they happen.

SECTION 6

Worked Example

Let's build a function from scratch, specifying its full contract. We'll write a function called calculate_average that computes the arithmetic mean of a list of numbers.

Building a Fully Contracted Function: calculate_average

1
Step 1 — Identify the Contract

Before writing any logic, we determine the contract. Preconditions: The input must be a list of numbers (int or float), and the list must not be empty (to avoid division by zero). Postconditions: The returned value must be a float, and it must be between the minimum and maximum values in the list (inclusive). Invariant: The running total at any point during summation equals the sum of all elements processed so far.

Pre: non-empty list of numbers | Post: min ≤ result ≤ max | Inv: running_sum = Σ processed
2
Step 2 — Write the Signature with Type Hints

We express the type contract in the function signature: def calculate_average(numbers: list[float]) -> float:. This tells anyone reading the code that the function expects a list of floats and returns a float. While Python won't enforce this at runtime, tools like mypy will catch type errors before you run the code.

def calculate_average(numbers: list[float]) -> float:
3
Step 3 — Write the Docstring

Next we add the docstring, spelling out every part of the contract in plain English:"""Calculate the arithmetic mean of a list of numbers. Args: numbers: A non-empty list of numeric values. Returns: The arithmetic mean as a float. Raises: AssertionError: If the list is empty. Contract: Precondition: len(numbers) > 0 Postcondition: min(numbers) <= result <= max(numbers) Invariant: running total equals sum of processed elements """

Complete docstring documenting Args, Returns, Raises, and Contract
4
Step 4 — Add Precondition Assertions

At the top of the function body (after the docstring), we enforce preconditions with assert statements: assert len(numbers) > 0, "Precondition failed: list must not be empty". If someone calls calculate_average([]), the program will immediately crash with a clear message instead of silently returning NaN or causing a ZeroDivisionError.

assert len(numbers) > 0, "Precondition failed: list must not be empty"
5
Step 5 — Implement with Invariant Awareness

Now we write the logic. We initialize total = 0.0 and loop through each number, adding it to total. The loop invariant is that total always equals the sum of elements from index 0 up to the current index. After the loop, we compute result = total / len(numbers).

total = 0.0 for num in numbers: total += num # Invariant: total == sum of elements processed result = total / len(numbers)
6
Step 6 — Add Postcondition Assertions and Return

Before returning, we verify our postconditions: assert min(numbers) <= result <= max(numbers), "Postcondition failed: result out of range". Finally, we return the result. The complete function now communicates its full contract through type hints, a docstring, and runtime assertions.

assert min(numbers) <= result <= max(numbers) return result

SECTION 7

Strengths & Limitations of Contracts

Function contracts are powerful, but like any tool they have trade-offs. Understanding both sides helps you decide how thoroughly to specify contracts in your own projects.

Aspect	Strengths	Limitations
Bug Detection	Assert statements catch violations immediately at the exact line where the contract is broken, making debugging much faster.	Asserts only catch bugs if the code actually runs through the failing path. They don't guarantee full coverage.
Documentation	Contracts serve as living documentation—they describe what the function does and stay in sync with the code because they run with it.	Writing thorough contracts takes extra time upfront. For trivial helper functions, this can feel like over-engineering.
Performance	Contracts add negligible overhead in most applications. Python's `-O` flag can disable asserts in production.	Complex postcondition checks (like verifying a list is sorted) can slow down performance-critical code.
Team Collaboration	Contracts make expectations explicit, so teammates can use your function without reading every line of its implementation.	Type hints and asserts don't replace actual communication. Misunderstood contracts can create a false sense of safety.
Enforcement	Type checkers like mypy can catch type contract violations before the code ever runs, saving debugging time.	Python is dynamically typed, so type hints are not enforced at runtime by default. You need external tools to check them.

Comparing the strengths and limitations of function contracts in Python

✦

KEY TAKEAWAY

Function contracts are like the safety features in a car. Seat belts, airbags, and lane-departure warnings add a small amount of cost and weight, but they dramatically reduce the severity of accidents. You don't remove them just because most drives are uneventful. Similarly, contracts add a small amount of code, but they save enormous debugging time when things go wrong—and they will go wrong.

SECTION 8

Connection to Advanced Concepts

The contract-based thinking you've learned here is a foundation for several advanced topics in software engineering. As you continue studying computer science, you'll encounter these concepts again in more powerful forms.

What You Learned	Advanced Version	What Changes
Type hints (`int`, `str`)	Static type systems (TypeScript, Rust, Haskell)	The compiler refuses to run code that violates type contracts, catching errors at compile time instead of runtime.
Assert statements	Formal verification (Dafny, SPARK)	Mathematical proofs guarantee that contracts hold for all possible inputs, not just the ones you tested.
Docstring contracts	Property-based testing (Hypothesis library)	Automated tools generate thousands of random inputs and verify that postconditions hold for every one.
Loop invariants	Algorithm correctness proofs	In college-level algorithms courses, you formally prove that loop invariants imply the algorithm produces correct results.
Data invariants	Class invariants & OOP design	In object-oriented programming, class invariants ensure that an object is always in a valid state, no matter which methods are called.

How function contracts connect to advanced computer science concepts

The key insight is that the mindset of thinking in contracts matters more than any specific tool. Whether you're writing Python with assert statements or Rust with its type system, the underlying discipline is the same: clearly define what you expect, what you guarantee, and what must always be true. That discipline will serve you in every programming language and every stage of your career.

SECTION 9

Practice Problems

Question 1: CONCEPTUAL

A function called divide(a, b) divides a by b. Identify one precondition and one postcondition for this function. Explain why each is necessary.

Show answer

A critical precondition is that b != 0, because division by zero is undefined and would cause a ZeroDivisionError. This is the caller's responsibility—they must provide a non-zero divisor. A postcondition is that result * b == a (approximately, due to floating-point rounding). This guarantees the function actually performed correct division. If the postcondition fails, the bug is inside the function itself, not in the caller's input.

Question 2: BASIC

Write a complete function signature with type hints and one assert statement for a function called get_letter_grade(score) that takes an integer score (0–100) and returns a string letter grade.

Show answer

The function signature with type hints would be: def get_letter_grade(score: int) -> str:. The precondition assert should be: assert 0 <= score <= 100, "Precondition failed: score must be between 0 and 100". This ensures that only valid percentage scores are accepted. The type hint -> str communicates the postcondition that the function will return a string. You might also add a postcondition assert like assert result in ['A', 'B', 'C', 'D', 'F'] to guarantee the returned grade is one of the valid options.

Question 3: INTERMEDIATE

Consider this function that finds the maximum value in a list:

def find_max(items: list[int]) -> int:
    best = items[0]
    for item in items:
        if item > best:
            best = item
    return best

Write a complete contract for this function including: (a) all preconditions, (b) all postconditions, and (c) the loop invariant. Express each as both English text and a Python assertion.

Show answer

(a) Precondition: The list must not be empty. In Python: assert len(items) > 0, "List must not be empty". This is needed because accessing items[0] on an empty list raises an IndexError. (b) Postconditions: First, the result must be an element of the list: assert result in items. Second, no element in the list is greater than the result: assert all(item <= result for item in items). (c) Loop invariant: At the start of each iteration, best is the largest value among all elements examined so far. In code (conceptually, inside the loop): # best == max(items[:i+1]) where i is the current index.

Question 4: APPLIED

You are writing a function for a student gradebook application: def add_grade(gradebook: dict, student: str, grade: float) -> dict. The gradebook maps student names to lists of grades. Write the full function (with type hints, docstring, precondition asserts, postcondition asserts, and at least one invariant stated in a comment) that adds a new grade to an existing student's record.

Show answer

Here is the complete implementation:

def add_grade(gradebook: dict, student: str, grade: float) -> dict:
    """Add a grade to a student's record.
    
    Args:
        gradebook: Maps student names to lists of grades.
        student: Name of existing student.
        grade: Grade value between 0.0 and 100.0.
    
    Returns:
        The updated gradebook.
    
    Raises:
        AssertionError: If student not found or grade out of range.
    """
    assert student in gradebook, f"Precondition: {student} must exist"
    assert 0.0 <= grade <= 100.0, "Precondition: grade must be 0-100"
    old_count = len(gradebook[student])
    # Invariant: all grades in gradebook are between 0 and 100
    gradebook[student].append(grade)
    assert len(gradebook[student]) == old_count + 1, "Postcondition: one grade added"
    return gradebook

The preconditions verify the student exists and the grade is valid. The postcondition verifies that exactly one grade was added. The invariant (all grades between 0 and 100) is maintained because we checked the new grade before appending it.

Question 5: CRITICAL THINKING

A classmate argues: "Assert statements are useless because Python lets you disable them with the -O flag, so they might not even run in production. We should just use if statements and raise exceptions instead." Write a thoughtful response that (a) acknowledges the valid point, (b) explains when asserts are still valuable, and (c) describes a scenario where raising an exception is better than using an assert.

Show answer

(a) Your classmate has a valid point: asserts can indeed be disabled with python -O, so they shouldn't be used for input validation that must always run (like checking user input from a web form). (b) However, asserts are still valuable as development-time safety nets. They document assumptions, catch programmer mistakes during testing, and serve as executable specifications. When an assert fires, it pinpoints the exact contract that was violated, making debugging much faster than tracing a mysterious wrong answer. They express intent differently than regular if-statements—an assert says 'this should be impossible if the code is correct,' while an if-statement says 'this is an expected scenario we need to handle.' (c) For user-facing input, exceptions are better. For example, if you're writing a function that reads a file path from the user, you should use if not os.path.exists(path): raise FileNotFoundError(...) instead of an assert, because invalid user input is expected, not a programmer error. The rule of thumb: use asserts for conditions that indicate bugs in your code, and exceptions for conditions that indicate problems with external input.

SUMMARY

Lesson Summary

Summary

A function contract is an explicit agreement between a function and its caller, consisting of three parts: preconditions (what the caller must provide), postconditions (what the function guarantees to return), and invariants (conditions that remain true throughout execution). In Python, you express contracts using type hints in the function signature, docstrings for human-readable documentation, and assert statements for runtime enforcement.

Thinking in contracts helps you design better functions, communicate your intentions to teammates, and catch bugs early. The concept traces back to Hoare logic (1969) and Design by Contract (1986), and it connects forward to advanced topics like static type systems, formal verification, and class invariants in object-oriented programming. Whether you write a simple helper function or a complex algorithm, always ask yourself: what are my preconditions, what are my postconditions, and what must always be true?