2

私はいくつかのホーア論理に取り組んでいますが、私のアプローチが正しいかどうか疑問に思っています。

私は次のプログラムPを持っています：

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

これは、hoare triple {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 |

保持するには、iがn + 1であり、nより大きいiだけではないことを証明する必要があります。だから私が考えたのは、不変量に（i <= n + 1）を追加して、次のようにすることです。

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

そうすれば、プログラムを証明できるので、正しいはずだと思います。

それにもかかわらず、私は不変条件が少し、「不変条件」ではないことを発見しました:)。そして、これまでのコースや演習で見たものとは違うので、ここにもっとエレガントな解決策があるのだろうかと思いました。

4

1 に答える 1

1

だから私が考えたのは、 a (i <= n + 1) を不変式に追加して、次のようにすることです。

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

それにもかかわらず、不変条件は少し「不変」ではありません:)。そして、これまでのコースや演習で見たものとは違うので、もっとエレガントな解決策があるかどうか疑問に思っていましたか?

いいえ、コードが書かれている方法を考えると、それはまさに行くべき道です。(私は、2 つの異なるコースで数学期にわたってホーア論理を教えてきたので、それは私の大学院の研究の一部であるため、経験から言えます。)

を使用するi <= nことは、プログラミングの一般的な方法です。あなたの特定のプログラムでは、i != n+1代わりに書くこともできます.

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

これは明らかに成り立ちます。

于 2012-07-16T12:13:02.623 に答える