ホーア論理

ホーア論理（Hoare Logic、別名 Floyd–Hoare Logic）は、アントニー・ホーアが開発した形式体系。ホーアの1969年の論文 "An axiomatic basis for computer programming" で発表された。この体系の目的は、数理論理学の厳密さでプログラムの正当性を論じるための論理的規則群を提供することにある。

ホーアは、フローチャートに関して同様の体系を発表したロバート・フロイドからの影響を認めている。

ホーア論理の中心となる部分は Hoare Triple である。Hoare Triple はコードの実行による状態変化を表すものである。Hoare Triple の形式は以下の通りである。

$\{P\}\;C\;\{Q\}$

ここで、P と Q は「表明(assertion)」であり、C は「コマンド」である。P は「事前状態」、Qは「事後状態」でもある。表明（状態）は述語論理の式で表される。

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

[編集] 部分正当性と完全正当性

標準ホーア論理はプログラムの完了を証明できないため、部分正当性しか証明できない。従って Hoare Triple の直感的な意味は「P が C を実行する前の状態であるとき、Q が完了後の状態を示すか、C が完了しない」となる。C が完了しなければ「完了後」は存在せず、Q は意味を成さない。あるいは、C が完了しないことを表現するために、偽の値を持つ Q を選択することも考えられる。

完全正当性は While 規則の拡張版（後述）で証明できる。

[編集] 空文の公理

$\frac{}{\{P\}\ \textbf{pass}\ \{P\}} \!$

[編集] 代入の公理のスキーマ

代入の公理は、代入前に真であった代入対象の変項を持つ全ての述語に、代入式の右辺を当てはめることを示す。

$\frac{}{\{P[x/E]\}\ x:=E \ \{P\} } \!$

ここで、 $P[x/E]$ は式 P の中で変項 x の全ての自由変項が式 E で置き換えられることを意味する。

正しい Triple の例:

$\{x+1=43 \land x=42\} \ y:=x + 1\ \{y=43 \land x=42\} \!$

ホーアが提案した代入の公理は、複数の（変項の）名前が（メモリ上の）同じ格納値を参照している場合に「正しくない」。例えば、以下の例で x と y が同じ値を参照している場合

$\{y = 3\} x := 2 \{y = 3\}$

この Triple は真ではない。なぜなら、 x に 2 を代入した後では y が 3 となるような事前状態は存在しないからである。

[編集] 逐次規則

$\frac {\{P\}\ S\ \{Q\}\ , \ \{Q\}\ T\ \{R\} } {\{P\}\ S;T\ \{R\}} \!$

例えば、次の2つの代入を考えてみよう。

$\{ x + 1 = 43\} \ y:=x + 1\ \{y =43 \}$

$\{ y = 43\} \ z:=y\ \{z =43 \}$

逐次規則を適用すると、これらは次のようになる:

$\{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z =43 \}$

[編集] 条件規則

$\frac { \{B \wedge P\}\ S\ \{Q\}\ ,\ \{\neg B \wedge P \}\ T\ \{Q\} } { \{P\}\ \textbf{if}\ B\ \textbf{then}\ S\ \textbf{else}\ T\ \textbf{endif}\ \{Q\} } \!$

[編集] While 規則

$\frac { \{P \wedge B \}\ S\ \{P\} } { \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} } \!$

ここで、P はループによって変化しない部分を示す。

[編集] 結果規則

$\frac { P^\prime \rightarrow\ P\ ,\ \lbrace P \rbrace\ S\ \lbrace Q \rbrace\ ,\ Q \rightarrow\ Q^\prime } { \lbrace P^\prime\ \rbrace\ S\ \lbrace Q^\prime\rbrace } \!$

[編集] 完全正当性のための While 規則

$\frac { \{P \wedge B \wedge t = z \}\ S\ \{P \wedge t < z \} \ ,\ P \rightarrow t \geq 0} { \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} } \!$

ここで、完了することを証明するために繰り返しの度に値が減っていく項 t を用意する。t として「良い性質」の値を用意することで、有限個の減少していく数によってループ回数がカウントされることになる。

[編集] 参考文献

C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–585, 1969年10月 DOI:10.1145/363235.363259 | Download PDF
Robert D. Tennent: "Specifying Software" (ホーア論理を紹介している最近の教科書) ISBN 0-521-00401-2 [1]
Project Bali では、ホーア論理的ルールをJava言語のサブセットに定義し、Isabelle theorem prover で使用した。

[編集] 関連項目