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