2

我正在研究一些 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 <= n + 1) ，这样它就变成了：

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

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

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

4

1 回答 1

1

所以我想到的是在不变量中添加一个 (i <= n + 1) ，这样它就变成了：

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

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

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

Using i <= n is common practice when programming. In your particular program, you could just as well have written i != n+1 instead, in which case your first invariant (which indeed looks cleaner) would have sufficed since you get

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

which evidently holds.

于 2012-07-16T12:13:02.623 回答