
タイトル：
0109 Correctness: Naive

概説：

Let's go through and actually do a proof of the correctness

of the naive algorithm we just spoke about.

We're going to proceed by taking advantage of a particular observation.

What we're trying to prove here is the correctness of the claim

that naive(a,b) outputs the product of a and b.

The observation that I'm going to make is that before or after the "while" loop

in the implementation of naive, this statement is always true.

The variables x and y multiply together and added to z

is exactly equal to a times b. How are we going to show that this is the case?

The first time we're going through the "while" loop in the very beginning

and the top of the function, x is assigned to a, y is assigned to b, and z is assigned to 0.

Let's check the expression with those variables plugged in.

We're saying that's ab equals ab+0. Well, that's kind of obvious.

Well, the next thing we're going to show is that if it's the case

that at the beginning of the "while" loop, this condition holds that a times b

is exactly equal to x times y plus z,

then it's going to be the case that with the new values, so x, y, and z may change.

The new values x prime, y prime, and z prime are going to satisfy this as well.

If it was true before, then it has to be true after.

Why would this be true? Let's remind ourselves what the code looks like again.

What happens in each integration of the loop is that a new value of z is computed,

which is the old value plus the value of y,

and a new value of x is computed, which is the old value minus 1.

We basically had the new value of x if the old value minus 1, the new value of y not been changed,

and the new value of z is the old value of z plus y.

All right! What can we say about x prime times y prime plus z prime?

We know what x prime, y prime, and z prime are, so let's substitute those in.

That's x minus 1 times y plus z plus y. Now we just do a little bit of algebra.

Multiplying this out, we get xy minus y plus z plus y.

and these y's, +y and y cancel and so we get xy plus z.

But, notice what we assumedwe say if it was the case the xy plus z is equal to ab,

then what we're showing is that x prime, y prime plus z prime is equal to ab.

Well guess what? We showed that x prime times y prime plus z prime does indeed equal ab

if it was true at the top of the loopso this condition that we're testing here

this ab equals xy plus z is maintained through each step of the "while" loop.

It starts out true but it remains true each time it goes through the "while" loop.

What we know is that while this code is running each time we go through the "while" loop,

this condition is always true and eventually, the "while" loop terminates.

The "while" loop terminates when x equals 0, so what does that mean?

The xy plus z has to equal ab, but x is 0, so that 0 times y plus z equals to ab. This has to be true.

Well, 0 times y is 0, so this is actually saying that z has to be equal to ab at the end of the loop.

Once x reaches 0, z has to equal ab. Keep in mind that's exactly what we returnthe value of z.

The thing that is returned is going to be a times b.

Let's just take a look at the code again to see that that's what it's doing.

Each time it goes through, it's decrementing x accumulating the values in z,

and eventually when x is exhausted, it returns z and it is exactly a times b.