ja.wikipedia.org

ホーア論理 - Wikipedia

出典: フリー百科事典『ウィキペディア（Wikipedia）』

この記事の正確性に疑問が呈されています。 問題箇所に信頼できる情報源を示して、記事の改善にご協力ください。議論はノートを参照してください。（2016年4月）
疑問点：トリプルの定義からすでに通常の定義と異なっている。例もおかしい

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

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

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

部分的正当性（partial correctness）

[編集]

事前条件（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\}\ \!} （結果規則）
  1. ^ Floyd(1967)
  2. ^ Hoare(1969)
    このような経緯から、フロイド−ホーア論理（Floyd-Hoare Logic）とも呼ばれる。荒木・張(2002) p.23
  3. ^ a b c d 荒木・張(2002) p.7
  4. ^ これをホーアの三つ組（Hoare triple）と呼ぶこともある。
  5. ^ これは、ホーアの共同研究者であったニクラウス・ヴィルトが開発したプログラミング言語のPascalのコメント記法に由来していると考えられる。系統的(1986)
  6. ^ 部分的正当性に関するホーア論理では、プログラムの完了を示すことができない。もしプログラム S が完了しなければ事後条件の Q は意味を成さない。そのような事情から事後条件 Q を偽の値である false とすることで完了しないプログラムを
    { P } S { false }
    と表すこともある。
  7. ^ 正しい Triple の例:
    • {\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\}\!}
    • {\displaystyle \{x+1\leq N\}\ x:=x+1\ \{x\leq N\}\ \!}
    ホーアが提案した代入の公理は、複数の（変項の）名前が（メモリ上の）同じ格納値を参照している場合に「正しくない」。例えば、以下の例で x と y が同じ値を参照している場合
    {\displaystyle \{A\}\ x:=2\ \{y=3\}}
    この Triple は真ではない。なぜなら、 x に 2 を代入した後では y が 3 となるような事後状態は存在しないからである。
  8. ^ 例えば、次の2つの代入を考えてみよう。
    {\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\}}
    {\displaystyle \{y=43\}\ z:=y\ \{z=43\}}
    合成規則を適用すると、これらは次のようになる:
    {\displaystyle \{x+1=43\}\ y:=x+1;z:=y\ \{z=43\}}
  9. ^ なお、完全正当性のための While 規則としては以下のようになる。
    {\displaystyle {\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つである）。
  • 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
  • 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
  • N. Wirth 著、野下 浩平, 筧 捷彦, 武市 正人 訳『系統的プログラミング入門』（第２版補訂）近代科学社、1986年。
  • ロバート B. アンダスン 著、有澤 誠 訳『演習 プログラムの証明』近代科学社〈ソフトウェア工学ライブラリ〉、1980年。
  • KeY-Hoare - KeY という定理証明機上に構築された半自動検証システムで、ホーア論理を散りいれている。
  • j-Algo-modul Hoare calculus — アルゴリズム視覚化プログラム j-Algo におけるホーア論理視覚化モジュール