证明部分正确性的循环不变量

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

我猜这是预期的后置条件。由于我们现在知道后置条件等于这个总和，所以应该很容易从总和中读出不变量。