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

我刚开始阅读算法设计手册，发现很难掌握如何证明算法的正确性。有人可以通过解释我提供的示例问题来帮助我。

对于所有整数常量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))

David Eisens.. 5

让我们正式说明我们要证明的内容：

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.

基本情况是when |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,

按要求。

让我们正式说明我们要证明的内容：

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.

基本情况是when |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,

按要求。