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 | 

這顯然成立。