Algorithms, invariants and correctness

Which route has fewer arrows?

Six places A,B,C,D,E,F have directed connections A→B, A→C, B→D, D→E, E→F and C→F. Starting at A, you can reach F by A,C,F using two arrows, or by A,B,D,E,F using four. A computer needs precise instructions to find the shorter route, rather than a favourable drawing.

A vertex is a named place; an edge u→v permits a move from u to v. It permits the reverse move only if v→u is also listed. Here every move counts as one edge. Drawing lengths are irrelevant. Our question asks for the fewest edges, not the least travel time or monetary cost.

Prepare the arithmetic and state the contract

Counting, zero and natural numbers prepares finite counts and zero. Addition and subtraction prepares changes in those counts; Multiplication and division prepares equal groups and remainders. Formulas and rearranging simple relationships prepares reading, substitution and retaining an equation’s structure. Graph, queue and proof terms are defined here. On a first reading, follow the division example and search checkpoints; then return to the layer proof and independent certificate.

An algorithm gives precise instructions on declared inputs. Its precondition says which inputs are allowed; its postcondition says what the returned output must satisfy. For integer division, the precondition is an integer n≥0 and an integer divisor d>0. The postcondition is integers q≥0 and r with n=dq+r and 0≤r<d. A different contract could ask a different question of the same numbers.

Partial correctness means: for every input satisfying the precondition, if the algorithm terminates, its result satisfies the postcondition. Total correctness also requires that it terminates for every such input. An algorithm that runs forever does not establish total correctness merely because it never returns a wrong answer.

For our search contract, the graph is finite, each directed edge occurs once, and the source s is an existing vertex. Self-loops u→u are allowed. A route is a finite vertex sequence following the directed edges; it may repeat vertices. Its length is its number of edges, so the route consisting only of s has length zero. A vertex is reachable if such a route starts at s and ends there. We seek all reachable vertices, their minimum edge counts and one minimum route to each.

Write V for the vertex collection and |V| for its count. Write v∈D to mean v belongs to collection D, and D∪P for the vertices belonging to D or P. A graph with no vertices has no valid source for this single-source contract. This is an input exclusion, not a claim that every problem on an empty graph is impossible.

Say when the invariant must hold

A loop repeats its body while a condition, called its guard, is true. A loop invariant is a statement that holds at specified checkpoints: before the first guard test and after each completed iteration, just before the next test. It may fail temporarily between instructions inside the body. The checkpoint must be part of the claim.

Prove three things. Initialization: the starting state satisfies the invariant. Preservation: whenever the invariant and the guard hold, executing the complete body re-establishes it. Exit reasoning: the invariant together with a false guard implies the postcondition. These steps prove partial correctness; termination is a separate obligation.

The always-true statement 1=1 is preserved by every loop, but usually says nothing about its output. An invariant asserting that every reachable vertex has already been found fails at the beginning of most searches. A useful invariant is strong enough for the exit argument and weak enough to hold at every declared checkpoint.

Division keeps the same total

Start q=0 and r=n. While r≥d, replace q by q+1 and r by r−d, then test again. Each completed iteration removes one group of d from the remainder and counts that group in q. For 13 divided by 3, the checkpoint pairs (q,r) are (0,13),(1,10),(2,7),(3,4),(4,1).

The invariant is n=dq+r, with q and r nonnegative integers. Initially n=d·0+n. During an iteration, the new equation is d(q+1)+(r−d)=dq+r=n. The guard r≥d makes the new remainder nonnegative; q+1 remains nonnegative. These are simultaneous mathematical descriptions of the new values, not an instruction to use an already changed r in the first calculation.

At exit the guard is false, so r<d. Together with the invariant this gives exactly n=dq+r and 0≤r<d. The result is unique: if n=dq+r=dq′+r′ with both remainders in that interval, then d(q−q′)=r′−r. The right side lies strictly between −d and d. Its only possible multiple of d is zero, so r=r′ and then q=q′ because d>0.

A decreasing integer proves termination

