循環不變的證明部分正確性

Question

我試圖找到一個循環不變，這樣我們可以證明這個節目部分糾正：

{ n >= 1 } pre-condition 
i = 1; 
z = 1; 
while (i != n) { 
    i = i + 1; 
    z = z + i*i; 
} 
{ z = n*(n+1)*(2*n + 1)/6 } post-condition 

我很堅持。一些到目前爲止，我已經試過不變的是：

z <= n*(n+1)*(2*n + 1)/6^i <= n 

和

z = i*(i+1)*(2*i + 1)/6^i <= n 

我真的很感激一些建議。

Answer 1

要找到一個適當的不變量，你必須有一個直覺，調查功能實際上做了什麼。在您的示例中，值i^2被連續添加到累加器z。因此，函數計算（只是要通過手，然後推廣的while循環的前幾個迭代）：

1^2 + 2^2 + 3^2 + 4^2 + 5^2 + ... + n^2 

或書面略偏正式

SUM_{i=1}^{n} i^2 

即所有的總和i的正方形範圍從1到n。

初看起來，這可能看起來不像你的後置條件。但是，它可以通過感應被顯示在n，上述總和等於

(n*(n+1)*(2*n + 1))/6 

我的猜測是預期的後置條件。既然我們現在知道後置條件等於這個總和，那麼應該很容易從總和中讀出不變量。