Algorithm Correctness Lab

Retrieval Prompts

1. State the three parts of a loop-invariant proof.
2. State the schema for a recursive correctness proof by strong induction.
3. Define a termination variant and explain what "well-founded" means.
4. Why is testing not a substitute for a correctness proof?
5. What goes wrong in a recursive proof if the inductive hypothesis is assumed only for n - 1 when the function recurses on n / 2?

Compare and Distinguish

Separate these pairs:

• loop invariant versus postcondition
• correctness proof versus termination proof
• strong induction versus ordinary induction
• "the algorithm works" versus "the algorithm terminates"

Common Mistake Check

Identify the error:

1. "My invariant is that the array will be sorted after the loop ends."
2. "I proved correctness by running the algorithm on 50 random inputs and it always worked."
3. "My recursive function calls itself on n - 1 or on n depending on the branch; termination is obvious."
4. "I do not need a base case because the inductive step handles everything."
5. "The loop terminates because the index variable changes every iteration."

Mini Application

Loop invariant proofs

Write a loop invariant, then prove initialization, maintenance, and termination for each:

1. linear_search(A, x): returns an index i with A[i] == x, or -1 if none.

2. max_of(A): returns the maximum element of a non-empty array.

3. The Lomuto partition step:

   def partition(A, lo, hi):
       pivot = A[hi]
       i = lo - 1
       for j in range(lo, hi):
           if A[j] <= pivot:
               i += 1
               A[i], A[j] = A[j], A[i]
       A[i + 1], A[hi] = A[hi], A[i + 1]
       return i + 1

   Invariant should describe A[lo..i], A[i+1..j-1], and A[j..hi-1].

Recursive induction proofs

For each, state the induction hypothesis explicitly and prove the base and inductive steps:

1. power(x, n) computing x^n by x * power(x, n-1), base power(x, 0) = 1.
2. Binary search on a sorted array.
3. Recursive merge_sort (you may assume merge is correct as a lemma).

Termination arguments

Give a decreasing variant and justify well-foundedness:

1. Euclid's gcd(a, b) = gcd(b, a mod b).
2. The recursive merge_sort.
3. A DFS on a finite graph using a visited set.
4. A loop while lo <= hi: in binary search.

Evidence Check

This page is complete only if, for any code you have written this module, you can produce:

• a loop invariant or induction hypothesis in one sentence
• a proof sketch of initialization, maintenance, and termination (or base case and inductive step)
• a termination variant with a written argument for why it strictly decreases