Induction Solution

Document last modified: 

Induction Proof of loop invariant - Summation of a sequence

Note

Use of Pk and Pk+1 not necessary but helpful in thinking about the induction.

Question 2.7.2 

a. What is the postcondition?    ∀j: 1 ≤ j ≤ i=n, ∑aj = Pn

b. What is the loop invariant?    ∀j: 1 ≤ j ≤ i, ∑aj = Pk ^ i ≤ n

-- Precondition:  ∃a1
procedure Pn( a1, a2, a3, ..., an : integers)

Pk ← a1

i ← 1

while  i < n

Pk+1 ← Pk + ai+1

i ← i + 1

Pk ← Pk+1
i n Pk ai
1 4 7
1 2 3 4
7 5 9 8
2 4 12
1 2 3 4
7 5 9 8
3 4 21
1 2 3 4
7 5 9 8
4 4 29
1 2 3 4
7 5 9 8

 

Solution

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

before the loop,

-- Precondition:  ∃a1

 c. Base step, show invariant holds:

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

∃a1 ^ (Pk = a1) ^ (1 ≤ n = 4)
2. Inductive Step: Pk → Pk+1

at the end of each loop,

Assume (when loop executes)

i < n

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

Show

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

-- Precondition:  ∃a1
procedure Pn( a1, a2, a3, ..., an : integers)

Pk ← a1

i ← 1

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

Pk+1 ← Pk + ai+1

i ← i + 1

Pk ← Pk+1

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

 

Note ∀j: 1 ≤ j ≤ i, ∑aj = Pk → a1+ a2 ... + ai = Pk  
Pk+1 = Pk +  ai+1 Pk+1 ← Pk + ai+1
  = a1+ a2 ... + ai + ai+1 Substitute
  = ∀j: 1 ≤ j ≤ i, ∑aj + ai+1 Substitute
∴ = ∀j: 1 ≤ j ≤ i+1, ∑aj Summation
     
i+1 ≤ n  
∴ i+1 ≤ n since i < n assumed true

∴ ∀j: 1 ≤ j ≤ i+1, ∑aj = Pk+1 ^ i+1 ≤ n
3. and after the loop completes e. Prove when terminates: ∀j: 1 ≤ j ≤ i = n, ∑aj = Pk ^ i ≤ n

i = n when loop terminates

∀j: 1 ≤ j ≤ i = n, ∑aj = Pk at end by loop invariant

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

Postcondition results from loop invariant at termination.

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

 

Induction Proof of loop invariant - Sorting a sequence

Practical programs consist of modules called by other modules.

Implementing verified programs require that all modules be verified for correctness.

Verified modules, for which preconditions are true, can be assumed to produce true postconditions.

The insert module below inserts a value into an array of n+1 elements that is sorted through the nth element.

insert( a4, {a1, a2, a3})

results in an array a1, a2, a3, a4 that is sorted through the n+1 element.

insert( 5, {3, 6, 9})

results in an array {3, 5, 6, 9}.

-- Precondition:  ∃an+1^∀j: 1 ≤ j < n, aj ≤ aj+1
procedure insert( x, a1, a2, a3, ..., an, an+1 : integers)

i ← 1

while  i < n ^ x > ai

i ← i + 1

x ⇔ ai

while  i ≤ n

i ← i + 1

x ⇔ ai

-- Postcondition:  ∀j: 1 ≤ j ≤ n, aj ≤ aj+1
i n+1 x ai
1 4 5
1 2 3 4
3 6 9 5
2 4 5
1 2 3 4
3 6 9 5
3 4 6
1 2 3 4
3 5 9 6
4 4 9
1 2 3 4
3 5 6 9

 

Insertion sort is relatively simple using insert module.

-- Precondition:  ∃a1
procedure insertionSort( a1, a2, a3, ..., an : integers)

i ← 1

∀j: 1 ≤ j < i,  aj ≤ aj+1 ^ i ≤ n
while  i < n

i ← i + 1

a ← insert( ai , a)

-- Postcondition:  ∀j: 1 ≤ j < n, aj ≤ aj+1
 

Question 2.7.3 

a. What is the postcondition?    ∀j: 1 ≤ j < n, aj ≤ aj+1

b. What is the loop invariant?    ∀j: 1 ≤ j < i,  aj ≤ aj+1 ^ i ≤ n

1. Base Step:

-- Precondition:  ∃a1

i ← 1

 c. Base step, show invariant holds:

∀j: 1 ≤ j < i,  aj ≤ aj+1 ^ i ≤ n

Vacuously true: 1 ≤ j < 1.
2. Inductive Step: Pk → Pk+1

at the end of each loop.

∀j: 1 ≤ j < i,  aj ≤ aj+1 ^ i ≤ n
while  i < n

i ← i + 1

a ← insert( ai , a)
d. Assume what for Pk? Note that k=i.

∀j: 1 ≤ j < i,  aj ≤ aj+1 ^ i ≤ n

e. Show what for Pk+1?

∀j: 1 ≤ j < i+1,  aj ≤ aj+1 ^ i+1 ≤ n

f. Prove ∀j: 1 ≤ j < i+1,  aj ≤ aj+1 ^ i+1 ≤ n

i+1 ≤ n true since executing while requires i < n

insert preconditions must hold, where k=n=i: ∃ai+1^∀j: 1 ≤ j < i, aj ≤ aj+1

Assuming k=i precondition true: ∀j: 1 ≤ j < i,  aj ≤ aj+1 ^ i ≤ n

insert k=i postcondition true: ∀j: 1 ≤ j ≤ i, aj ≤ aj+1

and also true:

∀j: 1 ≤ j < i+1, aj ≤ aj+1

i+1 ≤ n → ∃ai+1
3. and after the loop completes g. Prove when loop terminates:

∀j: 1 ≤ j < i,  aj ≤ aj+1 ^ i ≤ n

i = n when loop terminates

∀j: 1 ≤ j < i,  aj ≤ aj+1 at end by loop invariant

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