問題タブ [hoare-logic]

次が正しいことを証明せよ。

次の推論規則が役立ちます

明確な説明または少なくとも従うべき例を求めてウェブ全体を探していましたが、よくわかりません。以下に役立つ可能性のあるサイトをいくつか見つけましたが、例はありません。

148～160ページ

どんな助けでも大歓迎です。この問題を解決して他の問題を解決できるようにしたいと思います。非常に行き詰まっており、この本には例がありません。

これらのリンクも役立つ場合があります。ありがとう、10ポイント！

http://en.wikipedia.org/wiki/Hoare_logic#Conditional_rule

ウィキペディアがリストするループ不変条件を考えると、ループの最も弱い前提条件を生成する良い方法 ( http://en.wikipedia.org/wiki/Predicate_transformer_semanticsから):

M[x <- N] は、M 内のすべての x を N に置き換えます。

さて、私の問題は変数 y です。\forall y, は式で y をバインドするため、「y は新しい変数のタプルです」は解析されません。"[x <- y]" の y と同じように、y は \forall でバインドされていますか? 上記を解析することはできません。

編集：参照要求を避けるために言い換えました。

私の質問は、ループ不変条件と最も弱い前提条件の計算との間の直接的な関係は何かということです。実際に行われている多くのことは、ループの最も弱い前提条件を検証に適した前提条件に緩和しているようです。ウィキペディアの上記は、ループ不変条件が与えられた場合、鼻の最も弱い前提条件を実際に計算できることを示唆していますが、この条件を理解するのに苦労しています。

Hoare Logicを使用するまで、プログラムを繰り返し証明するにはどうすればよいですか?

次のようなルールを見つけました。

{P} の場合、B {Q} まで S を繰り返す

しかし、このルールをどのように使用できるかについての説明はまだ見つかりません

たとえば、この質問では：

ルールを使用してこのプログラムを証明するにはどうすればよいですか?

ループ不変式を見つけて証明するプログラムがあります。

私にとって唯一の論理ループの不変は ですres<=x*y。これは事後条件から簡単ですが、続けるのが最善だとは思いません。多分他の提案はありますか？

次の問題があります: 前提条件が True

私が考えているバリアントは次のとおりn-iです。ただし、ユーザーが負の値を指定するのを止めるものは何もないと思います。その場合、バリアントは負になります(定義と矛盾します)。

不変量を |n| として指定することは可能ですか? - i、または前提条件として n>=0 を含める必要がありますか?

どんな助けや提案も大歓迎です。

私は論理の世界に不慣れです。Hoare Logic と、プログラムの部分的および全体的な正しさを学んでいます。以下の質問を解決するために多くのことを試みましたが、失敗しました。

私の友人の一人が私に次の答えをくれましたが、それが正しいかどうかはわかりません.

この問題の解き方を順を追って教えてください。

それをよりよく理解するために、独自のhoareパーティション関数を作成しようとしています。私はその定義と擬似コードにうまく従ったと思っていましたが、多くの場合期待どおりに動作しているように見えますが、pivot に等しい複数の値を持つリストが渡されるとバラバラになり、無限ループに陥ります。私の間違いはどこですか?バグを修正するには、これをどのように変更すればよいですか?