Question 2.7.2
a. What is the postcondition?
b. What is the loop invariant?

Show ∀j: 1 ≤ j ≤ i, ∑a_j = P_k ^ i ≤ n is always true

1. Base Step: before the loop,
-- Precondition: ∃a₁ c. Base step, show invariant holds:
∀j: 1 ≤ j ≤ i, ∑a_j = P_k ^ i ≤ n

2. Inductive Step: P_k → P_k+1

at the end of each loop,
Assume (when loop executes)

i < n
∀j: 1 ≤ j ≤ i, ∑a_j = P_k ^ i ≤ n

Show ∀j: 1 ≤ j ≤ i+1, ∑a_j = P_k+1 ^ i+1 ≤ n

-- Precondition: ∃a₁
procedure P_n( a₁, a₂, a₃, ..., a_n : integers)

P_k ← a₁i ← 1

∀j: 1 ≤ j ≤ i, ∑a_j = P_k ^ i ≤ n

while i < n

P_k+1 ← P_k + a_i+1i ← i + 1
P_k ← P_k+1

d. Prove ∀j: 1 ≤ j ≤ i+1, ∑a_j = P_k+1 ^ i+1 ≤ n

Note ∀j: 1 ≤ j ≤ i, ∑a_j = P_k→ a₁+ a₂ ... + a_i = P_k

3. and after the loop completes e. Prove when terminates: ∀j: 1 ≤ j ≤ i , ∑a_j = P_k ^ i ≤ n

-- Precondition: ∃a_n+1^∀j: 1 ≤ j < n, a_j ≤ a_j+1
procedure insert( x, a₁, a₂, a₃, ..., a_n, a_n+1 : integers)

i ← 1

while i < n ^ x > a_i

i ← i + 1

x ⇔ a_i

while i ≤ n

i ← i + 1

x ⇔ a_i

-- Postcondition: ∀j: 1 ≤ j ≤ n, a_j ≤ a_j+1

i n+1 x a_i

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: ∃a₁
procedure insertionSort( a₁, a₂, a₃, ..., a_n: integers)
i ← 1

∀j: 1 ≤ j < i, a_j ≤ a_i ^ i ≤ n

while i < n

i ← i + 1

a ← insert( a_i , a)

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

Question 2.7.3

a. What is the postcondition?

b. What is the loop invariant?

1. Base Step:

-- Precondition: ∃a₁

i ← 1

c. Base step, show invariant holds:

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

2. Inductive Step: P_k → P_k+1

at the end of each loop.

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

while i < n

i ← i + 1

a ← insert( a_i , a)

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

d. Assume what for P_k? Note that k=i.

e. Show what for P_k+1?

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

insert preconditions must hold,

where k=n=i: ∃a_i+1^∀j: 1 ≤ j < i, a_j ≤ a_j+1

Assume k=i precondition true: ∀j: 1 ≤ j < i, a_j ≤ a_j+1 ^ i < n
then use insert postconditions for k+1= i+1.

3. and after the loop completes

g. Prove when loop terminates:

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