0

我试图为此代码编写循环不变量和后置条件：

sum = 0;
for (i = 0; i < 10; ++i)
  ++sum;

sum = 10是这里明显的后置条件。但是有朋友告诉我，这i = sum也是循环不变量，sum = 12也是后置条件。我检查了以下内容：

  • 循环不变量最初是正确的：这是正确的，i = sum因为两者最初都是 0
  • 循环不变量被保留：假设i < 10然后i = sum在一次迭代之后它仍然是真的++i = ++sum
  • 循环不变量意味着后置条件：假设i >= 10and i = sumthensum = 12也为真

但显然 sum 在这里不等于 12。那么我的推理有什么问题呢？

4

2 回答 2

3

取一个稍微不同的不变量i == sum && i <= 10。和你一起i >= 10搞定i = sum = 10。

顺便提一句。在您最初的推理中，您无法得出结论sum = 12是正确的，而只能得出结论sum >= 10。后者是正确的，只是不足以证明预期的结果。

于 2020-07-06T05:44:04.583 回答
1 
// Loop invariant SUM_IS_INDEX: sum == i
// Loop variant: i is increased in every step, and initial value 0 before 10.

sum = 0;
for (i = 0;
        // SUM_IS_INDEX      before the actual loop
        i < 10;
        // next loop step, after first step:
        // sum == index + 1
        ++i
        // next index = index + 1
        // sum == index
        // SUM_IS_INDEX      after a loop step, continuing
        ) {
    // SUM_IS_INDEX
    ++sum;
    // sum == index + 1
}
// Post: i >= 10 (negation of the for condition), SUM_IS_INDEX

关于 12 的评论与i. 要拥有i == 10一个，需要添加一个仅增量为 1 的谓词。

最佳实践是在控制流顺序中重写 for：

sum = 0;
i = 0;
while (i < 10)
    ++sum;
    ++i:
}

这可以防止愚蠢的错误。

于 2020-07-06T05:45:23.220 回答