Learning Objectives

• Define preconditions, postconditions, and specifications for methods.
• Distinguish partial correctness from total correctness.
• Write Hoare triples $\{P\}\ C\ \{Q\}$.
• Encode pre/postconditions in Java using assertions and documentation.
• Connect specifications to Module 3's logical reasoning and Design by Contract.

Concept Overview

What Is a Specification?

A specification describes what a method does without saying how. It consists of:

• Precondition ($P$): What must be true before the method executes.
• Postcondition ($Q$): What will be true after the method executes (assuming the precondition held).

Hoare Triples

A Hoare triple $\{P\}\ C\ \{Q\}$ means:

If $P$ holds before executing $C$, and $C$ terminates, then $Q$ holds afterward.

This is partial correctness. Total correctness additionally requires that $C$ terminates whenever $P$ holds. We write $[P]\ C\ [Q]$ for total correctness (some notations use curly braces for both).

Examples of Specifications

Partial vs Total Correctness

• Partial correctness: If the program terminates, the result is correct.
• Total correctness: The program always terminates and the result is correct.

Total correctness = partial correctness + termination.

Design by Contract

Bertrand Meyer (1986) formalized this as Design by Contract (DbC):

• The caller is responsible for satisfying preconditions.
• The method is responsible for establishing postconditions.
• Class invariants must hold before and after every public method.

Formal Notation

Worked Examples

Example 1: Maximum of an Array

Specification:

requires: a.length >= 1
ensures:  result == max element of a

Hoare triple: $\{a.\text{length} \geq 1\}\ \texttt{max(a)}\ \{r = \max(a)\}$

Java implementation with assertions:

public static int max(int[] a) {
    assert a.length >= 1 : "Precondition: non-empty array";
    int result = a[0];
    for (int i = 1; i < a.length; i++) {
        if (a[i] > result) result = a[i];
    }
    // Postcondition: result is the maximum
    return result;
}

Correctness argument: The loop invariant is "result = max(a[0..i-1])." After the loop, $i = a.\text{length}$, so result = max(a[0..n-1]).

Example 2: Array Contains

Specification:

requires: a is not null
ensures:  result == true iff x appears in a

public static boolean contains(int[] a, int x) {
    assert a != null : "Precondition: array not null";
    for (int i = 0; i < a.length; i++) {
        if (a[i] == x) return true;
    }
    return false;
}

Loop invariant: At the start of iteration $i$: $x \notin \{a[0], \ldots, a[i-1]\}$.

Example 3: Count Occurrences

requires: a is not null
ensures:  result == |{i : 0 <= i < a.length and a[i] == x}|

public static int countOccurrences(int[] a, int x) {
    assert a != null;
    int count = 0;
    for (int i = 0; i < a.length; i++) {
        if (a[i] == x) count++;
    }
    return count;
}

Loop invariant: count = $|\{j : 0 \leq j < i \text{ and } a[j] = x\}|$.

Example 4: GCD Specification

requires: a >= 0 and b > 0
ensures:  result == gcd(a, b) and result > 0

public static int gcd(int a, int b) {
    assert a >= 0 && b > 0 : "Precondition";
    while (b != 0) {
        int r = a % b;
        a = b;
        b = r;
    }
    return a;
}

Invariant: $\gcd(\text{original } a, \text{original } b) = \gcd(a, b)$ at each iteration. (From Module 1!)

Example 5: Factorial

requires: n >= 0
ensures:  result == n!

public static long factorial(int n) {
    assert n >= 0 : "Precondition: non-negative";
    long result = 1;
    for (int i = 2; i <= n; i++) {
        result *= i;
    }
    return result;
}

Loop invariant: At the start of iteration $i$: result = $(i-1)!$.

Proof Techniques Spotlight

Proving Partial Correctness with Hoare Logic

To prove $\{P\}\ C\ \{Q\}$:

1. Identify the invariant $I$ for each loop.
2. Initialization: Show $P \Rightarrow I$ before the loop starts.
3. Maintenance: Show $\{I \wedge \text{guard}\}\ \text{body}\ \{I\}$ — the invariant is preserved.
4. Termination: When the loop guard is false, show $I \wedge \neg\text{guard} \Rightarrow Q$.

This mirrors mathematical induction (Module 6):

• Initialization = base case
• Maintenance = inductive step
• Termination = final conclusion

Sequential Composition Rule

Chain method calls: the postcondition of the first becomes the precondition of the second.

Java Deep Dive

import java.util.*;

public class SpecificationLibrary {

    // --- max with full specification ---

    /**
     * @requires a.length >= 1
     * @ensures result == maximum element of a
     */
    public static int max(int[] a) {
        assert a != null && a.length >= 1 : "Pre: non-empty array";
        int result = a[0];
        // Invariant: result == max(a[0..i-1])
        for (int i = 1; i < a.length; i++) {
            if (a[i] > result) result = a[i];
            // Invariant maintained: result == max(a[0..i])
        }
        // Post: result == max(a[0..n-1])
        return result;
    }

    // --- contains with specification ---

    /**
     * @requires a != null
     * @ensures result == true iff x is in a
     */
    public static boolean contains(int[] a, int x) {
        assert a != null : "Pre: non-null array";
        // Invariant: x not in a[0..i-1]
        for (int i = 0; i < a.length; i++) {
            if (a[i] == x) return true;
        }
        // Post: x not in a[0..n-1], so result = false
        return false;
    }

    // --- countOccurrences ---

