Hoare Logic whileループwhile '<='

Question

私はいくつかのHoareのロジックに取り組んでいます。私のアプローチが正しいかどうかは疑問です。

Iは、次のプログラムPを有する：それだけかかるので、それは{（N + 1）/ 2、S = Nの*}（ホア三重{N> = 0} Pを満たさなければならない

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

を和）。今、私は最初に| s = i *（i-1）/ 2 |私のインバリアントとして、うまく動作します。しかし、私は自分のループの終わりまで、私の望む事後条件に行くことから問題を抱えていました。 impliciationため

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

を保持するので、私はiがn + 1であることを証明する必要はなく、ただのnよりも私は大きな。

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

その後、私は、私はそれが正しいことだと思いますので、プログラムを証明することができます：だから私は考えは、それがなるように、不変に（I < = N + 1）を追加することです。

しかし、私は不変式が少し、「不変」ではないことが分かります:)。私がコースや練習で見たことのないように、私はここにもっと洗練されたソリューションがあるのだろうかと思っていました。

Answer 1

それでは、私が考えることは、それがなるように、不変に（I < = N + 1）を追加することです：

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

それでも、私は不変であることを見つけます少し、 "不変的に"少ない:)。私がコースや練習で見たことのないように、私はここにもっと洗練されたソリューションがあるのだろうかと思っていました。コードが書かれている方法で与えられた

いやは、それは正確に移動するための方法です。 （私は2つの異なるコースで、それは私の大学院の研究の一部なので、いくつかの学期の間、ホーア論理を教えてきたので、私は経験から言うことができます。）

は、プログラミング時i <= nが良い方法と考えられている使用します。しかし、あなたの特定のプログラムでは、あなただけのようにもあなたは明らかに成り立つ

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

を取得するので、その場合、あなたの最初の不変を（確かにきれいに見えた）で足りているだろう、代わりにi != n+1を書かれている可能性があります。