ホーア論理
プログラムの正当性を証明するための形式システム
計算の軌跡によって検証する
不変条件を使ってループを処理する
ループしても変化しない不変条件に着目
GPT-4.icon
ホーア論理（Hoare logic）は、プログラムの正当性を推論するための形式的体系で、特に命令型プログラムに適用されます。これは、トニー・ホーアによって1969年に導入されたもので、プログラムの各部分が特定の条件を満たすことを証明するのに役立ちます。ホーア論理は「前提条件」と「後置条件」という2つの概念を用いてプログラムの動作を記述します。
ホーア論理の基本は「ホーア・トリプル」と呼ばれる形式 \( \{P\} C \{Q\} \) を取ります。ここで \( P \) は「前提条件」(precondition)、\( C \) は「コマンド」(command) またはプログラムの断片、\( Q \) は「後置条件」(postcondition) です。このトリプルは、「\( P \) が真のときにコマンド \( C \) を実行すると、\( Q \) が真になる」という意味です。 例えば、変数 \( x \) に対する代入を考えてみましょう。ホーア・トリプルではこの操作を \( \{x = 5\} x := x + 1 \{x = 6\} \) のように表現できます。これは、「\( x \) が5である状態で \( x \) に1を加えると、\( x \) は6になる」と読むことができます。
ホーア論理のルールには、代入、シーケンス、条件分岐、ループなど、基本的なプログラム構造に対応するものがあります。これらのルールを組み合わせることで、より複雑なプログラムの正当性を段階的に証明できます。
形式的検証、特にプログラム検証において、ホーア論理は重要な役割を担っています。ただし、ホーア論理はプログラムの側面によっては扱いにくい場合があり、そのためにより洗練された手法（例えば、モデル検査や抽象解釈）が開発されています。また、関数型言語や論理型言語など、命令型以外のパラダイムには適用が難しい場合もあります。
プログラムの自動検証のツールや理論的な研究では、このようなホーア論理が基礎として使用され、さらに発展した形式手法の基盤をなしています。
圏論的定式化