    /**
     * @requires a != null
     * @ensures result == number of times x appears in a
     */
    public static int countOccurrences(int[] a, int x) {
        assert a != null;
        int count = 0;
        // Invariant: count == |{j : 0 <= j < i, a[j] == x}|
        for (int i = 0; i < a.length; i++) {
            if (a[i] == x) count++;
        }
        return count;
    }

    // --- isSorted ---

    /**
     * @requires a != null
     * @ensures result == true iff a is sorted in non-decreasing order
     */
    public static boolean isSorted(int[] a) {
        assert a != null;
        // Invariant: a[0..i-1] is sorted
        for (int i = 1; i < a.length; i++) {
            if (a[i] < a[i - 1]) return false;
        }
        return true;
    }

    // --- sum ---

    /**
     * @requires a != null
     * @ensures result == sum of all elements in a
     */
    public static long sum(int[] a) {
        assert a != null;
        long result = 0;
        // Invariant: result == sum(a[0..i-1])
        for (int i = 0; i < a.length; i++) {
            result += a[i];
        }
        return result;
    }

    // --- indexOf ---

    /**
     * @requires a != null
     * @ensures result == first index where a[result]==x, or -1 if not found
     */
    public static int indexOf(int[] a, int x) {
        assert a != null;
        // Invariant: x not in a[0..i-1]
        for (int i = 0; i < a.length; i++) {
            if (a[i] == x) return i;
        }
        return -1;
    }

    // --- Verification harness: check postconditions at runtime ---

    public static void verifyMax(int[] a) {
        int result = max(a);
        // Check postcondition
        for (int x : a) assert result >= x : "max is not >= all elements";
        boolean found = false;
        for (int x : a) if (x == result) found = true;
        assert found : "max is not in the array";
        System.out.println("max(" + Arrays.toString(a) + ") = " + result + " ✓");
    }

    public static void verifyContains(int[] a, int x, boolean expected) {
        boolean result = contains(a, x);
        assert result == expected : "contains mismatch";
        System.out.println("contains(" + Arrays.toString(a) + ", " + x + ") = "
                + result + " ✓");
    }

    // --- Demo ---

    public static void main(String[] args) {
        System.out.println("=== Specification Library ===\n");

        // Verify max
        verifyMax(new int[]{3, 7, 1, 9, 4});
        verifyMax(new int[]{-5, -2, -8});
        verifyMax(new int[]{42});

        // Verify contains
        verifyContains(new int[]{3, 7, 1, 9, 4}, 7, true);
        verifyContains(new int[]{3, 7, 1, 9, 4}, 5, false);

        // Count occurrences
        int[] data = {1, 2, 3, 2, 1, 2};
        System.out.println("\ncountOccurrences(" + Arrays.toString(data) + ", 2) = "
                + countOccurrences(data, 2));

        // isSorted
        System.out.println("isSorted([1,2,3,4]) = " + isSorted(new int[]{1, 2, 3, 4}));
        System.out.println("isSorted([1,3,2,4]) = " + isSorted(new int[]{1, 3, 2, 4}));

        // sum
        System.out.println("sum([1,2,3,4,5]) = " + sum(new int[]{1, 2, 3, 4, 5}));

        // indexOf
        System.out.println("indexOf([10,20,30], 20) = " + indexOf(new int[]{10, 20, 30}, 20));
        System.out.println("indexOf([10,20,30], 40) = " + indexOf(new int[]{10, 20, 30}, 40));
    }
}

Historical Context

C.A.R. Hoare (1969) published "An Axiomatic Basis for Computer Programming," introducing Hoare logic — a formal system for reasoning about program correctness using triples $\{P\}\ C\ \{Q\}$.

Edsger W. Dijkstra later developed weakest precondition calculus (1975), which computes the weakest precondition $\text{wp}(C, Q)$ such that executing $C$ establishes $Q$.

Bertrand Meyer (1986) coined Design by Contract with the Eiffel programming language, embedding preconditions and postconditions directly into code.

Java's assert statement (added in Java 1.4) and tools like JML (Java Modeling Language) bring these ideas into practice.

Slide-Ready Problem Sets

Slide Set A: Conceptual Questions

A1. What is the difference between a precondition and a postcondition?

A2. Explain partial correctness vs total correctness with an example.

A3. Write a Hoare triple for int abs(int x).

A4. How does a specification differ from an implementation?

Slide Set B: Proof Problems

B1. Given method max(int[] a), state the loop invariant and prove initialization, maintenance, and termination.

B2. Prove partial correctness of contains(int[] a, int x) using a loop invariant.

B3. Write a Hoare triple for sequential composition: int m = max(a); boolean b = contains(a, m);. What does the combined postcondition guarantee?

Slide Set C: Java Coding Problems

C1. Implement countOccurrences(int[] a, int x) with documented preconditions, postconditions, and a loop invariant.

C2. Implement isSorted(int[] a) and write a verification harness that checks the postcondition.

C3. Add assert statements to an existing method to enforce its preconditions. Test that violations are caught.

Full Problem Set

Discrete Math Problems

DM1. Write a Hoare triple for each:

(a) int min(int[] a) (b) boolean allPositive(int[] a) (c) int gcd(int a, int b)

DM2. Prove: if $\{P\}\ C_1\ \{R\}$ and $\{R\}\ C_2\ \{Q\}$, then $\{P\}\ C_1; C_2\ \{Q\}$ (sequential composition rule).

DM3. A method has precondition $x > 0$ and postcondition $r > 0$. The body is r = x * x. Prove the Hoare triple.

DM4. Define what it means for a loop invariant to be inductive. Explain the analogy with mathematical induction (Module 6).

DM5. If a method is partially correct but not totally correct, give a concrete example showing what can go wrong.

Java Programming Problems

