Tip:
Highlight text to annotate it
X
Why does this work? We're going to do another proof of correctness.
It turns out that the same strategy that we used for naive is going to work out really well here.
In particular, what holds is that the product of a and b is always equal to the product of x and y plus z.
And again, since x is going to be counting down and eventually reads 0,
z is going to ultimately have to hold the product of a and b.
Can we prove that this is the case? Again, we need to do 2 things.
We need to say that it starts off with that being the case.
That's the same exact argument that we had in the naive algorithm,
because x starts out as a, y starts out as b, and z starts out as 0, so that holds.
Now we need to show that if this condition holds at the beginning of the top of the "while" loop,
then it's going to hold at the end with the new values of x, y, and z.
Let's remind ourselves how x, y, and z changed in the "while" loop,
so we can see whether the condition still holds.
We're going to have to break this into 2 cases.
First, if x is odd, and second, if x is even because 2 slightly different things happen.
So in the case when x is odd, the first thing we do is add z and y together,
make that a new value of z, then we do a bit shift on x,
which in this case is equivalent to subtracting 1 to make it even and smaller than having it.
And y, meanwhile, gets doubled.
What can we say about x prime times y prime plus z prime, so that is on the bottom of the loop.
We can substitute in these values--get x minus 1 over 2 times the new value of y just 2y,
plus the new value of z, which is z plus y.
We noticed that this 2 and that 2 cancel, and we get xy minus y plus z plus y.
Again that +y and -y cancel, then we do indeed get xy minus z,
which we had assumed holds in advance, so that's a times b.
What about the case where x is even?
So in some ways, this case is easier because the bit shift on x just halves it.
Z doesn't change at all and y again is doubled. Let's look to see what happens in this case.
What happens now is the value of z doesn't change at all,
and in some sense, x and y just move the 2 around, so x get half, then y's get doubled.
When we multiplied those 2 together, they cancel, and again we get xy plus z,
which we had assumed, coming in to this, is equal to a times b.
The new values of x, y, and z in either the case where x is odd or x is even,
continue to satisfy this property.
This is kind of strange--what is true in here is removing the factor 2
back and forth between x and y, actually generally from x to y.
When if it's odd, then we had to shift x a little bit more than that to make it balanced.
We move some of the value into z. This is kind of lucky.