よくわかりません
{ true } x := y { x = y }
は有効なHoare トリプルです。
変数 (この場合はy) を参照することが許可されているかどうかはわかりませんが、最初にトリプル プログラム本体または事前条件で変数を明示的に定義する必要があります。
{ y=1 } x := y { x = y } //valid
{true} y := 1; x := y { x = y } //valid
どうですか？
質問する
1138 次
3 に答える
6
よくわかりません
{ true } x := y { x = y }有効なHoareトリプルです。
トリプルは次のように読む必要があります。
「開始状態に関係なく、x:=yxを実行した後はyに等しくなります。」
そしてそれは成り立ちます。それが成り立つ理由の正式な議論はそれです
x := y与えられた事後条件の最も弱い前提条件{ x = y }は{ y = y }、、{ true }を意味し{ y = y }ます。
しかし、なぜこのトリプルに不安を感じるのかは完全に理解しており、正当な理由で心配しています！
前後の条件が有用な仕様を提供しないため、トリプルは不適切に定式化されています。なんで？なぜなら（あなたが発見したように）実行後にも保持さx := 0; y := 0れるので、仕様も満たしているからです。x = y
明らかに、x := 0; y := 0これはあまり有用な実装ではなく、それでも仕様を満たしている理由は、（私によれば）仕様のバグによるものです。
これを修正する方法：
仕様を表現する「正しい」方法は、プログラムがアクセスできない（この場合は）いくつかのメタ変数を使用して、仕様が自己完結していることを確認することです。x₀y₀
{ x=x₀ ∧ y=y₀ } x := y { x=y₀ ∧ y=y₀ }
ここでx := 0; y := 0は、post条件を満たしていません。
于 2012-06-01T09:01:36.560 に答える
1
{ true } x := y { x = y }は有効な Hoare トリプルです。その理由は次のとおりです。
x := yは割り当てであるため、前提条件でそれを置き換えます。
前提条件は で{y=y}あり、これは を意味し{true}ます。
つまり、{y=y} => {true}.
于 2011-11-28T22:49:22.437 に答える
-2
* x:=y の場合、QQED _ *
于 2011-10-02T21:04:52.493 に答える