Function Contracts & Invariants — State function contracts (inputs/outputs) and invariants - C Plus Plus

SECTION 1

Historical Context & Motivation

The idea that software components should carry explicit promises about their behavior did not originate with any single programming language — it grew from decades of formal methods research. In the 1960s and 1970s, as programs became too complex for ad hoc testing alone, computer scientists began searching for mathematical tools that could guarantee correctness before a single test was run. The central insight was deceptively simple: if every function declares exactly what it needs (preconditions), what it promises to deliver (postconditions), and what must remain true throughout (invariants), then reasoning about large systems reduces to reasoning about small, composable units.

1969 • Hoare Logic Published

C.A.R. Hoare introduced the Hoare triple {P} C {Q}, giving programs a formal proof framework where P is a precondition, C a command, and Q a postcondition.

1986 • Design by Contract Coined

Bertrand Meyer formalized Design by Contract (DbC) in Eiffel, embedding preconditions, postconditions, and class invariants directly into the language syntax.

1998 • C++98 and the STL Contract Model

The C++ Standard Template Library shipped with implicit contracts: iterators must be valid, ranges must be non-overlapping, comparators must define a strict weak ordering. These were documented in prose, not checked by the compiler.

2015 • C++ Core Guidelines

Bjarne Stroustrup and Herb Sutter published the C++ Core Guidelines, codifying Expects() and Ensures() macros from the Guidelines Support Library (GSL) as idiomatic ways to express contracts.

2026 • C++26 Contracts Proposal

After years of revision, a contracts facility using pre, post, and contract_assert attributes is on track for the C++26 standard, giving the language first-class contract support.

Despite this long history, most C++ code in production today relies on comments, naming conventions, or nothing at all to communicate contracts. This gap between what a function assumes and what a caller provides is the single largest source of undefined behavior in real-world C++ applications. The question this lesson addresses is straightforward: how do we state, check, and enforce the contract of every function we write?

SECTION 2

Core Principles & Definitions

A function contract is the complete specification of the agreement between a function and its callers. It consists of three parts: what must be true when the function is called (preconditions), what must be true when it returns (postconditions), and what must remain true across the function's execution without being violated at any observable point (invariants). Understanding these three pillars is essential for writing robust, self-documenting C++ code that composes safely in large systems.

Preconditions

Constraints on inputs and program state that must hold before the function body executes. Violating a precondition is the caller's fault. Example: a sqrt(x) function requires x >= 0.

Postconditions

Guarantees about the return value and program state that must hold after the function returns. Violating a postcondition is the function's fault. Example: sort(v) guarantees the output is a permutation of the input in non-decreasing order.

Class Invariants

Properties of an object that must hold after construction and after every public method completes. They may be temporarily broken inside a method but must be restored before it returns. Example: a BankAccount always has balance_ >= 0.

Loop Invariants

Conditions that hold at the beginning and end of every iteration of a loop. They bridge preconditions and postconditions by proving that repeated computation converges toward the desired result. They are fundamental in formal verification.

Wide vs. Narrow Contracts

A wide contract function accepts all possible inputs and specifies behavior for each. A narrow contract function has preconditions; calling it with invalid inputs is undefined behavior.

✦

KEY TAKEAWAY

Think of a function contract like a legal contract between a client (the caller) and a service provider (the function). The client agrees to supply valid inputs (preconditions), the service provider agrees to deliver a correct result (postconditions), and both agree on the persistent rules of engagement (invariants). If the client hands over garbage, the provider is not liable for the outcome — that is the essence of undefined behavior from a violated precondition.

SECTION 3

Visual Explanation — Anatomy of a Function Contract

The upper portion shows the flow of data from the caller through the function to the result. Preconditions (yellow) guard the entry, postconditions (green) guard the exit, and invariants (pink) span the lifetime of the object. The lower portion illustrates how a class invariant is established by the constructor, may be temporarily violated inside methods, but must be restored before each method returns.

