循环不变量(特别是“加速C”的第3章)

我目前正在通过“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时,我们将读取计数1等级,因此不变量将是不真实的.同样,当我们增加计数器时,总和将不再是最后计数等级的总和(如果您没有猜到,这是计算学生分数的传统程序).

我不明白为什么这很重要.当然对于任何其他循环,类似的陈述是真的吗？例如,这是本书的第一个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使得不变量的第一部分 – 即我们已经读过计数等级 – 假.因此,我们必须改变我们的分析,以考虑条件本身可能对不变量产生的影响.

我们知道在评估条件之前,不变量是正确的,因此我们知道我们已经读过计数等级.如果cin>> x成功,然后我们现在读取计数1等级.我们可以通过递增计数再次使这一部分变为真.然而,这样做会伪造不变量的第二部分 – 即总和是第一个计数等级之和的部分 – 因为在我们增加计数之后,求和现在是第一个计数的总和–1个等级,而不是第一个等级计数等级.幸运的是,我们可以通过执行sum = x来使不变量的第二部分成立;这样整个不变量在随后的旅程中都是真实的.

如果条件为false,则意味着我们对输入的尝试失败,因此我们没有获得更多数据,因此不变量仍然为真.因此,我们不必在完成这一过程后考虑病情的副作用.“

解决方法

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

在这种情况下,唯一可能发生的方法是,如果std :: cout抛出异常,而不变量是不真实的,那么你会在某处捕获该异常但继续执行处于错误状态.在我看来,作者过于迂腐.所以,只要你在错误的地方没有任何break / continue语句或抛出异常,你就可以了.我怀疑很多人都会专注于你的示例代码,因为它只是如此简单.

原文地址：https://www.jb51.cc/c/114255.html