Loop Invariant

Document last modified: 

Proof of Correctness - Loop Invariant

Program correctness proofs involving loop invariants done formally are often lengthy, we'll look at a less formal proof first and later a short formal proof of a factorial function.

Loop invariant proofs must show three parts:

  1. Initialization - the loop invariant holds prior to executing the loop, after initialization.
  2. Maintenance - the loop invariant holds at the end of executing the loop.
  3. Termination - the loop eventually terminates.
{ Precondition: n ≥ 1 }

fact(n)

i ← 1
fact ← 1

{ Invariant P: fact = i! && i ≤ n}

while (i < n) do
        i ← i + 1
        fact ← fact * i

{ Postcondition: fact = n! }

1. Initialization: Prove assertion P true at start of loop:

i ← 1 ≤ n                     -- by { Precondition: n ≥ 1 }

fact ← 1 = 1! = i!        -- by definition of 1!

{ P: fact = i! && i ≤ n } is true before while.

 

Loop invariant for while loops:

        {test && P} S {P}          
{P} while (test) S {!test && P}
2. Maintenance: Prove P is true at end of loop:

Assume:

{ P: fact = i! && i ≤ n } is true

test condition while (i<n) is true.

New values inew and factnew of i and fact are:

inew ← i + 1

factnew ← fact * (i+1) = (i+1)! = inew!

Since i < n also have:

inew ← i + 1 ≤ n

{ P: fact = i! && i ≤ n } is true at end of loop since fact = i! && i ≤ n.

3. Termination: Prove that loop terminates

At beginning:

i ←1

Assuming the precondition n ≥ 1 holds, after n-1 loop traversals of:

      i ← i + 1

the new value of i will be:

i = n

terminating the loop.

Loop terminates given that precondition holds:

n ≥ 1

{ P: fact = i! && i ≤ n } is then a loop invariant.

4. Postcondition met

Since P is a loop invariant, by:

       {test && P} S {P}          
{P} while (test) S {!test && P}

If the while terminates, { P: fact = i! && i ≤ n } is then true

fact = i!

i ≤ n

and i < n is false, from 3. Termination.

Hence at loop termination:

i = n

fact = i! = n!

 

Proof of correctness - Loop invariant induction proof

Loop invariant proofs can also be performed by induction, often with less bookkeeping than the previous method.

Note below use of Pk and Pk+1 not necessary but helpful in thinking about the induction.

The loop invariant is:

Pk = k! ^ k ≤ n
pre: n ≥ 1

Pn(n)

k := 1
Pk := 1

Pk = k! ^ k ≤ n
while k < n
        Pk+1 := Pk * k+1
        k := k + 1
        Pk := Pk+1

post: Pn = n!

Show Pk = k! ^ k ≤ n is always true:

1. Base Step:

before the loop,

P1 = 1! ^ 1 ≤ n

        Given pre: n ≥ 1

2. Inductive Step: Pk → Pk+1

at the end of each loop,

Show

Pk+1 = (k+1)! ^ (k+1) ≤ n

Assume Pk = k! ^ k < n

Pk = 1 * 2 * ... * k
  = k!

 k < n for loop execution

Pk+1 = 1 * 2 * ... * k * k+1
  = Pk * k+1
  = k! * (k+1)
  = (k+1)!
k+1 ≤ n k < n assumed true
  k+1 ≤ n

Pk+1 = (k+1)! ^ (k+1) ≤ n

3. and after the loop completes k = n

Pk = k! ^ k = n

∴ Pn = Pk

 

Correctness Proof of loop invariant - Summation of a sequence

Loop invariant proofs can also be performed by induction, often with less bookkeeping than the previous method.

Note below use of Pk and Pk+1 not necessary but helpful in thinking about the induction.

The loop invariant is:

∀j: 1 ≤ j < i, ∑aj = Pk ^ i+1 n
-- Precondition:  ∃a1
procedure Pn( a1, a2, a3, ..., an : integers)

Pk 0

i 0

∀j: 1 ≤ j ≤ i, ∑aj = Pk ^ i n
while  i < n

i i + 1

Pk+1 Pk + ai

Pk Pk+1

-- Postcondition: ∀j: 1 ≤ j ≤ n, ∑aj = Pk

Show ∀j: 1 ≤ j ≤ i, ∑aj = Pk ^ i n is always true

1. Base Step:

before the loop,

∀j: 1 ≤ j ≤ 0, ∑aj = Pk ^ 0 n

∀j: 1 ≤ j ≤ 0, ∑aj = Pk
vacuously true since 1 ≤ j ≤ 0 does not exist.

2. Inductive Step: Pk → Pk+1

at the end of each loop,

Show

∀j: 1 ≤ j ≤ i+1, ∑aj = Pk+1^ i+1 n

Assume for loop execution

i < n

∀j: 1 ≤ j ≤ i, ∑aj = Pk

Note that ∀j: 1 ≤ j ≤ i, ∑aj = Pk = a1+...+ai

Pk+1 = a1+...+ai+ai+1

        = Pk + ai+1

        = ∀j: 1 ≤ j ≤ i, ∑aj + ai+1

        = ∀j: 1 ≤ j ≤ i+1, ∑aj

 i+1 n

since i < n for loop execution

