Loop Invariant

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 P_k and P_k+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 P_k = 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 P_k and P_k+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, ∑a_j = P_k ^ 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

 

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; a_j ≠ 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, a_j ≠ x → location = 0 XOR ∃k: 1 ≤ k ≤ n, a_k = 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 = a_i} location ← i { location = i v location = 0}, {i > n && i > n xor x = a_i} location ← 0 { location = i v location = 0}
           {i > n xor x = a_i} 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 = a_i} location ← i { location = i v location = 0}

false: {i > n && i > n xor x = a_i} 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