Hoare Logic, while loop with '<='

Question

Я работаю над некоторой логикой Hoare, и мне интересно, подходит ли мой подход.

У меня есть следующие программы P:

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

Она должна удовлетворять Хоаром тройка {п> = 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 | 

держать, мне нужно, чтобы доказать, что я есть п + 1, а не просто я больше чем п. Так что я думал, чтобы добавить (я < = п + 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 вместо этого, в этом случае ваш первый инвариант (который действительно выглядит чище) хватило бы, так как вы получите

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

, который, очевидно, имеет место.