JP1. Implement int min(int[] a) with @requires, @ensures, loop invariant, and runtime assertion checks.

JP2. Implement int secondMax(int[] a) where a.length >= 2. State the loop invariant. Verify the postcondition.

JP3. Implement boolean isPalindrome(String s). Write the specification and loop invariant.

JP4. Write a verification harness that tests countOccurrences against a brute-force oracle.

JP5. Implement int[] reverseArray(int[] a). Precondition: a != null. Postcondition: result[i] == a[n-1-i] for all $i$.

Bridge Problems

BR1. Module 3 introduced Hoare triples informally. Now formalize: rewrite three method specs from Module 3's lab using $\{P\}\ C\ \{Q\}$ notation.

BR2. Module 1's GCD method has invariant $\gcd(a_{\text{orig}}, b_{\text{orig}}) = \gcd(a, b)$. Show that this is exactly a Hoare-logic loop invariant. State initialization, maintenance, and termination.

Solutions

Discrete Math Solutions

DM1.

(a) $\{a.\text{length} \geq 1\}\ \texttt{min(a)}\ \{r \leq a[i] \text{ for all } i \text{ and } r \in a\}$

(b) $\{a \neq \text{null}\}\ \texttt{allPositive(a)}\ \{r \Leftrightarrow \forall i \in [0, a.\text{length}): a[i] > 0\}$

(c) $\{a \geq 0 \wedge b > 0\}\ \texttt{gcd(a,b)}\ \{r = \gcd(a,b)\}$

DM3. Assume $x > 0$. The body sets $r = x^2$. Since $x > 0$, $x^2 > 0$, so $r > 0$. $\blacksquare$

DM4. A loop invariant $I$ is inductive if:

1. $I$ holds before the first iteration (initialization = base case).
2. If $I$ holds before an iteration and the guard is true, then $I$ holds after (maintenance = inductive step).
3. When the guard becomes false, $I$ implies the postcondition (conclusion).

This exactly mirrors induction: base case, inductive step, and final conclusion.

DM5. Consider: while (true) { } with precondition true and postcondition true. Partially correct (vacuously — it never terminates), but not totally correct.

Java Solutions

JP2:

public static int secondMax(int[] a) {
    assert a.length >= 2;
    int max1 = Math.max(a[0], a[1]);
    int max2 = Math.min(a[0], a[1]);
    // Invariant: max1 >= max2, and max1,max2 are the
    // two largest values in a[0..i-1]
    for (int i = 2; i < a.length; i++) {
        if (a[i] > max1) {
            max2 = max1;
            max1 = a[i];
        } else if (a[i] > max2) {
            max2 = a[i];
        }
    }
    return max2;
}

Learning Objectives

• Define and identify loop invariants for iterative algorithms.
• Prove initialization, maintenance, and termination for loop invariants.
• Apply loop invariants to binary search, selection sort, and insertion sort.
• Annotate Java code with invariant assertions.
• Connect loop invariants to mathematical induction (Module 6).

Concept Overview

What Is a Loop Invariant?

A loop invariant is a condition that:

1. Is true before the first iteration (initialization).
2. Remains true after each iteration (maintenance).
3. Combined with the loop's exit condition, implies the postcondition (termination).

The Three Steps

Why Invariants Matter

Invariants capture what progress the loop has made. They are the bridge between the precondition and the postcondition.

Formal Notation

For a loop while (B) { S; } with invariant $I$:

This is the Hoare loop rule.

Worked Examples

Example 1: Linear Search

public static int linearSearch(int[] a, int key) {
    for (int i = 0; i < a.length; i++) {
        if (a[i] == key) return i;
    }
    return -1;
}

Invariant: At the start of iteration $i$: $\texttt{key} \notin \{a[0], \ldots, a[i-1]\}$.

• Initialization: $i = 0$, the set $\{a[0], \ldots, a[-1]\}$ is empty, so $\texttt{key}$ is trivially not in it. ✓
• Maintenance: If $a[i] \neq \texttt{key}$, then $\texttt{key} \notin \{a[0], \ldots, a[i]\}$. ✓
• Termination: If the loop ends without returning, $i = a.\text{length}$, so $\texttt{key} \notin a$, and we return $-1$. ✓

Example 2: Binary Search

public static int binarySearch(int[] a, int key) {
    int lo = 0, hi = a.length - 1;
    while (lo <= hi) {
        int mid = lo + (hi - lo) / 2;  // avoids overflow
        if (a[mid] == key) return mid;
        else if (a[mid] < key) lo = mid + 1;
        else hi = mid - 1;
    }
    return -1;
}

Precondition: a is sorted in non-decreasing order.

Invariant: If key is in a, then key is in a[lo..hi].

• Initialization: $lo = 0$, $hi = n-1$. If key is in a, it's in a[0..n-1]. ✓
• Maintenance:
• If a[mid] < key, then key cannot be in a[lo..mid] (array is sorted), so lo = mid + 1 preserves the invariant.
• If a[mid] > key, then key cannot be in a[mid..hi], so hi = mid - 1 preserves it.
• If a[mid] == key, we return immediately.
• Termination: When lo > hi, the range is empty. Combined with the invariant: if key were in a, it would be in an empty range — contradiction. So key is not in a, and we return $-1$. ✓

Variant function: $hi - lo + 1$ (decreases each iteration, bounded below by 0).

Example 3: Selection Sort

public static void selectionSort(int[] a) {
    for (int i = 0; i < a.length - 1; i++) {
        int minIdx = i;
        for (int j = i + 1; j < a.length; j++) {
            if (a[j] < a[minIdx]) minIdx = j;
        }
        int temp = a[i]; a[i] = a[minIdx]; a[minIdx] = temp;
    }
}

