如何为这段代码找到最强的循环不变量？

Question

我正在尝试为以下 while 循环提出一个循环不变量，但遇到了一些麻烦。

确定循环不变量后，我想整理一个证明表并显示所有中间断言

ASSERT(k >= 0)
{i = 1;
 sum = 1;
 while (i <= k) { 
     sum = sum + 2*i + 1;
     i = i+1;
 } //end-while
}
ASSERT( sum == (k+1)*(k+1) )

Answer 1

INV(1) = {sum == (n+1)*(n+1)}  
INV(2) = {0<=n<=k}

sum = 1 适用于 n = 0
现在尝试证明它确实适用于 n+1（如果 n 为真），直到 n 达到 k（在你的情况下，我的 n 是你的 i）

Answer 2

注意，当循环存在时，i 的值为k+1，也就是说，似乎是一个很好的不变量：

INV(1) = {1 <= i <= k+1}

INV(2) = {sum == i*i}