Loop Invariants

A loop invariant is an assertion about the loop that is relevant to the purpose of the loop. It is a precise statement, in terms of the loop variables, of what is true before and after each iteration of the loop.

Loop invariants are used to reason about programs formally and to prove their correctness without tracing all the iterations through a loop. If you can establish that an assertion is true the first time the loop is evaluated as well as after each iteration of the loop body, then your assertion is a loop invariant.

Consider the following code segment. Note that count! means the factorial of count.

int factorial (int num){
  int product = 1;
  int count = 0;

  while (count < num){ // invariant: product == count!
    count += 1;
    product *= count;
  }
  return product;
}

Each time that the loop test is evaluated, the value of the variable product is always equal to (count)!. Since 0! = 1 (by definition), this is true the first time the loop test is evaluated as well as after each iteration of the loop body. Since product == count! is true each time the loop test is evaluated, it is the loop invariant—the truth of the statement does not vary or change. Loop invariants are useful in reasoning about the correctness of programs that use loops. Since product == count! is an invariant, and product is returned, we can reason that the factorial method calculates the correct value.