Outer loop invariant: At the start of iteration $i$:

1. $a[0..i-1]$ is sorted.
2. Every element in $a[0..i-1]$ is $\leq$ every element in $a[i..n-1]$.
3. $a[0..i-1]$ contains the $i$ smallest elements of the original array.

Inner loop invariant: $a[\texttt{minIdx}] = \min(a[i..j-1])$.

• Initialization (outer): $i = 0$, $a[0..-1]$ is empty — trivially sorted and minimal. ✓
• Maintenance (outer): After finding the minimum of $a[i..n-1]$ and swapping it to position $i$, the invariant extends to $a[0..i]$. ✓
• Termination (outer): When $i = n-1$, $a[0..n-2]$ is sorted and contains the $n-1$ smallest elements, so $a[n-1]$ is the largest. The entire array is sorted. ✓

Example 4: Insertion Sort

public static void insertionSort(int[] a) {
    for (int i = 1; i < a.length; i++) {
        int key = a[i];
        int j = i - 1;
        while (j >= 0 && a[j] > key) {
            a[j + 1] = a[j];
            j--;
        }
        a[j + 1] = key;
    }
}

Outer loop invariant: At the start of iteration $i$: $a[0..i-1]$ is a sorted permutation of the original first $i$ elements.

• Initialization: $i = 1$, $a[0..0]$ is trivially sorted. ✓
• Maintenance: The inner loop shifts elements right to make room, inserting key in its correct position. After insertion, $a[0..i]$ is sorted. ✓
• Termination: When $i = n$, $a[0..n-1]$ is sorted. ✓

Example 5: Summation

public static long sum(int[] a) {
    long s = 0;
    for (int i = 0; i < a.length; i++) {
        s += a[i];
    }
    return s;
}

Invariant: $s = \sum_{j=0}^{i-1} a[j]$.

• Initialization: $i = 0$, $s = 0 = \sum_{j=0}^{-1} a[j]$. ✓
• Maintenance: $s + a[i] = \sum_{j=0}^{i} a[j]$. ✓
• Termination: $i = n$, $s = \sum_{j=0}^{n-1} a[j]$. ✓

Proof Techniques Spotlight

Finding the Right Invariant

The key insight: the invariant should describe partial progress toward the postcondition.

Strategy: Replace the constant bound in the postcondition with the loop variable.

• Postcondition: "result = max of a[0..n-1]" → Invariant: "result = max of a[0..i-1]"
• Postcondition: "a is sorted" → Invariant: "a[0..i-1] is sorted and minimal"

Invariant + Termination = Correctness

This is the fundamental theorem of loop correctness:

Java Deep Dive

import java.util.*;

public class LoopInvariantLibrary {

    // --- Linear Search with invariant assertions ---

    public static int linearSearch(int[] a, int key) {
        assert a != null;
        for (int i = 0; i < a.length; i++) {
            // Invariant: key not in a[0..i-1]
            if (a[i] == key) return i;
        }
        // Post: key not in a
        return -1;
    }

    // --- Binary Search with invariant assertions ---

    public static int binarySearch(int[] a, int key) {
        assert a != null;
        assert isSorted(a) : "Pre: array must be sorted";
        int lo = 0, hi = a.length - 1;
        // Invariant: if key is in a, then key is in a[lo..hi]
        while (lo <= hi) {
            int mid = lo + (hi - lo) / 2;
            assert lo >= 0 && hi < a.length;
            assert lo <= mid && mid <= hi;
            if (a[mid] == key) return mid;
            else if (a[mid] < key) lo = mid + 1;
            else hi = mid - 1;
        }
        // Post: key not in a
        return -1;
    }

    // --- Selection Sort with invariant assertions ---

    public static void selectionSort(int[] a) {
        assert a != null;
        for (int i = 0; i < a.length - 1; i++) {
            // Invariant: a[0..i-1] sorted and contains smallest i elements
            assert isSortedUpTo(a, i);
            assert allSmallerOrEqual(a, i);

            int minIdx = i;
            for (int j = i + 1; j < a.length; j++) {
                if (a[j] < a[minIdx]) minIdx = j;
            }
            // Inner post: a[minIdx] == min(a[i..n-1])
            int temp = a[i];
            a[i] = a[minIdx];
            a[minIdx] = temp;
        }
        assert isSorted(a) : "Post: array is sorted";
    }

    // --- Insertion Sort with invariant assertions ---

    public static void insertionSort(int[] a) {
        assert a != null;
        for (int i = 1; i < a.length; i++) {
            // Invariant: a[0..i-1] is sorted
            assert isSortedUpTo(a, i);
            int key = a[i];
            int j = i - 1;
            while (j >= 0 && a[j] > key) {
                a[j + 1] = a[j];
                j--;
            }
            a[j + 1] = key;
        }
        assert isSorted(a) : "Post: array is sorted";
    }

    // --- Invariant checker helpers ---

    public static boolean isSorted(int[] a) {
        for (int i = 1; i < a.length; i++) {
            if (a[i] < a[i - 1]) return false;
        }
        return true;
    }

    private static boolean isSortedUpTo(int[] a, int end) {
        for (int i = 1; i < end; i++) {
            if (a[i] < a[i - 1]) return false;
        }
        return true;
    }

    private static boolean allSmallerOrEqual(int[] a, int boundary) {
        for (int i = 0; i < boundary; i++) {
            for (int j = boundary; j < a.length; j++) {
                if (a[i] > a[j]) return false;
            }
        }
        return true;
    }

    // --- Demo ---

