G01: Specifications, invariants, and finite-state checking

Prerequisites and observable goals#

The central question: what must every execution preserve?#

A test is a particular execution. A specification describes permitted executions. An implementation can pass examples while violating an unstated assumption: that inventory never becomes negative, that a rejected transaction has no effect, or that an object remains alive until its last use. Write the objects and the contract before choosing a proof or a test.

For a sequential inventory operation, let the state be $s=(a,b)$, where $a\in\N$ is available stock and $b\in\N$ is sold stock. An order requests $q\in\N$. Our policy is deliberately simple: accept only when $q\le a$; otherwise leave state unchanged. The mathematical transition is

This definition contains an error-handling policy, not merely an arithmetic formula. A policy that partially fills orders is also possible, but it is a different operation. The theorem we want is: starting with $a+b=N$ and nonnegative components, every finite sequence of valid requests preserves $a+b=N$ and nonnegativity.

Assertions and Hoare triples#

An assertion is a predicate on program state: a statement that can be true or false for a particular mapping from variable names to values. The notation

means partial correctness: for any initial state satisfying $P$, if command $C$ terminates normally, its final state satisfies $Q$. $P$ is the precondition and $Q$ the postcondition. It does not, by itself, promise termination or describe exceptions. A total-correctness claim adds termination under the precondition. [G-HOARE]

Consider assignment x=x+1 over mathematical integers. To guarantee $x>5$ afterward, it is sufficient to require $x+1>5$ beforehand, equivalently $x>4$. This backward substitution is the assignment rule: to establish $Q$ after $x:=E$, establish $Q[E/x]$ before. The substitution replaces the variable’s value in the assertion; it does not execute $Q$ as a program. With bounded machine integers, overflow behavior must be added to the model. Python’s arbitrary-precision integers avoid fixed-width wraparound, but memory/time remain finite resources.

For a sequence $C_1;C_2$, find an intermediate assertion $R$: prove $\{P\}C_1\{R\}$ and $\{R\}C_2\{Q\}$. For a conditional, prove each branch under $P$ plus its branch condition. Do not prove only the branch you expect to be common.

Worked proof: sum of squares#

Suppose $n$ is a fixed nonnegative integer and the program is

i = 0
s = 0
while i < n:
    s = s + i*i
    i = i + 1

An invariant true at every loop head is

An empty sum is zero. Initialization establishes $i=0$ and $s=0$. For preservation, assume $I$ and $i<n$ before the body. The first assignment gives $s'=s+i^2=\sum_{k=0}^{i}k^2$. The second gives $i'=i+1$, so $s'=\sum_{k=0}^{i'-1}k^2$ and $0\le i'\le n$. The same assertion is restored, expressed in new state.

At exit, $I$ and $\neg(i<n)$ imply $i=n$, not merely $i\ge n$. Substituting into the sum yields the postcondition $s=\sum_{k=0}^{n-1}k^2$. A separate variant $n-i$ is a nonnegative integer at loop heads and strictly decreases on every executed iteration. Thus the loop terminates in the ideal model. An invariant can be true forever in a nonterminating loop; a decreasing well-founded measure supplies the missing argument.

The closed form $n(n-1)(2n-1)/6$ can be proved by induction, but it is not necessary to prove that the loop computes the specified sum. Keeping the specification as a sum often makes the invariant easier to discover. Prove the closed form separately when it is useful for an oracle or optimization.

Recognition: choose the right evidence#

Use an invariant when the algorithm repeats a step while preserving a relationship. Use structural induction when it traverses a recursively built object. Use a finite-state model when transitions are small enough to enumerate and boundary behavior matters. Use tests to connect that model to the actual implementation. No one method makes the others redundant.

A good invariant is neither only a goal nor only a tautology. “The answer is correct” may be false until completion. “$s$ is an integer” is easy to preserve but too weak to prove the sum. Work backward from the final expression: replace the final bound $n$ with the evolving bound $i$, then add bounds needed for safe indexing and exit reasoning.

An inventory transition proof#

For acceptance, $q\le a$ implies $a-q\ge0$, and $b+q\ge0$ follows from nonnegative inputs. Conservation follows by cancellation:

For rejection, the state is unchanged, so both properties remain true. Induction over the number of requests proves the invariant for every finite sequential request list. This proof is stronger than checking a few orders, but it depends on the transition definition. It does not cover concurrent unsynchronized reads, database failures, or an API allowing a negative request.

Every shown node sums to four. The self-loop is a real transition: an operation can occur without changing inventory. This matters when distinguishing “no effect” from “no request received.”

Finite exploration and its boundary#

The lab explores all reachable states for a fixed initial stock $N$ and request range $0,\ldots,Q$. Breadth-first search stores a set of seen states so zero requests and rejections do not cause endless repetition. With $Q\ge1$, every $(N-b,b)$ for $b=0,\ldots,N$ is reachable by repeatedly ordering one unit. There are $N+1$ states. Each tries $Q+1$ requests, so work is $O((N+1)(Q+1))$ transition evaluations, assuming state hashing and integer arithmetic costs are bounded for this model.

The code rejects negative inputs and Booleans, even though Python treats bool as a subclass of int. This is a deliberate contract choice. The exhaustive exploration establishes properties only of this sequential finite model. To model concurrent check-then-decrement, split the operation into read/check/write transitions and include each thread’s local state; the resulting counterexample is not erased by the sequential proof.

Independent practice#

F foundation C standard course work T transfer S optional stretch L runnable lab or project. Attempt the complete set before opening its solutions.

Smallest useful hints#

For .01, replace the post-state $x$ by the expression used to compute it. For .04, give each buyer its own read value before choosing the writes. For .06, store seen states before enqueueing successors; do not count a repeated state as new work.

Complete solutions: G01#

Compare the first step where your work differs. A corrected answer is not yet an independent success.

Open every solution

"""G01: a finite state model. This is sequential, not a thread model."""
from collections import deque
from dataclasses import dataclass


@dataclass(frozen=True)
class Stock:
    available: int
    sold: int = 0


def reserve(state: Stock, amount: int) -> Stock:
    if any(type(x) is not int or x < 0
           for x in (state.available, state.sold, amount)):
        raise ValueError("nonnegative mathematical integers required")
    if amount > state.available:
        return state
    return Stock(state.available - amount, state.sold + amount)


def explore(initial: int, max_amount: int = 4) -> set[Stock]:
    if (type(initial) is not int or not 0 <= initial <= 100
            or type(max_amount) is not int or not 0 <= max_amount <= 100):
        raise ValueError("finite model bounds must be integers in [0,100]")
    start = Stock(initial)
    seen, todo = {start}, deque([start])
    while todo:
        state = todo.popleft()
        for amount in range(max_amount + 1):
            nxt = reserve(state, amount)
            if nxt.available < 0 or nxt.available + nxt.sold != initial:
                raise AssertionError((state, amount, nxt))
            if nxt not in seen:
                seen.add(nxt)
                todo.append(nxt)
    return seen


if __name__ == "__main__":
    print(sorted(explore(4), key=lambda s: s.sold))

Retention and readiness#

Explain why the proof needs both branches, why zero requests do not break exploration, and why this is not a concurrency proof. Revisit implication and induction if those explanations fail. Advance when you can modify the policy, repair the proof, and change tests consistently without viewing the solution. Continue with Hoare logic in Software Foundations for mechanized proof practice; this chapter’s handwritten arguments are not machine-checked proofs. [G-HOARE]