我试图找到一个循环不变量,以便我们可以证明这个程序部分正确:
{ 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
我真的很感激一些建议。