Section 2.3 More on Proof of Correctness
137
eXeRciSeS 2.3
1. Let Q: x
2
> x + 1 where x is a positive integer. Assume that Q is true after the kth iteration of the following while loop; prove that Q is true after the next iteration.
while (x > 5) and (x < 40) do
x = x + 1
end while
2. Let Q: x! > 3
x
where x is a positive integer. Assume that Q is true after the kth iteration of the following
while loop; prove that Q is true after the next iteration.
while (x > 10) and (x < 30) do
x = x + 2
end while
In Exercises 3–6, prove that the pseudocode program segment is correct by proving the given loop invariant Q
and evaluating Q at loop termination.
3. Function to return the value of x! for x ≥ 1.
Factorial (positive integer x)
Local variables:
integers i, j
i = 2
j = 1
while i ≠ x + 1 do
j = j * i
i = i + 1
end while
//j now has the value x!
return j
end function Factorial
Q: j = (i − 1)!
4. Function to return the value of x
2
for x ≥ 1.
Square (positive integer x)
Local variables:
integers i, j
i = 1
j = 1
while i ≠ x do
j = j + 2i + 1
i = i + 1
end while
S e c t i o n 2 . 3 review
tecHniQueS
• Verify the correctness of a program segment that
includes a loop statement.
• Compute gcd(a, b) using Euclid’s algorithm.
MAin iDeAS
• A loop invariant, proved by induction on the number of loop iterations, can be used to prove correctness of a program loop.
• The classic Euclidean algorithm for finding the
greatest common divisor of two positive integers is
provably correct.
W