为什么这个不变性会变成假的

Why does this invariant become false?

本文关键字：不变性 为什么      更新时间：2023-10-16

在阅读加速 c++ 时，我对为什么不变变为 false 的解释感到困惑（参见下面的代码）：

作者（在本例中）将不变量定义为：

我们的不变性是到目前为止我们已经编写了 r 行输出。当我们定义 r 时，我们给它一个初始值 0。在这一点上，我们根本没有写任何东西。将 r 设置为 0 显然使不变为真，因此我们满足了第一个要求。

// invariant: we have written r rows so far
int r = 0;
// setting r to 0 makes the invariant true
while (r != rows) {
    // we can assume that the invariant is true here
    // writing a row of output makes the invariant false <- WHY?
    std::cout << std::endl;
    // incrementing r makes the invariant true again
    ++r;
}   
// we can conclude that the invariant is true here

然后后来解释...

写入一行输出会导致不变量变为 false，因为 r 不再是我们写入的行数

鉴于定义，我无法在两者之间建立联系。

为什么在写入一行输出时不变量变为 false？

r定义为

已打印的行数。 因此，只有在以下情况下，不变性才为真

r == number of rows that have been printed

在打印行和递增r以更新到目前为止打印的行数之间，该不变性是不正确的。

r等于某个数字（例如，n），并且"已打印的行数"比该数字（n + 1）大一个，因为您刚刚打印了一行。 因此，不变性是不正确的，因为n != n + 1 .

到目前为止，我们已经编写了 R 行输出

r从 0 开始，在cout为 r 的点处仍然是 0。cout写了 1 行，但r是 0。因此，不变性暂时为假，因为如果您在上面的语句中插入 r 的值，则"到目前为止我们已经写出了 0 行输出"是不真实的。

递增r会导致不变性再次变为 true。

相关文章：