CSC165H1Y Homework Exercise # 6 | Sample Solutions Summer 2012
Worth: 3% Due: By 3 pm on Tuesday July 24.
1. (a) Write a detailed argument that shows that the loop invariant holds just before the loop condition is
evaluated for the ▯rst time, under the assumption that the precondition is true.
The code that we talk about in this sub-question is lines 1 ▯ 3. It does not change x and y, and a, b
and z don’t have values before the code is executed. So, we can use the variable names to talk about the
variables after line 3.
(Of course, we could also de▯ne v to be the value of a variable v just after line 3, and v to be the value
0 0 0 0 0
just before line 1. Then x = x, y = y, a = x, b = y and z = 1, and a, b and z are unde▯ned).
+ +
Assume x 2 N ^ y 2 N
Then, z ▯ (a )b
= 1(a ) # z = 1 by line 3
= x b # a = x by line 1
= x y # b = y by line 2
b y
Then, z ▯ (a ) = x
+ + b y
Then, (x 2 N ^ y 2 N ) ) (z ▯ (a ) = x )
(b) Assuming that the loop invariant is correct, write a detailed argument that shows that the postcondition
will be satis▯ed once the loop terminates.
The code between the end of the loop and the return statement is empty, so again we don’t need any
0
special notation. (Of course, we could still say that v = v for any variable v).
b y
The loop invariant is z ▯ (a ) = x , and if the loop terminates, then b = 0
Assume z ▯ (a ) = x ^ b = 0
Then, x = z ▯ (a ) b # Loop Invariant
= z(a ) # b = 0
= z
Then, z = x y
Then, z ▯ (a ) = x ^ b = 0 ) z = x y
(c) Write a detailed argument that shows that the loop invariant is correct. That is, show that the loop
invariant is true each time the program evaluates the loop condition.
Here we need to show that for an arbitrary loop iteration, if the loop invariant was true at the beginning
of the iteration, it is true at the end of that iteration.
Let i be an arbitrary iteration. Let us say that the variables a, b and z will refer to the values of these
t
variables when the loop condition is evaluated at the beginning of the i h iteration. Let us say that the
variables a , b and z will refer to the values of these variables when the loop condition is evaluated just
th
after the i iteration. The code we are considering is lines 5{9. The variables x and y are unchanged,
so we don’t need separate variables to refer to them.
We want to prove that if the loop invariant holds at the beginning of the i th iteration, it will hold at its

More
Less