Hoare Logicループ不変式

Question

私はHoare Logicを見ていますが、ループ不変式を見つける方法を理解する上で問題があります。

誰かがループ不変量の計算に使用した方法を説明できますか？

ループインバリアントは、「有用な」ものにする必要がありますか？

私だけのような例では、簡単な例を扱う不変条件を見つけ、部分的および完全な補正を証明しています：

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

Answer 1

私たちは、あなたが、前提条件と事後条件を使用してプログラムを分解し、誘導式を作成し、証明するためにホーアのロジック推論システムのルールを使用して、プログラムの（部分）正しさを証明するためホーアのロジックについて話している場合。あなたの例では

は、あなたがあなたのケースでは、ルール

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

を使用してプログラムを分解したい

• P：私≥0
• B：I> 0
• S： i：= i-1である。

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

Answer 2

は（あなたの推論のため）に有用であることは不変の主なポイントです。それで、あなたが証明したい事後条件を見て、事後条件に到達するのに役立ち、ループのコードから導かれる不変条件を作ります。

Answer 3

私はこれがあなたの質問にお答えしますかどうかわからないんだけど、念のためにそれがない：

• 「不変ループは」非公式の反復の前と後に真のまま事実の文ですループ。これは本質的に、そのループに関するプログラムの整合性制約を定義します。
• ループ不変式がどのように「計算されるか」を正確に伝えるためにHoare Logicについては十分に分かっていませんが、私はそのようなことが正式な証明言語自体よりも分析されるコードの言語に依存すると思われます。あなたが作業している形式的なアルゴリズム記述がありますか？私はもう少し背景を持ってさらに進むことができるかもしれません。
• 有用なループ不変式は、アプリケーションの状態に関する特定のものを記述します。例えば、挿入ソートを書く場合、主要な要素のモーションループのための有用なループ不変式は、ループの実行前後のオブジェクトの同じコレクションを（サブ）リストに含み、おそらくはソートされた順番で並べ替えられます。