LARA

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.