ホーア論理

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

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

P { S } Q

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

{ P } S { Q }

と記述されることが多い^[5][6]。

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

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

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

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

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

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

というように読む^[7]。

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

{ P } skip { P }

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

{ P } S1 { R } , { R } S2 { Q }
{ P } S1 ; S2 { Q }

{ P ∧ B } S1 { Q } , { P ∧ ¬B } S2 { Q }
{ P } If B Then S1 else S2 End { Q }

{ P ∧ B } S1 { Q } , P ∧ ¬B => Q
{ P } If B Then S1 End { Q }

{ P ∧ B } S1 { P }
{ P } While B Do S1 End { P ∧ ¬B }

ここで、P はループ不変条件である^[9]。

P => P1 , { P1 } S { Q1 } , Q1 => Q
{ P } S { Q }

例 1
${\displaystyle \{x+1=43\}\!}$	${\displaystyle \ y:=x+1\ \!}$	${\displaystyle \{y=43\}\!}$	（代入の公理）
			${\displaystyle (x+1=43\Leftrightarrow x=42)}$
${\displaystyle \{x=42\}\!}$	${\displaystyle \ y:=x+1\ \!}$	${\displaystyle \{y=43\land x=42\}\!}$	（結果規則）
例 2
${\displaystyle \{x+1\leq N\}\!}$	${\displaystyle \ x:=x+1\ \!}$	${\displaystyle \{x\leq N\}\ \!}$	（代入の公理）
			（${\displaystyle x<N\implies x+1\leq N}$ ここで x と N は整数型）
${\displaystyle \{x<N\}\!}$	${\displaystyle \ x:=x+1\ \!}$	${\displaystyle \{x\leq N\}\ \!}$	（結果規則）