    public static void main(String[] args) {
        System.out.println("=== Loop Invariant Library ===\n");

        // Linear search
        int[] data = {5, 3, 8, 1, 9, 2, 7};
        System.out.println("linearSearch(data, 9) = " + linearSearch(data, 9));
        System.out.println("linearSearch(data, 6) = " + linearSearch(data, 6));

        // Binary search (needs sorted array)
        int[] sorted = {1, 3, 5, 7, 9, 11, 13};
        System.out.println("binarySearch(sorted, 7) = " + binarySearch(sorted, 7));
        System.out.println("binarySearch(sorted, 6) = " + binarySearch(sorted, 6));

        // Selection sort
        int[] arr1 = {64, 25, 12, 22, 11};
        selectionSort(arr1);
        System.out.println("selectionSort: " + Arrays.toString(arr1));

        // Insertion sort
        int[] arr2 = {64, 25, 12, 22, 11};
        insertionSort(arr2);
        System.out.println("insertionSort: " + Arrays.toString(arr2));

        // Timing comparison
        Random rng = new Random(42);
        int n = 5000;
        int[] big1 = rng.ints(n, 0, 100000).toArray();
        int[] big2 = Arrays.copyOf(big1, big1.length);

        long start = System.nanoTime();
        selectionSort(big1);
        long selTime = System.nanoTime() - start;

        start = System.nanoTime();
        insertionSort(big2);
        long insTime = System.nanoTime() - start;

        System.out.printf("\nSorting %d elements:%n", n);
        System.out.printf("Selection sort: %,d ns%n", selTime);
        System.out.printf("Insertion sort: %,d ns%n", insTime);
    }
}

Historical Context

Robert W. Floyd (1967) introduced the idea of attaching assertions to program points. Tony Hoare (1969) formalized loop invariants in his axiomatic approach to program correctness.

The use of loop invariants in algorithm textbooks was popularized by Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein (CLRS), who systematically present invariants for every sorting and searching algorithm.

Edsger Dijkstra emphasized that invariants should be discovered simultaneously with the algorithm, not retrofitted: "the invariant is not a property of the loop; it is the core of its design."

Slide-Ready Problem Sets

Slide Set A: Conceptual Questions

A1. What are the three properties of a loop invariant?

A2. State the invariant for binary search and explain why the array must be sorted.

A3. How is the maintenance step of a loop invariant analogous to the inductive step in a proof by induction?

A4. Can a loop have more than one invariant? Give an example.

Slide Set B: Proof Problems

B1. Prove the correctness of selection sort using its loop invariant (all three steps).

B2. Prove the correctness of insertion sort using its loop invariant.

B3. Derive a loop invariant for bubble sort and prove its correctness.

Slide Set C: Java Coding Problems

C1. Implement binary search with assert statements checking the invariant at each iteration.

C2. Implement insertion sort and add assertion-based invariant checking.

C3. Write a method that takes a sorting function and an array, runs the sort, and verifies the postcondition (sorted + permutation of original).

Full Problem Set

Discrete Math Problems

DM1. State the loop invariant for linear search. Prove initialization, maintenance, and that the postcondition follows.

DM2. In binary search, the variant function is $V = hi - lo + 1$. Prove: (a) $V \geq 0$ throughout. (b) $V$ decreases each iteration. (c) When $V < 1$, the loop terminates.

DM3. Selection sort performs $\sum_{i=0}^{n-2}(n-i-1) = \frac{n(n-1)}{2}$ comparisons. Prove this using the summation formula from Module 6.

DM4. Derive the loop invariant for computing the product $\prod_{j=0}^{n-1} a[j]$.

DM5. Prove: if a loop maintains an invariant $I$ and terminates with guard $\neg B$, then $I \wedge \neg B$ holds. Explain why this is the postcondition.

DM6. State invariants for both the inner and outer loops of bubble sort. Prove that after pass $i$, the last $i$ elements are in their final positions.

Java Programming Problems

JP1. Implement selection sort with full invariant assertions (check after each swap that a[0..i] is sorted and minimal).

JP2. Implement binary search. Test with sorted arrays of various sizes. Verify correctness by checking that if binarySearch returns idx >= 0, then a[idx] == key.

JP3. Implement bubble sort with assertions. Count the total comparisons and swaps.

JP4. Write a generic invariant checker: a method checkInvariant(int[] a, int i, Predicate) that asserts the invariant at each step.

JP5. Implement a verified reverseArray method with loop invariant: at step $i$, result[0..i-1] = reverse of a[n-i..n-1].

Bridge Problems

BR1. Module 6: loop invariants mirror induction. Display the parallel explicitly for sum(int[] a): write the induction proof that $s = \sum_{j=0}^{i-1} a[j]$ alongside the loop.

BR2. Module 7: selection sort makes $\frac{n(n-1)}{2}$ comparisons (product rule: the inner loop runs $n-1, n-2, \ldots, 1$ times). Prove this count using Module 7's counting principles.

Solutions

Discrete Math Solutions

DM1. Invariant: key $\notin$ a[0..i-1].

• Init: $i = 0$, a[0..-1] = $\emptyset$. ✓
• Maint: If we don't return, $a[i] \neq$ key, so key $\notin$ a[0..i]. ✓
• Term: $i = n$, key $\notin$ a. Return $-1$. ✓

DM2. (a) $lo \leq hi + 1$ by loop guard, so $V = hi - lo + 1 \geq 0$. (b) Each iteration either increases $lo$ or decreases $hi$ (or both via return), so $V$ decreases by $\geq 1$. (c) When $V < 1$, $hi < lo$, guard fails. ✓

