This is an old revision of the document!
Proving Correctness of Recursive Multiplication
We prove that this function computes x*y:
private static int f(int x, int y) { if (y == 0) { return 0; } else { if (y % 2 == 0) { int z = f(x, y / 2); return (2 * z); } else { return (x + f(x, y - 1)); } } }
By translating Java code into math, we obtain the following mathematical definition of :
\[
f(x,y) = \left\{\begin{array}{rl}
0, & \mbox{ if } y = 0
2 f(x,\lfloor\frac{y}{2}\rfloor), & \mbox{ if } y > 0, \mbox{ and } y=2k \mbox{ for some } k
x + f(x,y-1), & \mbox{ if } y > 0, \mbox{ and } y=2k+1 \mbox{ for some } k
\end{array}\right.
\]
By induction on we then prove .
- Base case. Let . Then
- Inductive hypothesis. Assume that the claim holds for all values less than .
- Goal: show that it holds for where .
- Case 1: . Note . By definition
\[
f(x,y) = f(x,2k) = 2 f(x,k) = 2 (x k) = x (2 k) = x y
\]
-
- Case 2: . Note . By definition
\[
f(x,y) = f(x,2k+1) = x + f(x,2k) = x + 2 f(x,k) = x + 2 (x k) = x (2 k + 1) = x y
\] This completes the proof.