∴ ∀j: 1 ≤ j ≤ i+1, ∑aj = Pk+1^ i+1 n

3. and after the loop completes i = n

∀j: 1 ≤ j ≤ i = n, ∑aj = Pk

ESCJava version - Summation of a sequence

class Summation {

	int Pk;

/*@ pre A != null; 
       post \result == Pk;                                                    @*/

  int sum(int A[]) {

        int j;
        j=0; 
        Pk=0;

        /*@ loop_invariant (\forall int k; 
                                                 0 <= k && k < j; 
                                                 Pk == \old(Pk) + A[k]);   @*/
        while(j < A.length) {
	 Pk = Pk+A[j];
            j++;
        }
        return Pk;
   }
}

 

Correctness Proof of loop invariant - Linear Search

The loop invariant is:

∀j: 1 ≤ j < i; aj ≠ x ^ i ≤ n+1
-- pre: ∃x ^ ∃a1

procedure linear search (x: integer,
                                        a1, a2, ..., an: integers)
       i ← 1

∀j: 1 ≤ j < i; aj ≠ x ^ i ≤ n+1
while  i ≤ n and x ≠ ai
   i  ← i + 1

if i ≤ n then
   location  ← i
else
   location  ← 0

-- post: ∀j: 1 ≤ j ≤ n, aj ≠ x → location = 0
--  XOR ∃k: 1 ≤ k ≤ n, ak = x → location = k

Show ∀j: 1 ≤ j < i; aj ≠ x ^ i ≤ n+1 is always true

1. Base Step:  Show P1 is true

before the loop,

Given: ∃x ^ ∃a1

∀j: 1 ≤ j < 1; aj ≠ x ^ 1 < n+1

vacuously true since 1 ≤ j < 1 does not exist.

2. Inductive Step: Pk → Pk+1

at the end of each loop,

Show Pk+1

∀j: 1 ≤ j < i+1; aj ≠ x ^ i+1 ≤ n+1

Assume Pk (for loop execution to occur)

i n

∀j: 1 ≤ j < i; aj ≠ x = Pk

∀j: 1 ≤ j < i, aj ≠ x → a1≠ x ^ ...^ ai-1≠ x = Pk

Pk+1 = a1≠ x ^ ...^ ai-1≠ x ^ ai≠ x

        = Pk ^ ai≠ x

        = ∀j: 1 ≤ j < i; aj ≠ x ^ ai≠ x

        = ∀j: 1 ≤ j < i+1; aj ≠ x

 i+1 n+1

since i n for loop execution

∴ ∀j: 1 ≤ j < i+1; aj ≠ x ^ i+1 ≤ n+1

3. and after the loop completes, the following is false

i ≤ n and x ≠ ai

   and the inverse is true

i > n or x = ai

   Since mutually exclusive, only one can be true

i > n xor x = ai

i > n xor x = ai

∀j: 1 ≤ j < i; aj ≠ x ^ i ≤ n+1 when i > n

∀j: 1 ≤ j < i; aj ≠ x ^ i ≤ n+1 when i ≤ n ^ ai = x

Postcondition

∀j: 1 ≤ j ≤ n, aj ≠ x → location = 0 XOR ∃k: 1 ≤ k ≤ n, ak = x → location = k

Most of the work has been completed in Step 3. above by proving correctness of the loop invariant.

Because the algorithm includes an if-else condition, we can prove the postcondition is true using the if-else rule of inference:

{test && P} S1 {Q}, { !test && P} S2 {Q}
           {P} if (test) then S1 else S2 {Q}

if i ≤ n then
   location  ← i
else
   location  ← 0

P i > n xor x = ai                          From Step 3
test i ≤ n                                          if i ≤ n
S1 location  ← i
S2 location  ← 0
Q location = i v location = 0        

Substituting P, S1, S2, and Q of the if-else conditional, we get:

{i ≤ n && i > n xor x = ai} location ← i { location = i v location = 0}, {i > n && i > n xor x = ai} location ← 0 { location = i v location = 0}
           {i > n xor x = ai} if (i ≤ n) then location ← i else location ← 0 { location = i v location = 0 }

Both S1 and S2 must be proven (the true and false case) to hold for precondition P, producing the same Q postcondition.

true: {i ≤ n && i > n xor x = ai} location ← i { location = i v location = 0}

false: {i > n && i > n xor x = ai} location ← 0 { location = i v location = 0}

Proof of true case:

i ≤ n && i > n xor x = ai i ≤ n given to be true
i > n xor x = ai true from loop invariant
i ≤ n Simplification Rule of Inference
x = ai From loop invariant
∀j: 1 ≤ j < i; aj ≠ x ^ i ≤ n+1 when i ≤ n ^ ai = x
location ← i i ≤ n && i > n xor x = ai

From loop invariant, i is location where found, so false

i > n

and true

i ≤ n && x = ai

Proof of false case:

i > n && i > n xor x = ai i > n given to be true
i > n xor x = ai true from loop invariant
i > n Simplification Rule of Inference
x ≠ ai From loop invariant
∀j: 1 ≤ j < i; aj ≠ x ^ i ≤ n+1 when i > n
location ← 0 i > n && i > n xor x = ai

From loop invariant, x ≠ ai, is true so

x = ai

is false and true

i > n && i > n