是否需要在循环前后都定义循环不变量？

Question

到目前为止，我一直对循环不变量及其特定属性感到困惑。它们是否需要在循环之前和之后都为真？或者只是在循环体本身的某个点？

例如：

int sum = 0;
for (int = 0; i < 10; i++) {
    sum += i
}

不变量是总和等于 0 + 1 + 2 + ... + i。您可以说在第二次迭代结束时 i = 1，sum = 1。这行得通，但不变量也需要在迭代开始时有效 - 但事实并非如此。在循环开始之前总和为 0，违反了该不变量。对吗？

Answer 1

循环不变量不属于整个循环，而是属于循环中的一个特定点。你会写一个循环不变式，它在总和增加之前为真，一个在总和增加之后为真，一个在 i 增加之后为真。

当你遍历循环的语句时，你会得到不同的不变量。当您重新进入循环时，循环结束处的那个应该导致循环开始处的那个正确。

Answer 2

是的，循环不变式需要在循环之前和之后都定义并为真。

这是完整的注释代码。为清楚起见，我们已将 for 循环转换为 while。我们定义一个空和 (i-1<0) 为 0:

int sum = 0;
// sum == 0
int i= 0;
// Loop invariant: sum == 0 + 1 + ... i-1
while (i < 10) {
    // Loop invariant: sum == 0 + 1 + ... i-1
    sum += i;
    // sum == 0 + 1 + ... i
    i++;
    // Loop invariant: sum == 0 + 1 + ... i-1
}
// Loop invariant: sum == 0 + 1 + ... i-1, and i == 10 => sum == 0 + 1 + ... 9

如你所见，循环不变量是sum == 0 + 1 + ... i-1。它在循环之前（平凡地）建立，在循环中修改然后恢复，在循环之后为真。与循环退出条件(i == 10)一起保证正确性(sum == 45).

是否需要在循环前后都定义循环不变量？

Does a loop invariant need to be defined both before and after the loop?

algorithm

code-analysis

loops