loops - 了解循环不变式。寻找并证明它们的算法

Question

我需要一些帮助来理解循环不变式。我只需要有人解释如何找到循环不变式并为以下算法证明它:

public int sumSquares ( int n )
{
    int sum = 0 ;
    for ( int i = 1 ; i <= n ; i++)
    {
        sum += i ∗ i ;
    }
    return sum ;
}

Answer 1

循环不变量是在循环的每次迭代之前和之后都可证明为真的语句。事实证明有很多这样的方法，但关键是证明其中一个确实有帮助。

例如，确实如此

the value of i is always equal to i before and after each iteration.

不是很有帮助。相反，想想你想证明什么

When i is equal to n, sum is equal to the sum of the first n squares

在这种情况下，如果您想证明您的算法产生前 n 个平方的和，您需要声明以下不变量。对于每个i，

The value of sum is equal to the sum of the first i squares