ホーア論理

出典: フリー百科事典『ウィキペディア（Wikipedia）』
移動: 案内、 検索

ホーア論理（Hoare Logic、別名 Floyd–Hoare Logic）は、コンピュータプログラムの正当性について厳密に推論する論理規則群を備えた形式体系。1969年、イギリス人の計算機科学者で数理論理学者のアントニー・ホーアが提案し、ホーアや他の研究者が発展させた[1]。ロバート・フロイドのフローチャートに関しての同様の体系をベースとしている[2]。

目次

Hoare triple [編集]

ホーア論理の中心となる部分は 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 規則の拡張版（後述）で証明できる。

規則群 [編集]

空文の公理のスキーマ [編集]

空文の規則は、skip文がプログラムの状態を変化させないことを表しており、skip以前に真であったことはそのまま真となる。

\frac{}{\{P\}\ \text{skip}\ \{P\}} \!

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

代入の公理は、代入前に代入の右辺に対して真であった述語が、代入後の変数についても成り立つことを示している。形式的には変数 x が自由である式を P とし、次のように表す。

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

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

代入の公理は、\{P[E/x]\} の真理値が代入後の \{P\} の真理値と同じであることを意味する。すなわち、代入前に \{P[E/x]\} が「真」であれば、代入後の \{P\} も「真」ということになる。逆に、代入前の \{P[E/x]\} が「偽」なら、代入後の \{P\} も必ず「偽」となる。

これはつまり、事前条件を求めるには、まず事後条件を定め、その中に出現する代入の左辺を全て代入の右辺で置き換えればよい。事前と事後を取り違えて \{P\} x :=E \{P[E/x]\} としないよう注意が必要である。

正しい Triple の例:

  • \{x+1 = 43\}\ y:=x + 1\ \{ y = 43 \}\!
  • \{x + 1 \leq N \}\ x := x + 1\ \{x \leq N\}\ \!

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

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

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

合成規則 [編集]

ホーアの合成規則は逐次的に実行されるプログラム S と T についてのもので、S を実行してから T を実行することを S;T と書き、次のように表す（Q は中間条件）[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\} } \!

結果規則 [編集]

\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 \}\ S\ \{P\} } { \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} } \!

ここで、P はループ不変条件（英語版）である。

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

\frac { <\;\textrm{is\ well-founded,}\;[P \wedge B \wedge t = z ]\ S\ [P \wedge t < z ]} { [P]\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ [\neg B \wedge P] } \!

この規則では、ループ不変条件が保持されるだけでなく、ループが終了することを証明するためにループ変化条件（英語版） t を加えている。t は整礎関係 (well-founded relation) の観点でループの反復ごとに厳密に減少していく値である。なお不変条件 P が与えられたとき、条件 B は t がその範囲の極小元でないことを暗に示さなければならず、さもなくば事前条件は偽となる。関係 "<" は整礎なので、ループの各ステップで有限鎖（英語版）の元が減少していくことでカウントされる。また、ここで波括弧ではなく角括弧が使われているのは完全正当性を示すためであり、部分正当性のみならず完了も示す（これは、完全正当性の数ある記法の1つである）。

例 [編集]

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

脚注 [編集]

  1. ^ C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–580,583 October 1969. doi:10.1145/363235.363259
  2. ^ R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.
  3. ^ Logic in Computer Science (second edition), page 276

参考文献 [編集]

関連項目 [編集]

外部リンク [編集]

  • KeY-Hoare - KeY という定理証明機上に構築された半自動検証システムで、ホーア論理を散りいれている。
  • j-Algo-modul Hoare calculus — アルゴリズム視覚化プログラム j-Algo におけるホーア論理視覚化モジュール
「http://ja.wikipedia.org/w/index.php?title=ホーア論理&oldid=46781988」から取得