===========================================================================
CSC 236 Tutorial Solutions for Week 8 Winter 2012
===========================================================================
Prove the correctness of the following algorithm.
mult(m, n):
# Pre: m in N, n in Z
x = m
y = n
z = 0
# Loop Inv: z = m * n - x * y
while x != 0:
if x % 2 == 1: z = z + y
y = y << 1 # left shift, equivalent to y = y * 2
x = x >> 1 # right shift, equivalent to x = floor(x / 2)
return z
# Post: returns m * n
Recall that the "right shift" operator >> removes some number of bits from
the right end of its first operand (e.g., 11010 >> 2 = 110).
Similarly, the "left shift" operator << adds 0s to the right end of its
first operand (e.g., 1101 << 2 = 110100).
[This is the example in section 2.4 of the textbook, rephrased to use the
same notation I use in lecture.]
{ Before getting into proofs, go over the algorithm and make sure everyone
understands the operations that are being carried out (right and left
shift). Some examples might help the students:
12 << 1 = (1100) << 1 = (11000) = 24 = 2 * 12
37 >> 1 = (100101) >> 1 = (10010) = 18 = floor(37 / 2) }
Q: What does it mean to prove the algorithm correct?
A: Prove for all inputs that satisfy precondition, postcondition holds
after execution.
Q: How do we approach this?
A: Code consists of one loop with a few initial statements, so focus on
proving loop invariant.
{ See below for discussion of how to obtain loop invariant, if there is
time at the end. For now, focus on proof. }
Q: How do we know loop invariant is "right"?
A: Two quick ways to check:
1. Check loop invariant is useful:
At end of loop, x = 0 (negation of loop condition) and
z = m * n - x * y (loop invariant), so z = m * n, as desired.
NOTE: Once we have shown the loop terminates, this proves correctness
of the entire algorithm! All we need is to prove loop invariant, and
termination.
2. Check loop invariant is reasonable:
At start of loop, x = m, y = n, z = 0, so z = m * n - x * y.
NOTE: This is base case in the proof!
Q: Format of proof? Induction on what value?
A: By induction on the number of iterations of the loop.
{ Get students to suggest steps one by one, and content of each step. }
Base: x_0 = m, y_0 = n, z_0 = 0, so z_0 = m * n - x_0 * y_0.
I.H.: Let k >= 0 and suppose LI_k holds (z_k = m * n - x_k * y_k).
Step: To prove LI_{k+1}, consider two cases.
Q: Which cases?
A: Either there is or there is no iteration number k+1.
Case 1: If there is NO iteration number k+1, ...
Q: What can we conclude?
A: ... LI_{k+1} is equivalent to LI_k and holds by IH.
Case 2: If there is an iteration number k+1, ...
Q: What can we conclude?
A: ... x_k != 0 (directly from loop condition).
Q: What next?
A: Figure out effect of one iteration.
- If x_k % 2 == 0, z_{k+1} = z_k;
otherwise, z_{k+1} = z_k + y_k.
- y_{k+1} = 2 y_k
- x_{k+1} = floor(x_k / 2)
Q: How do we put this together?
A: Consider cases x_k even, x_k odd.
Subcase A: x_k even, i.e., x_k % 2 == 0:
z_{k+1} = z_k
= m * n - x_k * y_k (by IH)
= m * n - (x_k / 2) * (2 * y_k)
= m * n - x_{k+1} * y_{k+1}
Subcase B: x_k odd, i.e., x_k % 2 == 1:
z_{k+1} = z_k + y_k
= m * n - x_k * y_k + y_k (by IH)
= m * n - (x_k - 1) * y_k
= m * n - ((x_k - 1) / 2) * (2 * y_k)
= m * n - x_{k+1} * y_{k+1}
In all subcases, z_{k+1} = m * n - x_{k+1} * y_{k+1}.
In all cases, LI_{k+1} holds.
By induction, LI_k holds for all k in N.
Q: What next?
A: Termination.
Q: Standard technique?
A: Find expression E such that for all k >= 0,
- E_k in N,
- if there is an iteration number k+1, E_{k+1} < E_k.
Q: What expression will work?
A: Find a quantify that keeps decreasing: E = x.
E_0 = x_0 in N (by precondition).
Let k in N and suppose E_k in N.
If there is no iteration k+1, E_{k+1} = E_k in N.
If there is an iteration k+1, then x_k != 0 (from loop condition) and
x_{k+1} = floor(x_k / 2) (from loop body) so E_{k+1} = x_{k+1} in N,
and E_{k+1} = floor(x_k / 2) < x_k = E_k.
Q: Conclusion?
A: E_0 > E_1 > ... is a sequence of natural numbers and must be finite,
i.e., loop terminates.
Q: What next?
A: Overall conclusion, derived above (see NOTE under "check loop invariant
is useful").
---------------------------------------------------------------------------
How to derive loop invariant -- if time permits and there is interest (it
would be fine if you run out of time for this, or if you decide not to
cover it even if there is time left; judge the interest of the students).
[See section 2.4 in textbook.]