c++ - 循环不变量(特别是 "Accelerated C++"的第 3 章)

Question

我目前正在学习“Accelerated C++”，只是在第 3 章中遇到了这个问题:

// invariant:
//  we have read count grades so far, and
//  sum is the sum of the first count grades
while (cin >> x) {
    ++count;
   sum  +=  x;
}

作者随后解释说，需要特别注意不变量，因为当输入被读入 x 时，我们将读取 count + 1 等级和因此不变量将是不真实的。同样，当我们递增计数器时，sum 将不再是最后计数成绩的总和(如果您没有猜到，它是计算学生分数的传统程序)。

我不明白为什么这很重要。对于几乎任何其他循环，类似的陈述肯定是正确的吗？例如，这是本书的第一个 while 循环(输出稍后填写):

// invariant: we have written r rows so far
while (r != rows) {
    // write a row of output 
    std::cout << std::endl;
    ++r;
}

一旦我们编写了适当的输出行，在我们递增 r 之前，不变量肯定是假的，就像在另一个例子中一样？

是什么让这两个条件不同？

编辑:感谢您的所有回复。 我想我已经明白了，但在我选择一个“已接受的答案”之前，我会把它放久一点，只是为了确定。到目前为止，所有的回复基本上都同意，所以很难看起来很公平，但我想值得一试。

原始段落，如下要求:

“理解这个循环的不变量需要特别小心，因为 while 中的条件有副作用。那些副作用会影响不变量的真实性:成功执行 cin >> x 使不变量的第一部分 - the 部分这表明我们已经读取了 count grades-false。因此，我们必须更改我们的分析以说明条件本身可能对不变量产生的影响。

我们知道在评估条件之前不变量为真，所以我们知道我们已经读取了计数等级。如果 cin >> x 成功，那么我们现在已经读取了 count + 1 个成绩。我们可以通过递增计数使这部分不变量再次为真。然而，这样做会伪造不变量的第二部分——表示 sum 是第一个 count 成绩总和的部分——因为在我们增加 count 之后，sum 现在是第一个 count 的总和 - 1 个成绩，而不是第一个算成绩。幸运的是，我们可以通过执行 sum += x; 使不变量的第二部分为真。这样整个不变量在这段时间内的后续行程中都为真。

如果条件为假，则意味着我们的输入尝试失败，因此我们没有获得更多数据，因此不变量仍然为真。因此，我们不必考虑 while 结束后条件的副作用。”

Answer 1

一般来说，不变量被理解为仅适用于循环的迭代之间。 (至少我是这样读的!)

一般情况是这样的:

[invariant true];
while (keep going) {
    [state transformation];
    [invariant true];
}

但是在状态转换过程中，你的不变量不一定成立。

作为一个单独的风格注释:如果你想成为一名 super 编码员，与其将不变量留在注释中，不如将它们变成断言!

// Loop invariant: x+y = -4
for (int x = 0; x < 10; x++) {
    [do something];
    assert(x+y == -4);  // Loop invariant here!
}

这样你就有了自检代码。