Notice that the diagram draws a sharp boundary between the caller's responsibilities and the function's responsibilities. This boundary is the contract itself. In C++, unlike in Eiffel, the contract is traditionally implicit — communicated through documentation comments, naming conventions (e.g., noexcept, [[nodiscard]]), and defensive programming with assert(). Modern C++ is moving toward making these contracts explicit through language features and library tools, but the conceptual model remains the same: every function has a contract whether you state it or not, and the only question is whether you make it legible to humans and machines.

SECTION 4

How It Works — Formal Notation and C++ Expression

The formal foundation for function contracts comes from Hoare logic, which gives us a notation for reasoning about program correctness. The Hoare triple relates a precondition P, a command (or function body) C, and a postcondition Q. If P holds before C executes, then Q is guaranteed to hold after C completes. This framework maps directly to how we write contracts in C++.

HOARE TRIPLE

{P} C {Q}

P = precondition (what must be true before execution), C = command or function body, Q = postcondition (what is guaranteed after execution). If P holds and C terminates, then Q holds.

LOOP INVARIANT RULE

{I ∧ B} S {I} ⟹ {I} while(B) S {I ∧ ¬B}

I = loop invariant, B = loop condition, S = loop body. If the invariant and the loop condition together imply the invariant after executing the body, then the loop preserves the invariant, and upon termination (when B is false), both I and ¬B hold.

Expressing Contracts in C++

C++ provides several mechanisms for expressing contracts, ranging from comments to compile-time checks. The most common approach today uses assert() from <cassert> for runtime checks, static_assert() for compile-time checks, and the GSL macros Expects() and Ensures() for semantically clearer precondition and postcondition assertions. The upcoming C++26 contracts facility introduces pre and post attributes directly in function declarations, bringing contracts into the type system.

Mechanism	Syntax Example	When Checked
`assert()`	`assert(n > 0);`	Runtime (debug builds only; removed by `NDEBUG`)
`static_assert()`	`static_assert(sizeof(int) >= 4);`	Compile time
GSL `Expects()`	`Expects(ptr != nullptr);`	Runtime (always, unless configured otherwise)
GSL `Ensures()`	`Ensures(result >= 0);`	Runtime (always, unless configured otherwise)
C++26 `pre/post`	`int f(int x) pre(x > 0) post(r: r >= 0);`	Configurable: ignore, observe, or enforce

C++ contract mechanisms from traditional to modern

CLASS INVARIANT RULE

∀ public method m: {INV ∧ PRE_m} body_m {INV ∧ POST_m}

Every public method of a class must preserve the class invariant: it may assume the invariant on entry (along with its own preconditions) and must re-establish it on exit (along with its postconditions).

SECTION 5

Contract Types and Invariant Classification

Contracts and invariants come in several flavors, each serving a different purpose in the design of correct software. Understanding the taxonomy helps you decide which tools to reach for in different scenarios. A precondition on a free function is fundamentally different from a class invariant on a container, even though both fall under the umbrella of "contracts." Similarly, a representation invariant (constraining private data) differs from an abstraction invariant (constraining the logical model visible to clients).

This taxonomy tree shows how the umbrella concept of a contract decomposes into preconditions, postconditions, and invariants (class, loop, and data structure). The bottom panel contrasts wide and narrow contracts.

The distinction between wide contracts and narrow contracts has practical implications for API design. A function like std::vector::at() has a wide contract: it accepts any index and throws std::out_of_range for invalid ones. In contrast, std::vector::operator[]() has a narrow contract: calling it with an out-of-bounds index is undefined behavior. The C++ Standard Library uses narrow contracts pervasively for performance-critical paths, relying on the caller to satisfy preconditions. This is a deliberate design choice: checking preconditions costs time, and in performance-sensitive code, the contract shifts that responsibility to the caller in exchange for zero overhead.

SECTION 6

