LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:proof_of_first_lecture01_example [2008/02/19 14:16]
vkuncak
sav08:proof_of_first_lecture01_example [2015/04/21 17:30]
Line 1: Line 1:
-====== Proving Correctness of Recursive Multiplication ====== 
- 
-We prove that this function computes x*y: 
- 
-<​code>​ 
-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)); 
-    } 
-  } 
-} 
-</​code>​ 
- 
-By translating Java code into math, we obtain the following mathematical definition of $f$: 
- 
-\[ 
-    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 $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. 
-\[ 
-   ​f(x,​y) = f(x,2k) = 2 f(x,k) = 2 (x k) = x (2 k) = x y 
-\] 
-  * 
-     * **Case 2**: $y = 2k+1$. Note $y-1 < y$ and $k < y$. By definition and I.H. 
-\[ 
-   ​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.