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
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