Hoare Logic, а цикл с «<=» - PullRequest
Новая
       21

Hoare Logic, а цикл с «<=»

1 голос
/ 27 января 2012

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

У меня есть следующая программа 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 | как мой инвариант, который отлично работает. Тем не менее, у меня была проблема от перехода к концу цикла до желаемого постусловия. Потому что за значение 

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

чтобы удержаться, мне нужно доказать, что я есть n + 1, а не просто я больше n. Итак, я подумал о том, чтобы добавить (i <= n + 1) к инварианту, чтобы он стал: </p> 

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

Тогда я могу доказать программу, поэтому я думаю, что она должна быть правильной.

Тем не менее, я считаю, что инвариант немного, менее "инвариантно" :). И не то, что я видел в курсе или в упражнениях до сих пор, поэтому мне было интересно, было ли здесь более элегантное решение?

1 Ответ

0 голосов
/ 16 июля 2012

Итак, я подумал о том, чтобы добавить (i <= n + 1) к инварианту, чтобы он стал: </em>

|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 |

что, очевидно, верно.

...