A Formal Definition

A loop invariant, namely, is a set of conditions that will always hold true if and only if the loop condition holds true. Finding the correct loop invaraint will fundamental to the core proof of the algorithm, function, etc. because of the lovely property of mathematical induction. It has the following properties:

• Initialization: the invariant must hold before loop begins.
• Persistence: the invariant must hold in the loop body.
• Termination*: When the loop ends, the invariant can provide me with meaningful information and the invariant must terminate simultaneously.

A Simple Example

Let us consider a very simple bubble sort algorithm in Rust.

fn bubble_sort<T>(arr: &mut [T]) {
		for i in 0..arr.len() {
				for j in 1..arr.len() {
						if arr[j - 1] > arr[j] {
								std::mem::swap(arr[j - 1], arr[j]);
						}
				}
		}
}

We, of course, want to prove the correctness of the above algorithm. That is, if arr.len() > 1, we have

$$ \forall i \in [0, arr.len() - 1) , arr[i] \leq arr[i + 1]. $$

If we can prove that the sub-slice of arr is correctly sorted during each loop, by mathematical induction, then we can prove the correctness.

Anyway, from observation, we know that during each iteration (outside), the slice arr[len - i..len] must be properly sorted, and that after during each iteration (inside), arr[len-i] is the largest element in the range 0..len-i.