霍尔逻辑，带有'<='的while循环答案

【问题标题】：Hoare Logic, while loop with '<= '霍尔逻辑，带有'<='的while循环
【发布时间】：2012-01-27 16:22:21
【问题描述】：

我正在研究一些 Hoare 逻辑，我想知道我的方法是否正确。

我有以下程序P：

s = 0
i = 1
while (i <= n) {
    s = s + i
    i = i + 1
}

它应该满足 hoare 三元组 {n >= 0}P{s = n*(n+1)/2} （所以它只需要总和）。现在，最初我有 |s = i*(i-1)/2|作为我的不变量，效果很好。但是，从循环结束到我想要的后置条件，我遇到了问题。因为为了暗示

|s = i*(i-1)/2 & i > n|
=>
| s = n * (n+1) / 2 |

为了保持，我需要证明 i 是 n+1，而不仅仅是任何大于 n 的 i。所以我想到的是在不变量中添加一个 (i

|s = i * (i-1)/2 & i <= n+1|

然后我可以证明这个程序，所以我认为它应该是正确的。

尽管如此，我发现不变量有点“不变量”:)。而且不像我目前在课程或练习中看到的任何东西，所以我想知道这里是否有更优雅的解决方案？

【问题讨论】：

【解决方案1】：

所以我想到的是在不变量上加一个 (i
|s = i * (i-1)/2 & i <= n+1|
尽管如此，我发现不变量有点“不变量”:)。而且不像我目前在课程或练习中看到的任何东西，所以我想知道这里是否有更优雅的解决方案？

不，鉴于代码的编写方式，这正是要走的路。（我可以从经验中看出，因为我在两个不同的课程中教了几个学期的 Hoare 逻辑，而且这是我研究生学习的一部分。）

使用i <= n 是编程时的常见做法。在您的特定程序中，您也可以改写i != n+1，在这种情况下，您的第一个不变量（确实看起来更干净）就足够了，因为您得到了

| s=i*(i-1)/2 & i=n+1 |
=>
| s=n*(n+1)/2 |

显然成立。

【讨论】：