Loop invariants are properties of the algorithm or structure that are always true at particular points in the program. Within a loop's body these properties may become violated briefly, but the rest of the loop's instructions fix these properties for the next iteration.

Loop invariants are used in an inductive proof to formally validate the "correctness" of an algorithm. For a loop invariant to be used in a proof features of the code being analyzed must be used to demonstrate that any violations of the loop invariant are restored before the next iteration.

Determining the Loop Invariant

To determine the loop invariant we can roughly follow these steps

1. Analyze what the code does
   • Read through the instructions and determine roughly what it's purpose is
2. Start with a concrete example
   • Run through the function with an example input
3. Suppose we pause somewhere in the middle of the loop
   • What can we determine about the state of the local variables

Proving a Loop Invariant

1. Induction variable:
   • Number of times through the loop
2. Base case:
   • Prove the invariant holds before the loop starts
3. Induction hypothesis:
   • Assume the invariant holds before beginning some (unspecified) loop iteration
4. Inductive step:
   • Prove the invariant holds at the end of the iteration, ready for the next iteration
5. Termination:
   • Make sure the invariant implies correctness when the loop ends

Example

int minIndex(vector<int>& arr, int a) {
	int m = a;
	
	for (int i = a+1; i < arr.size(); i++) {
		if (arr[i] < arr[m]) {
			m = i;
		}
	}
	
	return m;
}

Firstly, we can read through the code and see that it only updates m to be the current index if the element at the current index is smaller than the element at the index m. We can roughly determine then that our exampleFunction returns the index smallest element after a, or a if the element at a is the smallest already.

Running through a few examples we can see that m is always the index of the smallest element of the processed array so far.

Loop Invariant: m is the index of the minimum element in the arr[a..i-1] at the start of the iteration i for all

Base Case: i=a+1

• Before the first iteration of the loop, the invariant states that m contains the index of the smallest element of arr[a..a]
• This is set explicitly by the line int m = a;
• Therefore the loop invariant must hold in the base case

Inductive Step: i = k, a + 1 <= k < arr.size()

• Assume the loop invariant holds prior to processing index k, ie. m contains the index of the smallest element of arr[a..k-1]
• Case 1: arr[k] < arr[m]
  • By assumption, arr[k] is smaller than any element of arr[a..k-1]
  • m is set to k, and contains the index of the smallest element of arr[a..k], thus loop invariant holds after processing index k
• Case 2: `arr[k] >= arr[m]
  • By assumption, arr[k] is not smaller than the smallest element of arr[a..k-1]
  • No action is taken, and m contains the index of the smallest element of arr[a..k], thus the loop invariant holds after processing index k

Termination: i=arr.size()

• Invariant property states that m contains the index of the smallest element of arr[a..arr.size()-1]
• This range describes the entire subarray from a to arr.size()-1
• Therefore at termination, m contains the index of the smallest element in the entire subarray
• Since arr.size() is finite, and i increments each iteration towards arr.size() the program must terminate.