# 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

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+...+aiPk+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 = PkPk+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