DM3. $\sum_{i=0}^{n-2}(n-1-i) = \sum_{k=1}^{n-1} k = \frac{(n-1)n}{2}$. By Module 6 summation formula. ✓

DM4. Invariant: $p = \prod_{j=0}^{i-1} a[j]$. Init: $p = 1$ (empty product). Maint: $p \cdot a[i] = \prod_{j=0}^{i} a[j]$. Term: $p = \prod_{j=0}^{n-1} a[j]$. ✓

DM6. After pass $i$ of bubble sort, the largest $i$ elements are in positions $a[n-i..n-1]$ and are sorted. The inner loop compares adjacent elements and bubbles the maximum to the end.

Learning Objectives

• Define variant functions (decrementing functions) for loops and recursion.
• Prove termination of iterative and recursive algorithms.
• Combine loop invariants with variant functions to achieve total correctness.
• Apply variant functions to binary search, Euclidean algorithm, and sorting.
• Connect termination to Module 6's well-ordering and recursive descent.

Concept Overview

The Termination Problem

Partial correctness tells us: if the program terminates, the result is correct. But how do we know it terminates? We need a variant function.

Variant Functions

A variant function (or decrementing function, or bound function) is a function $V$ from the program state to the integers such that:

1. $V \geq 0$ whenever the loop guard is true.
2. $V$ decreases by at least 1 with each iteration.

Since $V$ is a non-negative integer that strictly decreases, the loop must terminate in at most $V_0$ iterations (where $V_0$ is the initial value).

Total Correctness

Finding Variant Functions

Formal Notation

Hoare loop rule with termination:

Worked Examples

Example 1: Euclidean Algorithm Termination

public static int gcd(int a, int b) {
    while (b != 0) {
        int r = a % b;
        a = b;
        b = r;
    }
    return a;
}

Variant: $V = b$.

Proof:

1. $V \geq 0$: The loop guard ensures $b \neq 0$, and since we start with $b > 0$ (precondition) and the remainder $r = a \bmod b$ satisfies $0 \leq r < b$, after the swap $b_{\text{new}} = r \geq 0$. Actually when $r = 0$, the loop exits on the next check.
2. $V$ decreases: $b_{\text{new}} = r = a \bmod b < b = V_{\text{old}}$. So $V$ strictly decreases.
3. Bounded below: $V \geq 0$ always (remainders are non-negative).

Therefore the loop terminates. Combined with the invariant $\gcd(a_0, b_0) = \gcd(a, b)$:

Example 2: Binary Search Termination

Variant: $V = hi - lo + 1$.

1. $V \geq 0$: The loop guard is $lo \leq hi$, so $V = hi - lo + 1 \geq 1 > 0$.
2. $V$ decreases: In each iteration:

• If $a[\text{mid}] <$ key: $lo_{\text{new}} = \text{mid} + 1 > lo$, so $V$ decreases.
• If $a[\text{mid}] >$ key: $hi_{\text{new}} = \text{mid} - 1 < hi$, so $V$ decreases.
• If $a[\text{mid}] =$ key: we return (loop exits).

1. Bounded below: $V$ is an integer $\geq 1$ during the loop.

Maximum iterations: $\lfloor \log_2 n \rfloor + 1$, since $V$ halves (approximately) each iteration. $\blacksquare$

Example 3: Selection Sort Termination

Outer variant: $V_{\text{outer}} = n - 1 - i$. Starts at $n - 2$, decreases by 1 each outer iteration.

Inner variant: $V_{\text{inner}} = n - j$. Starts at $n - (i+1)$, decreases by 1 each inner iteration.

Both are non-negative integers that decrease. Total comparisons:

Example 4: Recursive Fibonacci Termination

public static long fib(int n) {
    if (n <= 1) return n;
    return fib(n - 1) + fib(n - 2);
}

Variant: $V(n) = n$.

1. Base case: $n \leq 1$ — no recursive call.
2. Recursive case: calls $\text{fib}(n-1)$ and $\text{fib}(n-2)$. Both arguments are $< n$ and $\geq 0$.
3. By well-ordering of natural numbers, the recursion terminates.

(Note: this proves termination, not efficiency. The time complexity is $O(2^n)$ — exponential!)

Example 5: While Loop with Non-Obvious Variant

public static int mysteryLoop(int n) {
    int x = n;
    int y = 0;
    while (x > 0) {
        x = x - 1;
        y = y + x;
    }
    return y;
}

Variant: $V = x$. Starts at $n$, decreases by 1 each iteration, bounded below by 0.

Invariant: $y = \sum_{k=x}^{n-1} k = \frac{n(n-1)}{2} - \frac{x(x-1)}{2}$.

At termination ($x = 0$): $y = \frac{n(n-1)}{2}$.

Proof Techniques Spotlight

Well-Ordering and Termination

The well-ordering principle (every non-empty set of natural numbers has a least element) is the foundation of termination proofs. A variant function maps program states to $\mathbb{N}$ and establishes that the sequence of states is well-ordered and decreasing — hence finite.

Recursive Termination

For recursive functions, the variant is typically the argument(s):

• Structural recursion on trees: size or height decreases.
• Numerical recursion: argument decreases toward the base case.
• Mutual recursion: use a joint variant function.

Non-Termination Detection

If no variant function exists, the program may not terminate. The classic non-terminating program:

while (true) { } // V = ??? No bounded decreasing quantity

The Halting Problem (Turing, 1936) shows that no algorithm can determine termination for all programs. But for specific programs, we can often find variant functions.

Java Deep Dive

import java.util.*;

public class TerminationLibrary {

    // --- GCD with variant tracking ---

