問題タブ [hoare-logic]

よくわかりません

は有効なHoare トリプルです。

変数 (この場合はy) を参照することが許可されているかどうかはわかりませんが、最初にトリプル プログラム本体または事前条件で変数を明示的に定義する必要があります。

どうですか？

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

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

これは、hoare triple {n> = 0} P {s = n *（n + 1）/ 2}を満たす必要があります（したがって、合計が必要です）。さて、最初は| s = i *（i-1）/2|でした 私の不変条件として、これはうまく機能します。しかし、ループの最後から希望の事後条件に至るまで、問題が発生しました。含意のために

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

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

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

誰かがこの質問に答えるのを手伝ってくれるかどうか疑問に思っていました. これは以前の試験用紙からのものであり、今年の試験の準備ができている答えを知っていればできることです。

この質問は非常に単純に思えて、完全に道に迷ってしまいます。正確には何を求めているのでしょうか?

整数変数を含むコードの次のセクションを検討してください。

適切な出力条件を記述し、コード片の正確性を検証することにより、実行後に m が i と j の最小値に等しいことを証明します。

私は投稿条件を次のように持っています: {m = i ∧ i < j ∨ m = j ∧ j < i}

これは正しいです？そして、これをどのように確認しますか？

配列を入力として受け取り、最初の要素をピボットとして分割する Hoare 分割関数を作成しようとしています (median-of-mediansアプローチのようにランダム化されたピボットを使用する必要があることはわかっています)。問題は、この関数が配列のように最初の要素が最大のときに無限ループに陥ること[14,6,8,1,4,9,2,1,7,10,5]です。outer の最初の繰り返しの後while、両方とも10iにj等しいため、エラーが表示されるため、ループは永遠に続きます。望ましい効果を得るには、どの部分を修復すればよいですか? コードは次のとおりです。

多くの Web サイトで提供されている疑似コードに従って、私はこのHoare分割アルゴリズムを作成しました。これは、指定されたピボットに基づいて分割されるサブ配列の開始インデックスと終了インデックスである配列を取ります。それは正常に動作しますが、誰かがロジックを説明できますか? コードは次のとおりです。

パーティショニングの別の変形であるLomutoアルゴリズムがあります。Hoareそもそもアルゴリズムを理解していないため、違いを見つけることはできませんが、似たようなことを行います。アルゴリズムで何が起こっているのか、どのケースでどちらがより良いパフォーマンスを発揮するのかを誰かが説明できますか?

これは重要な質問 です。構文やセマンティクスに関しては言わないでください。質問は、

WHILEループとFORループ、for ループに書かれていることはすべて while ループで実行できるのに、なぜ 2 つのループがあるのでしょうか。

これはケンブリッジ大学のセミナーで出題されます。そのため、パフォーマンスのオーバーヘッドと WC の複雑さの観点から説明する必要があると思います。

Floyd-Hoare ロジックの観点から行かなければならないと思います

Hoare Logic の演習について推論しています。

の評価ではストアを変更できないが、 の実行によってストアが変更され、 の値が変更される可能性があると仮定して、トリプル を満たすすべてのブール式BとすべてのプログラムSおよびを見つける必要があります。P{true} if B then S; if B then P; {a >= 0}BSB

a特に、事後条件にのみ存在し、このような例を見つけたことがないため、について何が言えるかわかりません。

ご協力いただきありがとうございます！

私は、Mordechai Ben-Ari 著『Mathematical Logic for Computer Science』、Springer、1993-2012 という本に触発されて、FOL とプログラム検証に関するコースを教えています。学生に Python でプログラムしてもらうことで、概念を説明したいと思います。

FOL には、優れた FOL パッケージを持つ NLTK を使用しています。

しかし、プログラム検証用の Python パッケージはまだ見つかりませんでした: 前提条件と事後条件の論理式を挿入し、ループ不変条件を見つけ、Python プログラムを段階的に検証します。つまり、Python 内および Python で Hoare 論理フレームワークを使用するプログラム。

このタスクのパッケージを知っていますか?

z3 の分離ロジックに関する推論規則と公理を設計し、それを使用して一部の小道具を自動的に証明できますか? たとえば、"x=y /\ (x |-> z) |- x=y /\ (y |-> z)"