循环不变量（特别是“Accelerated C++”的 Ch.3）

Question

我目前正在学习“加速 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< 之前，不变式肯定为 false。 /code>，就像另一个例子一样吗？

这两个条件有何不同？

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

原始段落，如下所示：

“理解此循环的不变量需要特别小心，因为 while 中的条件有副作用。这些副作用会影响不变量的真实性：成功执行 cin >> x 使第一个不变量的一部分——表示我们已经读取了计数等级的部分——因此，我们必须改变我们的分析，以考虑条件本身可能对不变量产生的影响，

在评估之前我们知道不变量是正确的。条件，所以我们知道，如果 cin >> 成功，那么我们现在已经读取了 count + 1 个等级，但是，这样做可以使这部分不变。伪造了不变量的第二部分 - 该部分表示 sum 是第一个计数成绩的总和 - 因为在我们递增计数之后，sum 现在是第一个计数 - 1 个成绩的总和，而不是第一个计数成绩。 ，我们可以通过执行 sum += x; 使不变量的第二部分为真；这样整个不变量在随后的 while 旅行中都是正确的。

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

Answer 1

我相信这本书指的是 while 循环停止的方式。在第二种情况下，很容易看出，一旦“r”增加到足以等于“行”，循环就会停止。因为 C++ 中的大多数计数都是从零开始的，所以很可能会为每一行输出一行。

另一方面，第一个示例是使用“>>”的运算符重载在 cin 对象上。只要该函数不返回零，while 循环就会继续。在输入关闭之前，该运算符重载不会返回该值。

按什么键可以发出“cin>>”返回0？否则循环将永远不会结束。您需要确保不会创建这样的循环。

需要添加一行来停止条件之外的循环。查找“break”和“continue”语句。

Answer 2

在异常安全的背景下，这确实很有趣/很重要。

考虑以下场景：

• “count”是一个用户定义的类，具有重载的 operator++ ，
• 重载的 operator++ 会引发异常。
• 稍后在循环外部捕获异常（即循环看起来像现在一样，没有 try/catch）

在这种情况下，循环不变式不再成立，并且循环中发生的所有事情的状态都存在问题。行写了吗？计数更新了吗？总数仍然正确吗？

需要使用一些额外的保护（以临时变量的形式来保存中间值和一些 try/catch），以确保即使抛出异常，一切也保持一致。

Answer 3

这本书似乎使事情变得比应有的复杂得多。我真的不认为用不变量解释循环是一件好事。这有点像用量子物理学解释加法。

作者接着解释说，不变量需要特别注意，因为当输入读入变量 x 时，我们将读取 count+1 级，因此不变量将不真实。类似地，当我们增加计数器时，变量 sum 将不再是最后计数成绩的总和（如果您没有猜到，这是计算学生分数的传统程序）。

首先，不变量不明确。如果不变量是“在 while 循环迭代结束时，我们已经读取了 count 成绩以及 sum 的总和”，那么这对我来说看起来是正确的。不变量没有明确指定，因此讨论它何时受到尊重和不被尊重是没有意义的。

如果不变量是“在 while 循环迭代的任何点，我们已经读过...”，那么严格来说，该不变量将不为真。就循环而言，我认为不变量应该指的是循环中开始、结束或固定点处存在的状态，

我没有那本书，我不知道事情是否得到澄清，但似乎是。如果它们的不变量不正确，为什么还要费心使用不变量呢？

只要您了解这些循环的工作原理，就可以了。如果你想通过不变量来理解它们，你可以，但是你必须注意你选择的不变量，否则它就达不到目的了。你应该选择一个易于编写代码的不变量。尊重它，而不是随机选择一个，然后努力编写尊重它的代码，并且绝对不要选择一个模糊的代码并编写与它无关的代码，然后说“必须注意，因为这不实际上尊重我选择的模糊不变量”。

我不明白为什么这很重要。对于任何其他循环，类似的陈述肯定是正确的吗？

这取决于所使用的不变量（从你所说的来看，这本书对此相当模糊），但是是的，在这种情况下你似乎是正确的。

对于这段代码：

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

“在 while 循环迭代结束时，我们已经写入了 r 行”这个不变式肯定是正确的。

我没有这本书，所以我不知道这些事情以后是否都会解决。从你所说的来看，这似乎是解释循环的一种非常糟糕的方式。

Answer 4

我同意你必须知道不变量是什么。假设我正在编写良好的旧 BankAccount。我可以说，任何时候，交易历史中所有交易的总和都会加起来就是账户的余额。这听起来很明智。如果这是真的那就太好了。但在我处理交易的几行代码中，事实并非如此。要么我先更新余额，要么我将交易添加到历史记录中并更新余额。暂时这个不变量并不成立。

我可以想象一本书希望你明白，不变量是你声称始终且始终为真的东西，但有时并非如此，并且最好知道它何时不为真，因为如果你返回，或者抛出异常，或者屈服于并发，或者其他什么，当它不正确时，那么你的系统就会一团糟。有点难以想象你的释义就是作者想要表达的意思。但我想如果我把头转向一边并眯着眼睛，我可以将其重新表述为“总和是第一个计数成绩的总和”始终是正确的，除了当我们忙于阅读和添加它们时 - 它可能不是在此过程中是正确的。有道理吗？

Answer 5

在您更新之后，作者正确地描述了如何在循环的每次迭代中“恢复”循环不变量。

我不明白为什么这很重要。当然，对于任何其他循环，类似的陈述都是正确的吗？

是的，确实如此——这个循环没有什么特别的（好吧，循环条件有一个副作用，但这可以很容易地重写）。

但我认为作者想要指出的重要事实是：在循环内执行操作后，循环不变式通常不再为真。这对于不变式来说当然是一个问题，除非后续语句通过采取适当的操作来纠正这个问题。

Answer 6

在第一个示例中，计数变量除了为每个输入循环递增之外没有用于任何其他用途。循环将继续直到>>返回 NULL。

在第二个示例中，必须使用要写入的行数来初始化行。循环将继续，直到写入指定的行数。

while (cin >> x) {
    ++count;
}


rows = NROWS;
r = 0;

while (r != rows) {
    // write a row of output 
    std::cout << std::endl;
    ++r;
}

Answer 7

一般来说，不变量被理解为仅适用于循环的迭代之间。 （至少我是这么读的！）

一般情况是这样的：

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

但是在状态转换期间，你的不变量不一定成立。

作为一个单独的风格注释：如果你想成为一名超级编码员，不要将不变量留在注释中，而是将它们设为断言！

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

这样你就有了自检代码。

Answer 8

从你的描述看来，作者是在胡说八道。是的，不变量在指令之间暂时变得不真实，但是只要有这样的非原子操作，这种情况就会发生。只要没有任何明显的断点可能导致不变量不正确并且程序处于不一致的状态，就可以了。

在这种情况下，唯一可能发生的情况是，如果 std::cout 在不变量不正确时抛出异常，那么您会在某处捕获该异常，但会继续以错误状态执行。在我看来，作者过于迂腐了。再说一次，只要您没有在错误的位置有任何中断/继续语句或抛出异常，就可以了。我怀疑很多人会费心关注您的示例代码，因为它是如此简单。