Loop Invariant

A loop invariant is a logical assertion about a program’s state that holds whenever execution reaches a designated point in a loop, usually immediately before the loop condition is evaluated. It expresses a relationship that successive iterations preserve, even though individual variables may change. Loop invariants are used to establish the correctness of algorithms and to support formal verification of programs. An invariant need not remain true at every intermediate statement within the loop body. (cs.cornell.edu)

Definition and proof obligations

For a loop of the form

while B:
    C

let $B$ be the loop condition, or guard, $C$ the body, and $I$ a proposed invariant. Establishing a correctness argument requires three obligations:

1. Initialization: the state immediately before the first condition test satisfies $I$.
2. Preservation: if $I$ and $B$ hold before an iteration, executing $C$ reestablishes $I$, provided that execution finishes normally.
3. Exit implication: $I$, together with the false guard $\neg B$, implies the desired result.

For a for loop, initialization is checked after its initialization statement; preservation includes the loop’s update step. An assertion that is too strong may fail initialization or preservation, whereas one that is too weak may not establish the desired result. (cs.cornell.edu)

The reasoning follows mathematical induction over the number of completed iterations: initialization supplies the base case, and preservation supplies the induction step. It therefore covers any finite number of iterations, including zero. (cs.cornell.edu)

Formal rule and termination

In Hoare logic, a triple $\{P\}\,C\,\{Q\}$ states that if command $C$ starts in a state satisfying its precondition $P$ and terminates normally, its final state satisfies its postcondition $Q$. The rule for a while loop is

The premise expresses preservation; the conclusion records what is known after normal exit through the false guard. Initialization and logical implications connect this rule to the surrounding program’s specification. (cs.cornell.edu)

This establishes partial correctness: if the loop terminates, the claimed result follows. Total correctness additionally requires a termination argument. A common method uses a loop variant, or ranking function, whose value strictly decreases in a well-founded ordering on every iteration. For a nonnegative integer variant, strict decrease prevents infinitely many iterations. Unlike an invariant, which expresses a preserved property, a variant measures progress toward termination. The loop body must also terminate on each iteration. (cs.cornell.edu)

Example: summing a sequence

Consider the following pseudocode, which sums an unchanged sequence $A$ of length $n$, using exact integer arithmetic:

i := 0
s := 0
while i < n:
    s := s + A[i]
    i := i + 1

A suitable invariant is

It states that $s$ is the sum of the already processed prefix. This is an instance of the common pattern of expressing a completed result over a progressively growing part of the input. (arxiv.org)

The proof obligations can be checked directly:

• Initialization: $i=0$ and $s=0$; the empty sum is zero.
• Preservation: if the old index is $i=j<n$, adding $A[j]$ makes $s$ the sum of the first $j+1$ elements. Incrementing $i$ then restores the stated relationship.
• Exit: the false guard gives $i\ge n$, while the invariant gives $i\le n$. Hence $i=n$, and $s$ is the sum of the entire sequence.

The variant $n-i$ is nonnegative at loop tests and decreases by one per iteration, establishing termination. Notice that the sum relationship may temporarily fail between the two assignments: it is restored before the next condition test. (dafny.org)

Choosing and checking invariants

A useful invariant captures both the work already completed and the constraints needed for subsequent work. One systematic approach starts with the postcondition and replaces a final bound with a changing loop index, as in the prefix-sum example. Additional clauses may describe index bounds, preserved input values, or relationships between variables. Research on invariant construction classifies several such transformations of postconditions. (arxiv.org)

Verification systems can accept explicit invariant annotations. In Dafny, for example, an invariant clause generates obligations to establish the assertion on entry and preserve it across iterations; a separate decreases clause supports termination proofs. The verifier uses the declared invariants when reasoning about the loop’s effects. (dafny.org)

The ordinary exit rule applies when the guard becomes false. Other exits, such as break, need separate reasoning: execution may leave before the invariant has been restored, and the guard need not be false. Consequently, an invariant at the loop head is not automatically a postcondition for every possible exit path. (dafny.org)

References

1. CS 2112/ENGRD 2112 Fall 2021: Loop Invariantscs.cornell.edu
2. Hoare: Hoare Logic, Part Ics.cornell.edu
3. Dafny Documentationdafny.org
4. Loop invariants: analysis, classification, and examplesarxiv.org