Loop invariant

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 fulfilled 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