A variant is a nonnegative integer at each checkpoint that strictly decreases in every guarded iteration. Starting at M, it can decrease strictly at most M times. If the loop were still running after those decreases, another decrease would force a negative value, contradicting the stated bound. This proves termination.

In division, choose r. When the guard holds, r changes to r−d. Since the integer d≥1, it drops by at least one and remains nonnegative. Thus the division loop stops. At n=0 the guard is already false, and the result is q=r=0. With d=0, the remainder would never decrease; that input is excluded by the contract.

Merely nonincreasing is insufficient: an unchanged value can continue forever. A nonnegative real number is insufficient without a suitable discrete lower bound: starting at x=1, the loop while x>0 with x←x/2 never reaches zero in exact arithmetic. These statements concern the mathematical algorithm; rounding or overflow in a particular implementation changes the model and must be checked separately.

Discover once and process in queue order

A queue is an ordered waiting list. First-in, first-out, abbreviated FIFO, removes its oldest entry from the front and adds new entries at the back. Keep a discovered collection D, a processed collection P, a queue Q, distance labels d(v) and parents p(v). A parent records the vertex from which v was first discovered; it is not a claim about every incoming edge.

Initialize D={s}, P empty and Q=[s]. Set d(s)=0 with no parent; all other vertices have no assigned distance or parent. While Q is nonempty, remove its front vertex u. Scan each outgoing edge u→v in the stated inventory order. If v is not in D, immediately add it to D, set d(v)=d(u)+1, set p(v)=u and append v to Q. After all outgoing edges of u have been scanned, add u to P. Only then take the next checkpoint.

Marking v as discovered when it is appended prevents duplicate queue entries, even if two parents point to it before it is processed. On the six-place example, processing A leaves Q=[B,C]; processing B leaves [C,D]; processing C leaves [D,F]. F already has the two-edge parent route A,C,F before the longer branch reaches it.

This is breadth-first search, or BFS. A finite adjacency list is simply the listed outgoing neighbours of one vertex. Scanning it has a definite end because there are finitely many edges. The explorer reports complete iterations, so a removed vertex has joined P before the displayed checkpoint.

Separate discovered, waiting and processed vertices

At each whole-iteration checkpoint, D is the disjoint union of P and the vertices in Q. Each occurs once in its part. The source has distance zero and no parent. Every other discovered vertex has a parent edge from a discovered vertex whose distance is one smaller. Following these parents gives a source route of exactly d(v) edges. Vertices outside D have no assigned label or parent.

Initialization satisfies these statements with only s discovered. Removing u temporarily puts it in neither Q nor P, which is why this invariant is stated at completed iterations. Newly appended vertices were outside D, so remain distinct and receive a genuine edge from u. The already existing parent route to u extends by one edge. Adding u to P restores the disjoint partition.

Every outgoing neighbour of a processed vertex is discovered. This holds initially because P is empty. Scanning u’s complete adjacency list establishes it for u, and discovering more vertices cannot invalidate it for older processed vertices. A self-loop points to an already discovered vertex and creates no new entry.

In FIFO order the queue’s distances are nondecreasing and occupy at most two consecutive levels. Initially the only distance is zero. If the front distance is k, the rest of the queue has distances k or k+1. Newly discovered neighbours receive k+1 and are appended at the back. After removing u, that ordering and two-level bound remain true. Once level k is absent, the next front is level k+1.

Stop after finitely many processed vertices

Queue length is not a decreasing variant: it goes from one to two after processing A. Instead use |V|−|P|. It starts nonnegative and drops by exactly one each iteration, because a queued vertex is not already processed and then joins P. It never becomes negative. Each inner adjacency scan is finite, so the whole search terminates after at most |V| completed iterations.

At exit Q is empty, hence D=P. The processed-neighbour invariant says D is closed under outgoing edges: every edge starting in D also ends in D. Every discovered vertex is reachable by its parent route. Conversely, if a route from s reached a vertex outside D, follow it to its first vertex outside D. The preceding vertex is in D and its outgoing neighbour must be in D, a contradiction. Thus exactly the reachable vertices are discovered.

