language-agnostic - ホーア論理ループ不変条件

Question

私はホーア論理を見ていますが、ループ不変条件を見つける方法を理解するのに問題があります。

誰かがループ不変条件を計算するために使用される方法を説明できますか？

そして、ループ不変条件が「有用な」ものであるために何を含むべきでしょうか？

私は単純な例だけを扱っており、不変条件を見つけて、次のような例で部分的および完全な修正を証明しています。

{ i ≥ 0 } while i > 0 do i := i−1 { i = 0 }

score 5 · Accepted Answer

プログラムの (部分的な) 正しさを証明するための Hoare の論理について話している場合、前提条件と事後条件を使用し、プログラムを分解し、Hoare の論理推論システムの規則を使用して、帰納的な公式を作成して証明します。

あなたの例では、ルールを使用してプログラムを分解したい

{p} while b do S {p^not(b)} <=> {p^b} S {p}

あなたの場合

したがって、次のステップでを推測し{i ≥ 0 ^ i > 0} i := i−1 {i ≥ 0}ます。これは、さらに推測して、非常に簡単に証明できます。これが役立つことを願っています。

score 3 · Accepted Answer

これがあなたの質問に答えるかどうかはわかりませんが、念のために:

非公式の「ループ不変条件」は、ループの反復の前後で真のままであるという事実のステートメントです。基本的に、そのループに関するプログラムの一貫性の制約を定義します。
Hoare Logic については、ループ不変条件がどのように「計算」されるかを正確に説明できるほど十分に知りませんが、そのようなことは、形式的な証明言語自体よりも、分析されるコードの言語に依存するのではないかと思います。作業している正式なアルゴリズムの説明はありますか? もう少し背景があれば、さらに先に進むことができるかもしれません。
有用なループ不変条件は、アプリケーションの状態に関する特定の何かを記述します。たとえば、挿入ソートを作成している場合、メイン要素のモーションループに役立つループ不変式は、(サブ) リストにはループの実行前と実行後に同じオブジェクトのコレクションが含まれていることを本質的に示します。ソート順のままです。

score 2 · Accepted Answer

（あなたの推論のために）有用であることは、不変条件の主なポイントです。したがって、証明したい事後条件を見て、段階的に事後条件に到達するのに役立ち、ループのコードから導出できる不変式を作成してみてください。

3 に答える 3