Worked Example — Designing a Contract-Rich Class

Let us design a simple BoundedStack<T, N> class — a stack with a compile-time maximum capacity — and systematically identify its preconditions, postconditions, and invariants. This example demonstrates how to translate informal requirements into explicit, checkable contracts.

BoundedStack Contract Specification

1
Step 1 — Identify the Class Invariant

A BoundedStack stores up to N elements. The internal state is an array data_[N] and a count size_. The class invariant is: 0 <= size_ && size_ <= N and elements data_[0..size_-1] are valid, constructed objects of type T.

INV: 0 <= size_ <= N ∧ all data_[0..size_−1] are valid T
2
Step 2 — Specify push() Contract

The push(const T& value) method requires that the stack is not full. Its postcondition guarantees that the new top element equals the pushed value and the size has increased by one. We also assert the invariant holds on exit.

PRE: size_ < N | POST: top() == value && size() == old_size + 1 | INV preserved
3
Step 3 — Specify pop() Contract

The pop() method requires that the stack is non-empty. Its postcondition guarantees that the size has decreased by one. Note that in C++ we typically separate top() (query) from pop() (command) for exception safety — this is itself a contract-driven design decision.

PRE: size_ > 0 | POST: size() == old_size − 1 | INV preserved
4
Step 4 — Write the C++ Code with Contracts