A cycle causes no infinite repetition because its vertices are discovered once. In A→B→C→A together with D→D, source A reaches A,B,C and leaves D unassigned. The final variant is 4−3=1, not zero: a variant need only decrease while the guard is true. Search may stop earlier because no waiting vertex remains.

FIFO layers give the shortest edge counts

For a reachable vertex v, let δ(v) be the least number of edges in a source route to v. This least integer exists: at least one finite route exists and the nonnegative integers have a least member in every nonempty subset. The recorded parent route gives δ(v)≤d(v). We must prove the reverse inequality, rather than infer it from reachability.

Use successive integer layers. At layer zero, only s has true minimum distance zero, and its label is zero. Suppose all vertices of true distance at most k have been discovered with their exact labels before their layer is processed. FIFO processes every labelled-k vertex before any labelled-(k+1) vertex: labels in the queue are ordered, and processing level k can append only level k+1.

Choose a vertex v with true distance k+1 and a shortest route to it. Its preceding vertex u has true distance k: if u had a shorter route, appending u→v would shorten the route to v. Thus u is processed in level k and the scan either discovers v with label k+1, or finds it already discovered by an earlier processed vertex of label at most k. In the latter case its existing label is at most k+1. Since δ(v)=k+1≤d(v), both cases force d(v)=k+1 before that next layer is processed.

This proves the next layer from the preceding layers. Starting with the base and repeating the step covers every reachable integer distance; this reasoning is called induction. Therefore every final label is a minimum edge count. Different neighbour orders may choose different shortest parents: in A→B,A→C,B→D,C→D, D can have parent B or C, but its distance is always 2.

Check the output without trusting the search trace

A certificate here is an output record that can be checked independently. Give distance labels on a proposed reached collection D and parents there. Require s∈D, d(s)=0, all labels nonnegative integers, and every other vertex of D to have a parent in D with an actual directed parent edge and distance one smaller. Unassigned vertices have no parent. These conditions give a source route of length d(v): following parents strictly lowers a positive integer until the unique distance-zero vertex s.

Also require closure under outgoing edges, and for every edge u→v starting in D require d(v)≤d(u)+1. Closure and the source show that every source route stays in D; the parent routes show every member of D is reachable. Along any route s=v₀,…,v_l=v, repeatedly using the edge inequality gives d(v)≤l. The parent route itself has length d(v), so d(v) is the minimum. These local checks establish the whole output claim.

Completed output certificate

The certificate tests the proposed output, not how it was obtained. It does not assert that the queue discipline was FIFO or that a particular program will terminate. A wrong label, missing reachable vertex or invalid parent can fail a check. Our explorer evaluates the completed output; earlier checkpoints use the search invariant instead.

Changing a condition changes the guarantee

A stack removes the most recently appended entry, called last-in, first-out or LIFO. Process the first listed branch B before C on our six-place graph. First discovery then gives F the parent route A,B,D,E,F of length 4. Later C→F does not replace its label. The route is valid, and every reachable vertex is found, but the required minimum label 2 is missed. In its output, the edge C→F violates d(F)≤d(C)+1 because 4>1+1.

If edge costs differ, BFS still minimizes the number of edges, not the sum of costs. Let A→C cost 9, A→B cost 1 and B→C cost 1. BFS finds the one-edge route A,C, yet the two-edge route A,B,C costs only 2. A different least-cost algorithm requires its own assumptions and proof.

Tests can reveal these counterexamples and check finite models. A collection of successful cases does not replace the initialization, preservation, exit and termination arguments for every valid input. A real implementation also needs its representation and arithmetic to match the stated model. Each reachable vertex is processed once and each outgoing adjacency entry from it is scanned once here; those counts alone do not claim that storing complete teaching snapshots is an efficient implementation.

Worked examples

Try it yourself

1. A program keeps its invariant forever in a loop while true and returns no result. Does its invariant establish total correctness?

   Show the answer and reasoning

   No. Termination is still missing.

   Partial correctness is conditional on returning. Preservation alone cannot prove the program reaches an exit or returns the required output.