    public static int gcd(int a, int b) {
        assert a >= 0 && b > 0 : "Pre: a >= 0, b > 0";
        int steps = 0;
        System.out.printf("GCD(%d, %d):%n", a, b);
        while (b != 0) {
            int variant = b; // variant function value
            int r = a % b;
            System.out.printf("  step %d: a=%d, b=%d, r=%d, V=%d%n",
                    ++steps, a, b, r, variant);
            a = b;
            b = r;
            assert b < variant : "Variant must decrease";
            assert b >= 0 : "Variant must be non-negative";
        }
        System.out.printf("  Terminated after %d steps. gcd = %d%n", steps, a);
        return a;
    }

    // --- Binary search with variant tracking ---

    public static int binarySearch(int[] arr, int key) {
        assert arr != null;
        int lo = 0, hi = arr.length - 1;
        int steps = 0;
        while (lo <= hi) {
            int variant = hi - lo + 1;
            int mid = lo + (hi - lo) / 2;
            steps++;
            System.out.printf("  step %d: lo=%d, hi=%d, mid=%d, V=%d%n",
                    steps, lo, hi, mid, variant);
            if (arr[mid] == key) {
                System.out.printf("  Found at index %d after %d steps%n", mid, steps);
                return mid;
            } else if (arr[mid] < key) {
                lo = mid + 1;
            } else {
                hi = mid - 1;
            }
            int newVariant = hi - lo + 1;
            assert newVariant < variant : "Variant must decrease";
        }
        System.out.printf("  Not found after %d steps%n", steps);
        return -1;
    }

    // --- Insertion sort with step counting ---

    public static int[] insertionSort(int[] a) {
        int[] arr = Arrays.copyOf(a, a.length);
        int comparisons = 0;
        int shifts = 0;
        for (int i = 1; i < arr.length; i++) {
            int key = arr[i];
            int j = i - 1;
            // Inner variant: j + 1 (decreases each inner step)
            while (j >= 0 && arr[j] > key) {
                arr[j + 1] = arr[j];
                j--;
                comparisons++;
                shifts++;
            }
            comparisons++; // the failing comparison
            arr[j + 1] = key;
        }
        System.out.printf("Insertion sort (%d elements): %d comparisons, %d shifts%n",
                a.length, comparisons, shifts);
        return arr;
    }

    // --- Recursive function with variant ---

    /**
     * Compute n! recursively.
     * Variant: n. Decreases by 1 each call. Base: n <= 1.
     */
    public static long factorialRecursive(int n, int depth) {
        assert n >= 0 : "Variant non-negative";
        System.out.printf("%sV=%d: factorial(%d)%n",
                "  ".repeat(depth), n, n);
        if (n <= 1) return 1;
        return n * factorialRecursive(n - 1, depth + 1);
    }

    // --- Collatz conjecture: no proven variant! ---

    /**
     * Collatz sequence: n -> n/2 if even, 3n+1 if odd.
     * Conjectured to always reach 1, but NOT PROVEN.
     * We cannot give a variant function!
     */
    public static int collatzSteps(int n) {
        assert n >= 1;
        int steps = 0;
        System.out.printf("Collatz(%d): ", n);
        while (n != 1) {
            System.out.printf("%d -> ", n);
            if (n % 2 == 0) n = n / 2;
            else n = 3 * n + 1;
            steps++;
        }
        System.out.printf("1 (%d steps)%n", steps);
        return steps;
    }

    // --- Total correctness proof template ---

    /**
     * Exponentiation by repeated squaring.
     * Pre: n >= 0
     * Post: result == base^exp
     * Invariant: result * base^exp == base_orig^exp_orig
     * Variant: exp
     */
    public static long power(long base, int exp) {
        assert exp >= 0;
        long result = 1;
        long b = base;
        int e = exp;
        // Invariant: result * b^e == base^exp
        while (e > 0) {
            assert e >= 0 : "Variant non-negative";
            if (e % 2 == 1) {
                result *= b;
            }
            b *= b;
            e /= 2;
            // Variant e has decreased (integer division by 2)
        }
        // Post: e == 0, so result * b^0 = result = base^exp
        return result;
    }

    // --- Demo ---

    public static void main(String[] args) {
        System.out.println("=== Termination Library ===\n");

        // GCD with variant tracking
        gcd(1071, 462);    // 5 steps
        System.out.println();
        gcd(610, 377);     // Fibonacci numbers: many steps

        // Binary search with variant
        System.out.println("\n--- Binary Search ---");
        int[] sorted = {2, 5, 8, 12, 16, 23, 38, 56, 72, 91};
        binarySearch(sorted, 23);
        binarySearch(sorted, 50);

        // Insertion sort with step counting
        System.out.println("\n--- Insertion Sort ---");
        int[] data = {64, 25, 12, 22, 11, 90, 45};
        int[] result = insertionSort(data);
        System.out.println("Sorted: " + Arrays.toString(result));

        // Recursive factorial with variant
        System.out.println("\n--- Recursive Factorial ---");
        long fact = factorialRecursive(6, 0);
        System.out.println("6! = " + fact);

        // Collatz: no variant function known!
        System.out.println("\n--- Collatz (no proven termination!) ---");
        collatzSteps(27);

        // Power with variant
        System.out.println("\n--- Power (repeated squaring) ---");
        System.out.println("2^10 = " + power(2, 10));
        System.out.println("3^7 = " + power(3, 7));
    }
}

Historical Context

Alan Turing (1936) proved the Halting Problem is undecidable: no algorithm can determine, for every program and input, whether the program terminates. This means we cannot automate termination proofs in general.

