6

我目前正在研究“加速 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 使得不变量的第一部分 - 表示我们已经读过count Grades-false。因此，我们必须改变我们的分析来考虑条件本身可能对不变量产生的影响。

我们知道在评估条件之前不变量为真，因此我们知道我们已经阅读了计数等级。如果 cin >> x 成功，那么我们现在已经读取了 count + 1 个等级。我们可以通过增加计数使这部分不变量再次为真。但是，这样做会篡改不变量的第二部分——即 sum 是第一个 count 等级的总和的部分——因为在我们增加 count 之后，sum 现在是第一个 count 的总和 - 1 个等级，而不是第一个计算成绩。幸运的是，我们可以通过执行 sum += x; 使不变量的第二部分为真。这样整个不变量将在随后的旅程中为真。

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

4

8 回答 8

4

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

一般情况如下：

[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!
}

这样你就有了自检代码。

于 2010-05-29T18:11:46.183 回答
2

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

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

于 2010-05-29T18:07:20.857 回答
2

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

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

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

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

于 2010-05-29T18:11:07.123 回答
2

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

考虑以下场景：

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

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

需要使用一些额外的保护（以临时变量的形式保存中间值和一些尝试/捕获）以确保即使在抛出异常时一切都保持一致。

于 2010-05-29T18:14:12.707 回答
1

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

作者通过解释不变量需要特别注意这一点，因为当输入被读入变量 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行”绝对是正确的。

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

于 2010-05-29T18:23:37.680 回答
1

我同意你必须知道不变量是什么。假设我正在写旧的 BankAccount。我可以说，无论何时何地，交易历史中所有交易的总和都会加起来账户的余额。这听起来很明智。最好是真的。但是在我处理事务的那几行中，这不是真的。我要么先更新余额，要么将交易添加到历史记录并更新余额。有那么一刻，不变量不是真的。

我可以想象一本书希望你明白，不变量是你一直声称是真实的东西，但有时不是，知道什么时候不真实是很好的，因为如果你返回，或抛出异常，或屈服于并发，或其他任何事情，当它不是真的时，那么你的系统就会一团糟。很难想象你的释义是作者想要表达的意思。但我想如果我侧头斜视，我可以改写为“总和是第一个计数成绩的总和”始终是正确的，除非我们正忙于阅读和添加它们 - 它可能不是在那个过程中是真的。有道理？

于 2010-05-29T18:49:01.103 回答
1

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

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

是的，这是真的——这个循环没有什么特别的（好的，循环条件有副作用，但很容易重写）。

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

于 2010-05-29T19:30:46.243 回答
0

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

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

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


rows = NROWS;
r = 0;

while (r != rows) {
    // write a row of output 
    std::cout << std::endl;
    ++r;
}
于 2010-05-29T23:22:46.067 回答