寻找循环不变量 - Hoare Triple答案

【问题标题】：Finding a loop invariant - Hoare Triple寻找循环不变量 - Hoare Triple
【发布时间】：2018-04-15 16:13:22
【问题描述】：

从下面的代码中，我需要推断/选择一个循环不变量。

(|true|)
x = 0 ;
s = 0 ;
while ( x <= n ) {
    s = s + x ;
    x = x + 1 ;
}
(|s = n(n + 1)/2|)

给出的解决方案是

s = (x-1)*x/2 ∧ (x ≤ n +1)

我不太明白它是如何达到上述解决方案的。

请帮助我了解如何从代码中推导出此类解决方案或其他循环不变量。

【问题讨论】：

似乎有多个拼写错误。最后一个1)=2 应该是1)/2，并且在你的不变量公式中，我希望它以s = (x+1) 而不是0 = (x-1) 开头。你能确认和编辑吗？
您好@tucuxi 感谢您指出这些错误。是的，我编辑了那些。在我的 pdf 文件中，它说 0 = (x-1)，但这没有意义。应该是 s，我同意你的看法。
明白了。我修好了:) @tucuxi
但就在循环终止之前，x+=1;它将是 x = n+1。那么 n = x-1。当用 x 项替换 n 时，不应该是 (x-1)*x/2 吗？ @tucuxi
糟糕。显然我走在了前面。 x-1 没问题（结束循环时，x-1 计算结果为 n；所以 x）。很抱歉增加了混乱。

标签： while-loop logic predicates loop-invariant hoare-logic

【解决方案1】：

鉴于不变量，您可以在循环之前、内部和之后轻松检查它是否为真（是的，将 1 到 n 的整数相加得到 (n+1)*n/2 - 请参阅 triangular numbers ）。由于它涵盖了循环中的所有相关变量（x 和 s），并且无法进一步细化（好吧，您可以添加^ x >= 0），它确实是 /em> 不变的。

要自己推导，恐怕你需要事先了解三角数（或半平方）的公式。你当然可以为那部分写出s = sum of integers from 1 to x，我认为它是一个有效的不变量。 x <= n+1的部分比较简单。

外行寻找不变量的方法是尝试写出循环中的变量在其生命周期内在循环中所做的事情：

s 始终保存不超过 x 的整数之和
x 遍历从 0 到 n 的整数，包括 0 到 n

然后用数学写出来。

【讨论】：

哇，感谢您的快速反馈和答复。我现在明白为什么选择这个不变量了。