从何处开始验证算法的正确性

Question

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

证明以下递归算法的正确性乘两个 自然数，对于所有整型常量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

让我们正式说明我们正在试图证明：

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, 

根据需要。

Answer 2

通过z上的递归。

我们假设这是真的，每Ž<ķ然后，它是K.

它为真，如果z = 0的情况：乘法（Y，Z）= 0（规则1）。

然后，它会是真实的每K.

案例1位：Z <Ç

则z/C = 0，Z％C = Z

然后乘以（ y，z）=乘（cy，z/c）+ y·（z mod c））（规则2）。

=乘（cy，0）+ y·z = 0 + y。 z = y。 žTRUE

案例2位：Z> = C

那么z/C < Z（因为C> = 2）

然后乘以（Y，Z）=乘法（CY，Z/c）+ y·（z mod c））（规则2）。

= cy。 （z/c）+ y。 （z mod c）（RECURSION）

= y。 （c。（z/c）+ z mod c）

但是c。（z/c）+ z mod c = z（mod的定义）

然后乘（y，z）= y。 z完成了。