Invariant

Context: FIT1008_MOC, FIT2004_MOC · the correctness-proof tool behind the elementary sorts, Binary Search, Heap · induction over iterations FIT2004 emphasis: correctness is a two-part obligation — termination AND loop invariant — and it is commonly asked in the exam: you are shown an algorithm (usually prose, not code) and asked to explain why it is correct.

Quick Revision

• 🎯 Objective: a property that stays true at a program point / across an algorithm ➔ the rigorous tool for proving correctness and finding optimisations.
• 📦 Core Components: initialization → maintenance → termination (induction over iterations).
• ⚡ Key Constraint: maintenance + termination ⟹ partial correctness; add a variant for total correctness — an algorithm that never halts returns nothing, however good its invariant.

📝 Core

1. The Invariant (A Property Preserved)

• Definition ➔ a property that remains true at a program point or throughout an algorithm; a loop invariant holds before the loop, is preserved by every iteration, and therefore still holds at exit.
• Payoff ➔ anything provably always-true can be exploited to skip work ➔ the basis of every correctness proof.
• Why prove instead of test ➔ testing cannot cover the input space and field failures are unbounded — Ariane 5 ($\approx 7$ billion USD, bad velocity conversion), the Patriot battery that missed a Scud (accumulated time-since-boot error, 28 dead). Proof applies at design time, where testing cannot reach.

2. The Three-Part Proof

• Initialization ➔ $P$ holds before the first iteration · Maintenance ➔ $P$ before ⟹ $P$ after each iteration · Termination ➔ loop ends + negated guard ⟹ postcondition.
• Total correctness ➔ maintenance + termination give partial; a variant (non-negative integer measure strictly decreasing, e.g. end - start) proves halting ⟹ total.

3. Termination — the Co-Equal Obligation

• The three-line template ➔ (i) the domain is finite · (ii) the counter starts at a known point · (iii) every iteration moves it monotonically toward the bound ⟹ the guard fails after finitely many steps.
• find_min worked ➔ array is finite · index starts at $1$ · each iteration does index += 1 ⟹ index reaches len(array) and the while exits.
• Say WHERE you are quoting it ➔ an invariant may be stated at the start or the end of an iteration and the two differ by one index — find_min reads naturally at the start (min $=\min ($A[1…i-1]$)$), Linear Search at the end (index $=$ the last match in A[1…i]). Unstated, the maintenance step cannot be checked.
• Failure is not exotic ➔ Binary Search written with lo = mid and while lo < hi does not terminate at $lo=5,hi=6$: $mid=5$, so the assignment is a no-op and no measure decreases.

4. Design Order — Invariant First, Then Code

• Reverse the usual order ➔ (1) define the invariant needed at exit, (2) write the loop that maintains it. Code written to a stated invariant is correct by construction; one reverse-engineered from finished code usually just paraphrases the code.
• Keep it minimal ➔ the invariant only has to be strong enough to imply the postcondition at exit; extra clauses are extra proof burden with no marks attached.
• Exam shape ➔ “(1 mark) Write a loop invariant for the Floyd–Warshall algorithm that can be used to show it correctly computes all-pairs shortest distances.” — one sentence, quantified over the loop counter, that becomes the postcondition when the counter hits its bound.

⚖️ Core Decision Matrix

