從何處開始驗證算法的正確性

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完成了。