Here is the implementation using GSL-style assertions: template <typename T, std::size_t N> class BoundedStack { std::array<T, N> data_{}; std::size_t size_ = 0; bool check_invariant() const { return size_ <= N; } public: void push(const T& value) { Expects(size_ < N); // precondition data_[size_] = value; ++size_; Ensures(data_[size_ - 1] == value); // postcondition Ensures(check_invariant()); // invariant } void pop() { Expects(size_ > 0); // precondition --size_; Ensures(check_invariant()); // invariant } const T& top() const { Expects(size_ > 0); // precondition return data_[size_ - 1]; } bool empty() const noexcept { return size_ == 0; } // wide contract bool full() const noexcept { return size_ == N; } // wide contract std::size_t size() const noexcept { return size_; } // wide contract };

Every mutating method checks its precondition on entry and asserts the invariant on exit. Query methods (empty(), full(), size()) have wide contracts — they accept any call and return a defined result.
5
Step 5 — Verify the Loop Invariant of a Client

Consider a client that drains the stack: // Loop invariant: all elements above size() have been processed. while (!stack.empty()) { process(stack.top()); stack.pop(); } // Post: stack.size() == 0 The loop invariant here is that at each iteration start, all elements from the original top down to the current size() have been processed. The loop condition !empty() satisfies pop()'s precondition, and termination is guaranteed because size() strictly decreases each iteration.

The client's loop invariant composes with the class contract to guarantee correctness of the drain operation.

SECTION 7

Strengths, Limitations, and Tradeoffs

Like any engineering discipline, enforcing function contracts involves tradeoffs. Runtime assertion checks impose a performance cost; overly restrictive preconditions can reduce API flexibility; and stating invariants formally requires effort that teams may resist. Understanding these tradeoffs helps you calibrate your approach based on the project's risk profile, performance requirements, and team culture.

Aspect	Strengths	Limitations
Bug Detection	Precondition and invariant checks catch contract violations early, often at the exact call site, rather than propagating to distant failures.	Runtime checks only catch violations that are actually executed. They do not prove absence of bugs across all inputs.
Documentation	Contracts serve as machine-readable documentation that stays synchronized with the code — unlike comments, they fail when wrong.	Complex contracts (e.g., "the input graph is a DAG") may be expensive or impossible to check at runtime.
Performance	Narrow contracts allow zero-overhead implementations: if the caller guarantees preconditions, the function skips validation.	Removing assertions in release builds (`NDEBUG`) means production code runs without safety nets; contract violations become UB.
Composability	When every function states its contract, reasoning about chains of calls becomes modular — each link's postcondition feeds the next link's precondition.	Inheritance can weaken contracts: a derived class can strengthen preconditions (violating LSP) if the developer is not careful.
Tooling	Static analyzers, sanitizers, and formal verification tools can leverage declared contracts to prune search spaces and generate targeted tests.	Until C++26 contracts ship widely, the ecosystem is fragmented: GSL, custom macros, and `assert()` each have different semantics and limitations.

Strengths and limitations of explicit function contracts in C++

✦

KEY TAKEAWAY

Contracts are like the specifications on an engineering blueprint: they cost effort to write and review, but they prevent catastrophic failures in the field. An aircraft manufacturer does not skip the load specification on a wing spar to save time — the specification is the engineering. Similarly, in high-reliability C++ code, the contract is not overhead on top of the implementation; it is the design itself.

SECTION 8

Connection to Advanced Theory — Formal Verification and Beyond

The contracts we have discussed so far are lightweight: they are runtime checks that sample correctness at specific program points. Advanced formal methods extend this idea to prove that contracts hold for all possible inputs, not just the ones encountered during testing. Tools like Frama-C (for C), SPARK/Ada, and theorem provers like Coq and Lean take Hoare-style reasoning to its logical conclusion: mathematical proof of total correctness. The Liskov Substitution Principle (LSP) connects contracts to object-oriented design by requiring that subtypes preserve the contracts of their supertypes — specifically, preconditions may be weakened but never strengthened, and postconditions may be strengthened but never weakened.

Feature	Runtime Contracts (this lesson)	Formal Verification (advanced)
Guarantee	Checks hold for executed paths only	Proves contracts hold for all reachable states
Effort	Low — a few lines of assertions per function	High — formal specifications and proof obligations
Expressiveness	Limited to efficiently checkable boolean expressions	Can express quantified properties (∀, ∃), temporal logic, etc.
C++ Support	`assert()`, GSL, C++26 `pre/post`	Limited — research tools like SAW, CBMC, or external verification
Best For	Application and library code where testing suffices	Safety-critical systems (avionics, medical devices, cryptography)

Runtime contracts versus formal verification

As you advance in software engineering, you will encounter systems where runtime contracts are necessary but not sufficient. The skills you are building now — precisely stating what a function requires and guarantees — are the same skills needed to write formal specifications. In that sense, learning to state contracts is the first step on the path from testing-based confidence to proof-based certainty.

SECTION 9

Practice Problems

Question 1: CONCEPTUAL

Explain the difference between a precondition and a postcondition. Who is responsible when a precondition is violated — the caller or the callee? What about a postcondition violation?

Show answer

A precondition is a constraint that must hold before a function begins execution; it defines what the caller must guarantee. A postcondition is a constraint that must hold when the function returns; it defines what the function guarantees to the caller. When a precondition is violated, the fault lies with the caller — the function was invoked incorrectly. When a postcondition is violated, the fault lies with the callee — the function failed to deliver on its promise. This division of responsibility is the core of the contract metaphor and mirrors the legal concept of breach of contract.

Question 2: BASIC APPLICATION

Given the function signature int binary_search(const std::vector<int>& v, int target), state the preconditions and postconditions. Write them using Expects() and Ensures() or C++26 pre/post syntax.

Show answer

The primary precondition is that the vector must be sorted in non-decreasing order: Expects(std::is_sorted(v.begin(), v.end())). The postcondition has two cases: if the return value is not −1, then Ensures(result == -1 || v[result] == target) — either the function signals "not found" or the element at the returned index equals the target. An additional postcondition might assert that result >= -1 && result < static_cast<int>(v.size()). Note that the sortedness precondition is expensive to check (O(n)), which is why std::binary_search in the standard library documents it but does not check it at runtime.

Question 3: INTERMEDIATE

Consider a CircularBuffer<T, N> class with methods enqueue(const T&) and dequeue(). State the class invariant, and for each method, state preconditions and postconditions. Identify whether each method has a wide or narrow contract.

Show answer

The class invariant is: 0 <= count_ <= N and both head_ and tail_ indices are in [0, N), and tail_ == (head_ + count_) % N. For enqueue(): precondition is count_ < N (not full), postcondition is count_ == old_count + 1 and the new tail element equals the enqueued value. This is a narrow contract. For dequeue(): precondition is count_ > 0 (not empty), postcondition is count_ == old_count − 1. Also a narrow contract. Query methods like empty() and full() have wide contracts since they accept all states and return a defined result.

Question 4: APPLIED

You are writing a function std::string format_currency(double amount, int decimal_places) for a financial application. State the complete contract. Then explain why you might prefer a wide contract (returning an error string or throwing) over a narrow contract (UB on invalid inputs) in this domain, referencing the risk profile of financial software.

Show answer

Preconditions: decimal_places >= 0 && decimal_places <= 10 and !std::isnan(amount) && !std::isinf(amount). Postcondition: the returned string is a valid currency representation with exactly decimal_places digits after the decimal point. In financial software, a narrow contract that silently invokes UB on bad input is unacceptable: a corrupted currency display could lead to incorrect transactions, regulatory violations, or loss of funds. A wide contract — throwing std::invalid_argument or returning an error — ensures that every input produces a defined, observable outcome. The performance cost of validation is negligible compared to the risk. This illustrates how the choice between wide and narrow contracts is driven by the domain's tolerance for undefined behavior, not by a universal rule.

Question 5: CRITICAL THINKING

The Liskov Substitution Principle (LSP) imposes constraints on how derived classes may modify contracts. Specifically, a derived class must not strengthen preconditions and must not weaken postconditions. Consider a base class Shape with a virtual method double area() const whose postcondition is result >= 0. A derived class Rectangle adds the postcondition result == width_ * height_. Does Rectangle satisfy LSP? Now suppose a class WeirdShape overrides area() to return negative values for certain inputs. Analyze the LSP violation and explain its consequences for code that depends on the Shape contract.

Show answer

Rectangle satisfies LSP because it strengthens the postcondition: it guarantees everything Shape guarantees (result >= 0) plus an additional constraint (result == width_ * height_). Strengthening postconditions is always safe because any code that relies on the weaker guarantee will also be satisfied by the stronger one. WeirdShape violates LSP because it weakens the postcondition: it no longer guarantees result >= 0 for all inputs. Any client code that calls shape->area() through a Shape* pointer and relies on the non-negativity postcondition — for example, computing sqrt(shape->area()) — will silently produce incorrect results or invoke UB. This demonstrates why contracts and inheritance must be designed together: the base class contract is a promise to all clients, and subtypes must honor it. In practice, this means documenting contracts on virtual functions is even more critical than on non-virtual ones, because the contract constrains an entire hierarchy.

SUMMARY

Summary — Function Contracts & Invariants

Summary

A function contract consists of three components: preconditions that the caller must satisfy before invocation, postconditions that the function guarantees on return, and invariants that must hold at designated program points (after construction, between method calls, at each loop iteration). These concepts trace back to Hoare logic (1969) and were refined by Bertrand Meyer's Design by Contract (1986). In C++, contracts can be expressed using assert(), the GSL's Expects()/Ensures(), or the upcoming C++26 pre/post attributes.

The distinction between wide contracts (which define behavior for all inputs) and narrow contracts (which have preconditions and invoke UB when violated) is central to C++ API design and performance engineering. Class invariants ensure object consistency across their lifetime, while loop invariants bridge preconditions to postconditions through iterative computation. The Liskov Substitution Principle extends contract reasoning to inheritance hierarchies: subtypes may weaken preconditions and strengthen postconditions, but never the reverse. Mastering contracts is the foundation for writing correct, composable, and self-documenting C++ code.