This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
int multiply (unsigned x, unsigned y) { | |
unsigned a,b; | |
unsigned c = 0; | |
// make sure a < b so that we add b a times | |
if (x<y) { | |
a = x; | |
b = y; | |
} else { | |
a = y; | |
b = x; | |
} | |
while (a > 0) { | |
if (a & 1) | |
c += b; | |
a >>= 1; | |
b <<= 1; | |
} | |
return c; | |
} |
To prove that it works, consider the function
f(a,b,c) = ab + c
before the loop, during the loop, and after the loop.
Before the loop, we have
f = xy + 0 = xy
During the loop, we have for even a,
a' = a/2
b' = 2b
c' = c
f' = ab + c = xy
and for odd a,
a' = (a-1)/2
b' = 2b
c' = c + b
f' = ab + c = xy
Hence, it must be the case that f(a,b,c) = xy for any number of iterations in the loop by induction. Now, the ending condition of the loop yields a = 0, so it must be the case that
c = f - ab = f = xy
In other words, the return value is guaranteed to be the product of the input x and y!
No comments:
Post a Comment