这个循环不变量和后置条件是否正确？答案

【问题标题】：is this loop invariant and post condition correct?这个循环不变量和后置条件是否正确？
【发布时间】：2020-07-06 05:27:37
【问题描述】：

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

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 >= 10 和i = sum 然后sum = 12 也为真

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

【问题讨论】：

for 循环的工作方式确保i = 10 不仅仅是i >= 10 在循环之后。
@henry 我认为 Hoare 逻辑声明“假设循环条件不再为真并且循环不变量为真，那么后置条件为真。”在这种情况下，“循环条件不再为真”意味着 !(i = 10?

标签： algorithm invariants hoare-logic

【解决方案1】：

取一个稍微不同的不变量i == sum && i <= 10。再加上i >= 10，你就会得到i = sum = 10。

顺便说一句。在您最初的推理中，您不能断定sum = 12 是真的，而只能是sum >= 10。后者是正确的，只是不足以证明预期的结果。

【讨论】：

【解决方案2】：

// 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:
}

这可以防止愚蠢的错误。

【讨论】：