An algorithm that "seems to work" is not necessarily correct. To justify correctness we use preconditions, postconditions and loop invariants.

What "correct algorithm" means

An algorithm is correct if, for every input that meets the precondition, it terminates and returns a result that meets the postcondition.

  • Precondition — what holds for the input, for example the list is not empty.
  • Postcondition — what holds for the result, for example best is the largest element of the list.

If the precondition is violated, the algorithm promises nothing: the fault is on the caller's side.

The loop invariant

An invariant is a statement that is true before every iteration of a loop. We check three stages:

  1. Initialization — the invariant is true before the first iteration.
  2. Maintenance — if it is true at the start of an iteration, it is true at the end.
  3. Termination — when the loop ends, the invariant and the exit condition give the postcondition.