Algorithm	Key loop invariant	Termination argument	What it enables
find_min	my_min holds the minimum of array[0…index]	finite array; index starts at $1$ and increments	at exit index $=N$ ⟹ global minimum
Bubble Sort	after pass $i$, the $i$ largest are final at the tail	outer counter shrinks by $1$ per pass	early-exit ($O(n)$ best)
Selection Sort	my_list[0…i-1] is sorted AND $\le$ every element of my_list[i…N]	both $i$ and $j$ only increment and reach the end	prefix is final ⟹ correctness; blocks adaptivity
Insertion Sort	my_list[0…i-1] sorted, not necessarily final	i increments; inner j strictly decreases, bounded below by $0$	incremental inserts
Binary Search	if the key exists in array[0…N] it exists in array[lo…hi]	hi - lo must strictly shrink — the bug vector	shrink-by-half correctness
Linear Search (no early exit)	at the end of iteration $i$: index $=$ the largest $j\le i$ with A[j] = target, else null	i runs $1\to n$ over a finite array	at $i=n$ the invariant is the postcondition ⟹ returns the last occurrence
Heap	every node $\ge$ its children	sift index halves / doubles toward a bound	$O(\log n)$ get_max
Linear Probing	key with hash $N$ sits between $N$ and first empty slot	probe count bounded by table size	search/delete correctness

When It Flips: the strength of the invariant, not the code, decides what optimisations are legal — selection sort's final prefix forbids the incremental insert that insertion sort's sorted-not-final prefix permits. Class invariants generalise the idea to objects (a CircularQueue's front/rear/count consistency). Invariants prove correctness; asymptotic analysis proves cost.

📊 Exam Execution Trace

Applied Exercise

Problem: Show the invariant method is induction over iterations, and that termination is a separate obligation.

$$\begin{array}{rl}\text{base}(\text{initialization})& :P\text{ holds before iteration }1\\ \text{step}(\text{maintenance})& :P\text{ before iter }k\Rightarrow P\text{ before iter }k+1\\ \text{variant}(\text{termination})& :V_k\in \mathbb{N},V_{k+1}<V_k\Rightarrow \text{finitely many iterations}\\ P\wedge \neg \text{guard}& \Rightarrow \text{postcondition}\text{(total correctness)}\end{array}$$

Final Extracted Output: initialization = base case, maintenance = inductive step, variant = the well-ordering argument that the induction actually reaches its last step.

⚠️ Common Mistakes

• 💡 Invariant ≠ termination ➔ it proves correctness if the loop halts; you still need a separate variant for total correctness.
• 💡 “Eventually they meet” is not a termination proof ➔ name the measure and show it strictly decreases; a move that can leave the measure unchanged (lo = mid) is exactly where infinite loops live.
• 💡 Choosing an invariant that does not match the code’s behaviour ➔ Linear Search without an early return keeps overwriting index, so “index is the first match” is false; the true invariant names the largest $j\le i$.
• 💡 Restating the code as the invariant ➔ “i increases each iteration” is a fact about the loop, not a property implying the postcondition; the invariant must mention the data, not just the counter.

🧠 Active Recall

State the three obligations of a loop-invariant proof and which combination gives total vs partial correctness — and how they map onto induction.

• Hint: Partial vs total; induction over the iteration counter.

Answer

• Short answer: initialization + maintenance + termination; maintenance + termination = partial, add a decreasing non-negative variant for total.
• Why: Discrete index ➔ initialization is the base case and maintenance the inductive step, so the property holds at every iteration reached; the variant is what proves the last one is reached.

Why is the difference between selection and insertion sort's invariants algorithmically significant?

• Hint: Invariant strength gates optimisation.

Answer

• Short answer: selection’s prefix is sorted and final — it also dominates the whole suffix — while insertion’s is “sorted but not final”.
• Why: Sound optimisations ➔ the weaker invariant makes insertion sort incremental/online; the stronger one forbids it, because a later element can never be admitted into a prefix already declared final.

You are shown an algorithm in prose and asked "explain why it is correct" for 2 marks. What exactly do you write?

• Hint: Two obligations, one sentence each.

Answer

• Short answer: (1) the loop invariant, quantified over the counter; (2) the termination argument naming the measure that strictly decreases; then one line showing invariant $\wedge$ exit condition $\Rightarrow$ the required postcondition.
• Why: Marks track obligations ➔ an invariant with no termination argument proves only partial correctness, and a termination argument with no invariant proves only that the algorithm stops — possibly with the wrong answer.