Loop invariant: Meaning (information, definition, explanation, facts)

In computer science, A loop invariant is an invariant used to prove properties of loops.

There is a normal form of loop invariants:

{P} while (condition) // condition = B { S; // {I} } {Q}

That means:

if P was true before the loop, then Q will be true after the loop. And the program will be partially correct.

The following conditions must be fullfilled for the invariant I:

1. P => I (the invariant is true at the beginning) 2. {I} B {I} (the invariant is not changed by evaluating B) 3. {I ^ B} S {I} (the invariant is not changed by the loop) 4. {I ^ (not B)} => Q (as soon as B is no longer true, Q must be implied)

Example:

f(n) { // {P: n >=0 } int k=n; int erg=1; while (k>0) { erg=erg*k; k=k-1; } // {Q: erg=k! } }

Suitable invariant:

{ I: (n!=erg*k!) ^ (k>=0) }

Proof of the 4 points:

1. (n>=0), erg=1; k=n; => n!=n! ^ (n>=0) => (n!=erg*k!) ^ (n>=0)

2. {(n!=erg*k!) ^ (k>=0)} (k>0) => {I}

3. (n!=erg*k!) ^ (k>=0) ^ (k>0) Now evaluate the program:

(n!=erg*k*(k-1)!) ^ (k>=-1) ^ (k>0) => (n!=erg*k!) ^ (k>0) = I ^ b => I

4. (n!=erg*k!) ^ (k>=0) ^ (k<=0)

=> (n!=erg*k!) ^ (k=0)

=> (n!=erg)

q.e.d