ホーア論理

ホーア論理（ホーアろんり、英: Hoare logic）とは、公理的意味論の立場でプログラムの正当性について厳密に推論するために第一階述語論理を拡張した形式論理の言語を言う。

プログラムの正しさを証明するためのロバート・フロイドによる流れ図に関する方法を基に、計算機科学者のアントニー・ホーアによって提案された。

概要

ホーア論理には、単純な命令型言語の全構成要素についての公理と推論規則が備わっている。当初の論文にあったそれら規則に加えて、ホーアや他の研究者は様々な言語要素に関する規則を開発した。並行性に関する規則、プロシージャに関する規則、分岐に関する規則、ポインタに関する規則などがある。

定義

部分的正当性（partial correctness）

事前条件（precondition） P が成り立つときに、プログラム S を実行して、それが停止した場合においては必ず事後条件（postcondition） Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して部分的に正当（partially correct）であると言い、

P { S } Q

と記述する。ホーアによる元々の記法は上記のものであるが、一般的にはプログラム S の部分正当性は、

{ P } S { Q }

と記述されることが多い。

正当性（correctness）

事前条件 P が成り立つときに、プログラム S を実行すると、その実行が必ず終了するならば、プログラム S は、事前条件 P に関して停止する（terminate）と言う。

プログラム S が部分的に正当かつ停止するものであるとき、すなわち、プログラム S が事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して正当（correct）であるという。

部分的正当性の証明体系

(A1) 代入文の公理

{ Q[e/x] } x:＝e { Q }

ここで、事前条件の Q[e/x] は置換であり、式 Q の中に出現するすべての x を式 e で置き換えた式を表す。一方で事後条件の Q は代入文実行後（置換ではなく代入を行ったあとの）x の値について式 Q が成り立つことを表す。

したがって、この公理は、

{ Q[e/x] }：式 Q 中の全ての x を e に置換するとき式 Q が成り立つのであれば、
x:=e：（置換で成り立つならば、ほぼ同じような代入操作でも変わらないはずのため）式 Q 中の x の値を代入 x:=e で変更することで、
{ Q }：（置換の場合は成り立っているのであるから x の値が e に変更されたのであれば当然に）代入文実行後の式 Q は成り立つ、

というように読む。

(A2) 空文の公理

空文（skip文）は、プログラムの状態を変化させないが、これを表すのが空文の公理である。skip以前に真であったことはそのまま真となる。

{ P } skip { P }

(R1) 複合文の規則

一般に順序的プログラムは機能ごとに分解することができるが、その逆として分解した手続きは複合文として合成することができる。以下の複合文の規則は分解したプログラムが中間条件 R を介することで元の機能に合成されることを表している。

(R2) if文の規則

(R3) while文の規則

ここで、P はループ不変条件である。

(R4) 帰結の規則

例

脚注

参考文献

Robert D. Tennent: "Specifying Software" (ホーア論理を紹介している最近の教科書) ISBN 0-521-00401-2
荒木啓二郎, 張漢明『プログラム仕様記述論』オーム社〈IT Text〉、2002年。
林晋『プログラム検証論』共立出版〈情報数学講座〉、1995年。
木村泉, 米澤明憲『算法表現論』岩波書店〈岩波講座情報科学〉、1982年。
R. W. Floyd (1967), “Assigning meanings to programs”, Proceedings of the American Mathematical Society Symposia on Applied Mathematics 19: 19–31, http://www.cs.virginia.edu/~weimer/2007-615/reading/FloydMeaning.pdf
C. A. R. Hoare (1969), “An axiomatic basis for computer programming”, Communications of the ACM 12(10): 576-580,583, doi:10.1145/363235.363259, http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf
N. Wirth 著、野下浩平, 筧捷彦, 武市正人訳『系統的プログラミング入門』（第２版補訂）近代科学社、1986年。
ロバート B. アンダスン著、有澤誠訳『演習プログラムの証明』近代科学社〈ソフトウェア工学ライブラリ〉、1980年。