2

我试图找到一个循环不变量,以便我们可以证明这个程序部分正确:

{ 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

我真的很感激一些建议。

4

1 回答 1

0

要找到合适的不变量,您必须对所研究的函数实际执行的操作有一个直觉。在您的示例中,该值i^2被连续添加到 accumulator 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

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

于 2013-07-29T03:47:58.947 回答