Loop Invariant

hoare-calculus program-proofing

Definition

Loop Invariant

A loop invariant is a logical formula (assertion) $Inv$ that holds true before, during, and after the execution of a loop. Specifically, for a loop while e do Π od, the invariant must satisfy:

1. It is true before the loop starts.
2. If it is true before an iteration of the loop body $\Pi$ (and the loop condition $e$ holds), it remains true after the execution of $\Pi$.

Verification Rule

The Hoare calculus rule for loops relies entirely on finding a suitable invariant:

$$\frac{\{Inv\wedge e\}\Pi \{Inv\}}{\{Inv\}\mathbf{while}e\mathbf{do}\Pi \mathbf{od}\{Inv\wedge \neg e\}}{}_{\text{(wh)}}$$

Application in Proofs

To prove a specification $\{F\}\mathbf{while}e\mathbf{do}\Pi \mathbf{od}\{G\}$, one must find an invariant $Inv$ such that:

1. Precondition implies Invariant: $F⟹Inv$
2. Invariance: $\{Inv\wedge e\}\Pi \{Inv\}$ is a valid Hoare triple.
3. Postcondition follows: $Inv\wedge \neg e⟹G$

Finding Invariants

Finding a loop invariant is the most difficult part of program verification. It often requires creativity and understanding of the algorithm. There is no general algorithm to automatically generate loop invariants for arbitrary programs (due to the Halting Problem).

Strategies

• Generalisation: Start with the postcondition $G$ and try to generalise it (e.g., replace a constant with a variable).
• ** weakening**: If $G$ is too strong to be an invariant, find a weaker formula that is still strong enough to imply $G$ upon termination.