Description
Problem 1. (20 points)
Verify that the following program segment is correct with respect to the initial assertion y = 3 and the final
assertion z = 6.
Algorithm 1: program segment
1 x := 2
2 z := x + y
3 if y > 0 then
4 z := z + 1
5 else
6 z := 0
Solution.
p ⇒ y := 3
x := 2
z := x + y ⇒ 5
Condition: y > 0
z := 5 + 1 = 6
∴ p{S}q because z = 6 ∧ z = 6 with given p
1
Problem 2. (30 points)
Use a loop invariant to prove that the following program segment for computing the n-th power, where n is
a positive integer, of a real number x is correct.
Algorithm 2: program segment
1 power := 1
2 i := 1
3 while i ≤ n do
4 power := power ∗ x
5 i := i + 1
Solution.
To show p is a loop invariant, if p is true at the beginning of the loop, then p must still hold true after the
exectutoin of the loop
Let p ⇒ i ≤ n + 1 ∧ power = x
i−1
Assume p is true,
Check if p is true at the end of the loop
iloop = i + 1
powerloop = power ∗ x
= x
i−1
∗ x
= x
i
= x
iloop−1
With condition i ≤ n
iloop ≤ n + 1 follows
∴ p is true at the end of the loop
Show p is true before loop is executed
It is given that n ≥ 1 so, i ≤ n + 1
power = 1
= x
0
= x
i−1
∴ p is true before the loop executes
Show loop terminates correctly
Loop terminates when p is true and i ≤ n is false
i = n + 1 so
power = x
(n+1)−i
= x
n
∴ Loop terminates correctly
Show loop terminates
i0 = 1
i = i + 1
i will continue to increace until i > n resulting in i ≤ n being false
∴ loop terminates after n iterations
∴ program is correct
2
Aggie Honor Statement: On my honor as an Aggie, I have neither given nor received any unauthorized
aid on any portion of the academic work included in this assignment.
Checklist: Did you…
1. abide by the Aggie Honor Code?
2. solve all problems?
3. start a new page for each problem?
4. show your work clearly?
5. type your solution?
6. submit a PDF to eCampus?
3
Powered by TCPDF (www.tcpdf.org)
