algorithm - 证明算法正确性时从何处开始

我刚刚开始阅读算法设计手册，发现很难掌握如何证明算法的正确性有人能帮我解释一下我提供的例题吗？
证明以下递归算法乘二的正确性
自然数，对于所有整数常数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))

最佳答案

让我们正式声明我们要证明的是：

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

对于递归算法，我们通常需要一个归纳证明这要求我们选择一个归纳数量，在每次递归调用时应该减少。在这里，我们可以使用|z|。归纳命题是

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

基本情况是当|z| = 0时。这意味着z = 0，我们验证multiply(y, z) = 0（取if）和y · z = y · 0 = 0。
当|z| > 0时为诱发病例取else，由于c ≥ 2，我们知道|trunc(z / c)| < |z|，因此，通过归纳假设，multiply(c · y, trunc(z / c)) = c · y · floor(z / c)。因此，返回值是

  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,

根据需要。