2. Apply repeated subtraction to n=10,d=4. Give the complete checkpoint pairs and result.

   Show the answer and reasoning

   (0,10),(1,6),(2,2); quotient 2 and remainder 2.

   Each step preserves 10=4q+r. The remainder drops by 4 while r≥4, then 2<4 ends the loop with 0≤2<4.

3. For n=0,d=5, how many iterations occur and what is returned?

   Show the answer and reasoning

   Zero iterations; q=0,r=0.

   The initial invariant holds and the guard 0≥5 is false. A correct algorithm need not execute its loop even once.

4. Why must d=0 be excluded from this division algorithm?

   Show the answer and reasoning

   The remainder would not decrease, and 0≤r<0 is impossible.

   For n≥0 the guard r≥0 would remain true; updating r to r−0 changes nothing. Both the required remainder interval and the termination proof fail.

5. Does x>0 with x←x/2 terminate from x=1 in exact real arithmetic because x decreases and is nonnegative?

   Show the answer and reasoning

   No; after k iterations x=1/2ᵏ remains positive for every finite k.

   Strict decrease of a real number with lower bound zero allows infinitely many steps. The stated integer-variant proof cannot be applied.

6. After processing A in the six-place BFS, what are the queue length and variant? Why does growth of the queue not contradict termination?

   Show the answer and reasoning

   Queue length 2; variant 6−1=5.

   The queue grew from [A] to [B,C], but exactly one new vertex joined P. The decreasing variant counts vertices not yet processed, rather than waiting vertices.

7. In the diamond, what can go wrong if a vertex is marked discovered only when it is removed from the queue?

   Show the answer and reasoning

   B and C can both append D before D is removed, creating duplicate entries.

   Both incoming scans occur while D is waiting. Marking it on the first append prevents the second append and supports the distinct-queue and termination invariants.

8. What does BFS return for one vertex A with edge A→A and source A?

   Show the answer and reasoning

   Distance 0, no parent and one completed iteration.

   A is discovered at initialization. Its self-loop creates no new entry; processing A empties the queue. The zero-edge route is shorter than using the loop.

9. Can the empty graph be passed to this single-source BFS with source A?

   Show the answer and reasoning

   No. A is not an existing vertex, so the precondition fails.

   There is no source to initialize. This does not exclude an independently specified algorithm that accepts an empty graph and returns an empty all-vertices record.

10. A proposed output has d(A)=0,d(B)=1,d(C)=3 and edges A→B,B→C,A→C. Can it be a valid minimum-distance certificate?

    Show the answer and reasoning

    No. A→C requires d(C)≤1, which fails.

    The edge inequality from A is already enough to reject it; B→C also requires d(C)≤2. The actual minimum distance of C is 1.

11. For costs A→C:9, A→B:1, B→C:1, which route has fewer edges and which has smaller total cost?

    Show the answer and reasoning

    A,C has one edge and cost 9; A,B,C has two edges and cost 2.

    The BFS contract minimizes edge count. It does not minimize unequal costs, so a one-edge answer is correct for one contract and wrong for the other.

12. Must two correct BFS runs with different neighbour orders return identical parents? What must agree?

    Show the answer and reasoning

    Parents need not agree. Reachability and every minimum edge-count label must agree.

    Several routes can have the same minimum length. The diamond supplies two choices for D, both with distance 2. Each valid parent record must still give a minimum route.

What to carry forward

• A contract declares valid inputs and required outputs. Total correctness combines partial correctness with termination.
• State the invariant’s checkpoint, prove initialization and preservation, then combine it with the false guard.
• A nonnegative integer that strictly decreases on every iteration proves termination; an arbitrary decreasing real or an unchanged integer does not.
• Repeated subtraction preserves n=dq+r and returns the unique remainder 0≤r<d for integer n≥0,d>0.
• BFS marks vertices on discovery, processes a FIFO queue and reaches exactly the vertices accessible from its valid source in a finite directed graph.
• The processed count proves termination; FIFO layers prove minimum edge counts. Distinct shortest parents may be equally correct.
• A parent-and-distance certificate checks source routes, closure and edge bounds independently. Unequal edge costs and stack order change the shortest-route guarantee.