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$ :

$\begin{equation*} 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. \end{equation*}$

By induction on $y$ we then prove $f(x,y) = x \cdot y$ .

Base case. Let $y=0$ . Then $f(x,y) = 0 = x \cdot 0$
Inductive hypothesis. Assume that the claim holds for all values less than $y$ .
- Goal: show that it holds for $y$ where $y > 0$ .
- Case 1: $y = 2k$ . Note $k < y$ . By definition and I.H.

$\begin{equation*} f(x,y) = f(x,2k) = 2 f(x,k) = 2 (x k) = x (2 k) = x y \end{equation*}$

- Case 2: $y = 2k+1$ . Note $y-1 < y$ . By definition and I.H.

$\begin{equation*} f(x,y) = f(x,2k+1) = x + f(x,2k) = x + x \cdot (2k) = x (2 k + 1) = x y \end{equation*}$

This completes the proof.