Loop Invariant

Why talk about invariant?

When we use a loop (for or while), we often modify variables at each iteration. But certain properties remain true throughout the loop: these are the invariants.

A loop invariant is a logical condition that is true:

before the first iteration of the loop,
at the end of each iteration. This helps understand and prove that the algorithm works correctly.

Example: sum of a list

We want to calculate the sum of elements in a list.

list = [2, 5, 7, 3]
sum = 0
for value in list:
    sum += value

During execution, at each loop turn:

sum contains the sum of already traversed elements of the list.

So, loop invariant:

sum contains the sum of elements in list already seen.

Another example: finding the largest element

list = [6, 4, 9, 1]
maximum = list[0]
for element in list[1:]:
    if element > maximum:
        maximum = element

Here, the invariant is:

maximum contains the largest value among those already traversed.

Why is it useful?

To reason about how a program works.
To verify that an algorithm is correct.
To demonstrate a result in math or computer science (correctness proof).

Invariants are often used in formal proofs, but even without going into proofs, they help better understand the behavior of an algorithm.

Summary

Term	Meaning
Loop invariant	A property that remains true at each loop turn
Before the loop	The invariant is already true before the first iteration
After each iteration	The invariant remains true, even if variables change
Usefulness	Verify logic, fix a bug, or prove that the algorithm works