Where to start when proving correctness of algorithms

Question

I have just begun going through the algorithm design manual and am finding it difficult to grasp how to prove the correctness of algorithms. Can someone please help me by explaining the example question I have provided.

Prove the correctness of the following recursive algorithm to multiply two natural numbers, for all integer constants c ≥ 2.

function multiply(y,z)
comment Return the product yz.
1. if z = 0 then return(0) else
2. return(multiply(cy, z/c) + y · (z mod c))

Answer 1

Let's formally state what we're trying to prove:

For all integers y, z, we have multiply(y, z) = y · z.

For recursive algorithms, we usually want an induction proof. This requires us to select an induction quantity, which should decrease on every recursive call. Here, we can use |z|. The inductive proposition is

For all integers k ≥ 0, for all integers y, z such that |z| = k,
  we have multiply(y, z) = y · z.

The base case is when |z| = 0. This implies that z = 0, and we verify that multiply(y, z) = 0 (the if is taken) and y · z = y · 0 = 0.

The inductive cases are when |z| > 0. The else is taken, and since c ≥ 2, we know that |trunc(z / c)| < |z| and hence, by the inductive hypothesis, multiply(c · y, trunc(z / c)) = c · y · trunc(z / c). The return value is thus

  c · y · trunc(z / c) + y · (z mod c)
= y · (c · trunc(z / c) + c · (z / c - trunc(z / c)))
= y · (c · z / c)
= y · z,

as required.

Answer 2

By recursion on z.

We suppose it is true for every z < K then, it is true for K.

It is true if z=0 : multiply(y,z)=0 (rule 1).

Then it will be true for every K.

Case 1: z< c

then z/c =0, z%c=z

then multiply(y,z)=multiply(cy, z/c) + y · (z mod c)) (rule 2).

= multiply(cy, 0) + y · z = 0 + y . z = y . z TRUE

Case 2: z>=c

then z/c < z (because c>=2)

then multiply(y,z)=multiply(cy, z/c) + y · (z mod c)) (rule 2).

= cy . (z/c) + y . (z mod c) (RECURSION)

= y . (c . (z/c) + z mod c)

but c . (z/c) + z mod c = z (definition of mod)

then multiply(y,z)= y . z It is done.