Robert W. Floyd (1967) introduced the use of well-founded orderings (a generalization of variant functions) for proving termination.

Edsger Dijkstra (1976) systematized variant functions (which he called "bound functions") in A Discipline of Programming. His approach: design the invariant and the variant together with the loop.

The Collatz conjecture (1937) — that the sequence $n \to n/2$ (even) or $n \to 3n+1$ (odd) always reaches 1 — remains one of the most famous open problems. No variant function is known!

Slide-Ready Problem Sets

Slide Set A: Conceptual Questions

A1. What is a variant function? What two properties must it have?

A2. Why can't while (true) { } have a variant function?

A3. What is the variant function for binary search? How does it relate to $O(\log n)$ complexity?

A4. Explain the difference between partial correctness and total correctness.

Slide Set B: Proof Problems

B1. Prove that the Euclidean algorithm terminates using $V = b$ as the variant.

B2. Prove termination of insertion sort using appropriate variant functions for both loops.

B3. Provide a variant function for power(base, exp) (repeated squaring). Prove it terminates.

Slide Set C: Java Coding Problems

C1. Add variant-tracking print statements to the GCD algorithm. Run on Fibonacci pairs ($F_{n+1}, F_n$) and observe the number of steps.

C2. Implement the Collatz sequence. Print each step. Try to find a variant function (you won't succeed — this is an open problem!).

C3. Implement repeated squaring for power(base, exp). Assert the variant decreases.

Full Problem Set

Discrete Math Problems

DM1. Define "variant function." State the two conditions it must satisfy.

DM2. Prove the Euclidean algorithm terminates. What is the maximum number of steps for inputs $

DM3. For a while loop with guard $i < n$ and body $i = i + 2$, state a variant function and prove termination. For which starting values of $i$ does it actually terminate?

DM4. Explain why the Halting Problem means we can never have a universal variant-function finder.

DM5. Give an example of a partial correctness proof where the program does not terminate. Is the Hoare triple still valid?

DM6. For repeated squaring: if $e_0$ is the initial exponent, how many iterations until termination? Prove: $\lfloor \log_2 e_0 \rfloor + 1$.

Java Programming Problems

JP1. Implement GCD with step-counting. Test on Fibonacci consecutive pairs ($F_n, F_{n-1}$) for $n = 5, 10, 20, 30$. Report step counts.

JP2. Implement binary search with variant tracking. For an array of size 1,000,000, verify the search takes at most $\lceil \log_2 1{,}000{,}000 \rceil = 20$ steps.

JP3. Implement the Collatz conjecture: print the sequence for $n = 1, ..., 100$. Track the maximum sequence length.

JP4. Write a totalCorrectnessChecker method that, given a sorting function, verifies:

(a) The output is sorted (partial correctness).

(b) The output is a permutation of the input.

(c) The function terminated (trivially true if we got a result).

JP5. Implement repeated squaring with variant assertion. Compute $2^{32}$, $3^{20}$, $7^{15}$ and verify against Math.pow.

Bridge Problems

BR1. Module 6: Prove by strong induction that the Euclidean algorithm terminates. Frame the proof using the well-ordering of $\mathbb{N}$ and connect to the variant function.

BR2. Module 7: The number of iterations of binary search is $\leq \lfloor \log_2 n \rfloor + 1$. This is a counting argument: the range $[lo, hi]$ halves each time. Connect this to the product rule: after $k$ halvings, $n / 2^k \leq 1$, so $k \geq \log_2 n$.

BR3. Module 1: The GCD loop maintains the invariant $\gcd(a_0, b_0) = \gcd(a, b)$ (Module 1, Class 3). The variant $V = b$ proves termination. Together, these give total correctness.

Solutions

Discrete Math Solutions

DM1. A variant function $V: \text{State} \to \mathbb{Z}$ satisfies:

(i) $V \geq 0$ whenever the loop guard is true.

(ii) $V$ strictly decreases each iteration ($V_{\text{after}} < V_{\text{before}}$).

DM2. Variant: $V = b$. $b_{\text{new}} = a \bmod b < b$, so $V$ decreases. Since $V \geq 0$ and is an integer, termination follows. By Lamé's theorem (1844), the Euclidean algorithm on inputs $< n$ takes at most $\lfloor 2.078 \ln n + 0.6723 \rfloor \approx 5 \log_{10} n$ steps. The worst case is consecutive Fibonacci numbers. $\blacksquare$

DM3. Variant: $V = n - i$ (for even $n - i$). The loop increments $i$ by 2 each time. If $(n - i_0)$ is positive and even, the loop terminates in $(n - i_0)/2$ steps. If $(n - i_0)$ is odd, it may skip past (depends on comparison type).

Strictly: for int i = 0; while (i < n) { i += 2; }, the variant is $\lceil (n - i) / 2 \rceil$. The loop terminates for all $n \geq 0$. $\blacksquare$

DM5. The Hoare triple $\{x > 0\}\ \texttt{while(true)\{\}}\ \{x < 0\}$ is valid! Partial correctness is vacuously true: the program never terminates, so the postcondition "holds" trivially (there's no terminating execution to violate it).

DM6. The variant is $e$. Each iteration: $e_{\text{new}} = \lfloor e / 2 \rfloor$. After $k$ iterations: $e_k = \lfloor e_0 / 2^k \rfloor$. The loop exits when $e = 0$: $\lfloor e_0 / 2^k \rfloor = 0 \Leftrightarrow 2^k > e_0 \Leftrightarrow k > \log_2 e_0$. So iterations $= \lfloor \log_2 e_0 \rfloor + 1$. $\blacksquare$