Hoare逻辑，while循环与'<='

Question

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

我有以下程序P：

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

应该满足霍尔三重{N> = 0} p {S = N *（N + 1）/ 2}（因此它只是需要的和）。现在，最初我有| s = i *（i-1）/ 2 |作为我的不变，这工作正常。但是，我的循环结束时出现了一个问题，达不到我想要的后置条件。因为对于impliciation

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

持有，我需要证明我是N + 1，而不是任何我超过n大。因此，我认为是一个（我< = N + 1）添加到不变，使之成为：

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

然后，我可以证明的程序，所以我觉得应该是正确的。

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

Answer 1

因此，我认为是一个（我< = N + 1）添加到不变，使之成为：

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

尽管如此，我觉得不变的是一点点，“不变”:)。而且不像我在课程或练习中见过的任何内容，所以我想知道这里是否有更优雅的解决方案？

没有，鉴于代码的写法，这正是要走的路。 （由于我在两个不同的课程中已经在几个学期教授霍尔逻辑，并且因为它是我研究生学习的一部分，所以我可以从经验中看出来）。

使用i <= n在编程时被认为是很好的做法。然而，在你的特定程序，你也可以同样有书面i != n+1代替，在这种情况下，你第1不变（这的确看起来比较清爽）就足够了，因为你得到

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

这显然成立。