loopinvarianter

Loopinvarianter are conditions that hold before and after every iteration of a loop. In formal verification they are used to prove that a program meets its specification. A loopinvariant can be seen as a property of the program state that remains true as the loop executes. The formal use typically requires showing three things: initialization (the invariant holds before the first iteration), maintenance (if it holds at the start of an iteration, it also holds after the iteration), and use of the invariant to establish the postcondition when the loop terminates.

Identifying loopinvarianter often starts from the desired postcondition, or by analyzing how the loop state changes. In practice analysts propose candidates and verify them, possibly with systematic methods such as Hoare logic or weakest preconditions. Invariants may be conjunctions of several simpler properties and are often discovered iteratively.

Loop invariants are distinct from loop variants, which are quantities that strictly decrease with each iteration and guarantee termination. Invariants ensure correctness, while variants ensure termination.

Example: Given an array a[0..n-1], computing the sum of its elements with a running total. A loop invariant could be: at the start of each iteration i (0 <= i <= n), total equals sum of a[0..i-1], and 0 <= i <= n. Initially i=0 and total=0, which satisfies the invariant. After processing a[i], i increments to i+1 and total increases by a[i], preserving the invariant. When i reaches n, total equals the sum of all elements, which is the postcondition.

Applications include algorithm verification, compiler optimizations, and formal methods education. Limitations include the difficulty of finding useful invariants for complex loops and the possibility of overly strong invariants restricting correctness proofs.