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

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

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

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

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