此循环不变和后置条件是否正确?

Question

我试图为这段代码编写一个循环不变和发布条件：

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也是真的

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

Answer 1

取一个稍微不同的不变i == sum && i <= 10。连同i >= 10你得到然后i = sum = 10.

顺便说一句，在你的原始推理中，你不能断定sum = 12是正确的，而只能断定sum >= 10。后者是正确的，只是不够强大，无法证明预期的结果。

Answer 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 in 控制流顺序：

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

这可以防止愚蠢的错误。