ホーア論理

ホーア論理（ホーアろんり、）とは、公理的意味論の立場でプログラムの正当性について厳密に推論するために第一階述語論理を拡張した形式論理の言語を言う。
プログラムの正しさを証明するためのロバート・フロイドによる流れ図に関する方法を基に、計算機科学者のアントニー・ホーアによって提案された。
概要.
ホーア論理には、単純な命令型言語の全構成要素についての公理と推論規則が備わっている。当初の論文にあったそれら規則に加えて、ホーアや他の研究者は様々な言語要素に関する規則を開発した。並行性に関する規則、プロシージャに関する規則、分岐に関する規則、ポインタに関する規則などがある。
定義.
部分的正当性（partial correctness）.
事前条件（precondition） P が成り立つときに、プログラム S を実行して、それが停止した場合においては必ず事後条件（postcondition） Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して部分的に正当（partially correct）であると言い、
と記述する。ホーアによる元々の記法は上記のものであるが、一般的にはプログラム S の部分正当性は、
と記述されることが多い。
正当性（correctness）.
事前条件 P が成り立つときに、プログラム S を実行すると、その実行が必ず終了するならば、プログラム S は、事前条件 P に関して停止する（terminate）と言う。
プログラム S が部分的に正当かつ停止するものであるとき、すなわち、プログラム S が事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して正当（correct）であるという。
部分的正当性の証明体系.
(A1) 代入文の公理.
ここで、事前条件の Q[e/x] は置換であり、式 Q の中に出現するすべての x を式 e で置き換えた式を表す。一方で事後条件の Q は代入文実行後（置換ではなく代入を行ったあとの）x の値について式 Q が成り立つことを表す。
したがって、この公理は、
というように読む。
(A2) 空文の公理.
空文（codice_3文）は、プログラムの状態を変化させないが、これを表すのが空文の公理である。codice_3以前に真であったことはそのまま真となる。
(R1) 複合文の規則.
一般に順序的プログラムは機能ごとに分解することができるが、その逆として分解した手続きは複合文として合成することができる。以下の複合文の規則は分解したプログラムが中間条件 R を介することで元の機能に合成されることを表している。
(R3) while文の規則.
ここで、"P" はループ不変条件である。