1

質問は：

        P1 {C} Q1
-------------------------
   P1 && P2 {C} Q1||Q2

このルールは有効ですか?

このようなことに取り組むにはどうすればよいでしょうか。私が考えることができるのは、それが偽になる例を見つけようとすることだけです.

P1 && P2 の組み合わせが Q1 と Q2 の両方を偽にするように考えてみましたが、何も考えられません。したがって、これが有効であることに傾いていますが、それを証明する場所がわかりません...このクラスのテキストは絶対にゴミであり、正しさのステートメントの組み合わせに関するリソースをオンラインで見つけることができません...

4

1 に答える 1

2

これらは通常は{P} C {Q};で表されるホーアトリプルであると想定しています。ウィキペディアも参考にしています。

だからあなたのルール：

      {P1} C {Q1}
-----------------------
{P1 && P2} C {Q1 || Q2}

有効です！

直感的に、ロジックを理解していないかどうかは非常に明確です。

  • {P1} C {Q1}意味：ホールドするときはいつでもP1、Q1コマンドの実行後にホールドしCます。
  • P1 && P2あなたは、もし成り立つなら、成り立つことを知っていP1ます。
  • Q1あなたは、もし成り立つなら、成り立つことを知っていQ1 || Q2ます。

これらのステートメントをつなぎ合わせて、ルールが有効である必要がある理由を確認できます。つまり、を実行すると、仮定によって取得されます。これは、を意味P1 && P2します。P1CQ1Q1 || Q2

したがって{P1 && P2} C {Q1 || Q2}、あなたが仮定するときはいつでも{P1} C {Q1}、それはまさにあなたのルールが述べていることです。

正式には、次のルールを使用できます（ウィキペディアからの抜粋）。

結果ルール

P' -> P, {P} C {Q}, Q -> Q'
---------------------------
        {P'} C {Q'}

ここで、単に、P'として、として、そして最後にとして設定します。P1 && P2PP1QQ1Q'Q1 || Q2

于 2012-04-03T22:27:05.713 に答える