ホーア論理のソースを表示

{{正確性|date=2016年4月|トリプルの定義からすでに通常の定義と異なっている。例もおかしい}}

<!--[[ソフトウェア工学]]における--><!-- ← ソフトウェア工学という語はホーア論理のようにガチガチに形式的なものを指しては、あまり使われない-->'''ホーア論理'''（ホーアろんり、{{lang-en-short| Hoare logic}}）とは、[[公理的意味論]]の立場でプログラムの[[正当性 (計算機科学) |正当性]]について厳密に推論するために[[第一階述語論理]]を拡張した形式論理の言語を言う。

プログラムの正しさを証明するための[[ロバート・フロイド]]による[[フローチャート|流れ図]]に関する方法<ref>[[#Floyd(1967)|Floyd(1967)]]</ref>を基に、計算機科学者の[[アントニー・ホーア]]によって提案された<ref>[[#Hoare(1969)|Hoare(1969)]]<br />
このような経緯から、フロイド−ホーア論理（Floyd-Hoare Logic）とも呼ばれる。[[#荒木・張(2002)|荒木・張(2002)]] p.23</ref>。
== 概要 ==
ホーア論理には、単純な[[命令型プログラミング|命令型言語]]の全構成要素についての[[公理]]と[[推論規則]]が備わっている。当初の論文にあったそれら規則に加えて、ホーアや他の研究者は様々な言語要素に関する規則を開発した。[[並行性]]に関する規則、[[プロシージャ]]に関する規則、[[分岐命令|分岐]]に関する規則、[[ポインタ (プログラミング)|ポインタ]]に関する規則などがある。

== 定義 ==
=== 部分的正当性（partial correctness） ===
事前条件（precondition） P が成り立つときに、プログラム S を実行して、それが停止した場合においては必ず事後条件（postcondition） Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して'''部分的に正当'''（partially correct）であると言い<ref name="#1">[[#荒木・張(2002)|荒木・張(2002)]] p.7</ref>、
:P { S } Q
と記述する<ref>これをホーアの三つ組（Hoare triple）と呼ぶこともある。</ref>。ホーアによる元々の記法は上記のものであるが、一般的にはプログラム S の部分正当性は、
:{ P } S { Q }
と記述されることが多い<ref>これは、ホーアの共同研究者であった[[ニクラウス・ヴィルト]]が開発した[[プログラミング言語]]の[[Pascal]]のコメント記法に由来していると考えられる。[[#系統的(1986)|系統的(1986)]]</ref><ref>部分的正当性に関するホーア論理では、プログラムの完了を示すことができない。もしプログラム S が完了しなければ事後条件の Q は意味を成さない。そのような事情から事後条件 Q を偽の値である '''false''' とすることで完了しないプログラムを
:{ P } S { false }
と表すこともある。</ref>。

=== 正当性（correctness） ===
事前条件 P が成り立つときに、プログラム S を実行すると、'''その実行が必ず終了するならば'''、プログラム S は、事前条件 P に関して'''停止する'''（terminate）と言う<ref name="#1"/>。

プログラム S が部分的に正当かつ停止するものであるとき、すなわち、プログラム S が事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して'''正当'''（correct）であるという<ref name="#1"/>。

== 部分的正当性の証明体系 ==
=== (A1) 代入文の公理 ===
: { Q[e/x] } <code>x:＝e</code> { Q }
ここで、事前条件の Q[e/x] は'''置換'''であり、式 Q の中に出現するすべての x を式 e で置き換えた式を表す。一方で事後条件の Q は代入文実行後（置換'''ではなく'''代入を行ったあとの）x の値について式 Q が成り立つことを表す<ref name="#1"/>。

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

:*<math>\{x+1 = 43\}\ y:=x + 1\ \{ y = 43 \}\!</math>
:*<math>\{x + 1 \leq N \}\ x := x  + 1\ \{x \leq N\}\ \!</math>

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

:<math>\{ A \} \ x := 2\ \{y = 3 \}</math>

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

=== (A2) 空文の公理 ===
空文（<code>skip</code>文）は、プログラムの状態を変化させないが、これを表すのが空文の公理である。<code>skip</code>以前に真であったことはそのまま真となる。
: { P } skip { P }

=== (R1) 複合文の規則 ===
一般に順序的プログラムは機能ごとに分解することができるが、その逆として分解した手続きは複合文として合成することができる。以下の複合文の規則は分解したプログラムが中間条件 R を介することで元の機能に合成されることを表している<ref>
例えば、次の2つの代入を考えてみよう。

:<math>\{ x + 1 = 43\} \ y:=x + 1\ \{y =43 \}</math>
:<math>\{ y = 43\} \ z:=y\ \{z =43 \}</math>

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

:<math>\{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z =43 \}</math>
</ref>。
{| style="margin-left:1em; border-collapse:collapse; text-align:center"
|-
| style="border-bottom:1px solid black" | { P } <code>S1</code> { R } , { R } <code>S2</code> { Q }
|- 
|| { P } <code>S1 ; S2</code> { Q }
|
|}

=== (R2) if文の規則 ===
{| style="margin-left:1em; border-collapse:collapse; text-align:center"
|-
| style="border-bottom:1px solid black" | { P &and; B } <code>S1</code> { Q } , { P &and; &not;B } <code>S2</code> { Q }
|- 
|| { P } <code>If B Then S1 else S2 End</code> { Q }
|
|}


{| style="margin-left:1em; border-collapse:collapse; text-align:center"
|-
| style="border-bottom:1px solid black" | { P &and; B } <code>S1</code> { Q } ,  P &and; &not;B => Q
|- 
|| { P } <code>If B Then S1 End</code> { Q }
|
|}

=== (R3) while文の規則 ===
{| style="margin-left:1em; border-collapse:collapse; text-align:center"
|-
| style="border-bottom:1px solid black" | { P &and; B } <code>S1</code> { P }
|- 
|| { P } <code>While B Do S1 End </code> { P &and; &not;B }
|
|}

ここで、''P'' は[[ループ不変条件]]である<ref>なお、完全正当性のための While 規則としては以下のようになる。
::<math>
\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] }
\!</math>
この規則では、ループ不変条件が保持されるだけでなく、ループが終了することを証明するために{{仮リンク|ループ変化条件|en|loop variant}} ''t'' を加えている。''t'' は[[整礎関係]] (well-founded relation) の観点でループの反復ごとに厳密に減少していく値である。なお不変条件 ''P'' が与えられたとき、条件 ''B'' は ''t'' がその範囲の[[極小元]]でないことを暗に示さなければならず、さもなくば事前条件は偽となる。関係 "<" は整礎なので、ループの各ステップで有限{{仮リンク|鎖 (数学)|en|chain (order theory)|label=鎖}}の元が減少していくことでカウントされる。また、ここで波括弧ではなく角括弧が使われているのは[[正当性 (計算機科学)|完全正当性]]を示すためであり、部分正当性のみならず完了も示す（これは、完全正当性の数ある記法の1つである）。
</ref>。

=== (R4) 帰結の規則 ===
{| style="margin-left:1em; border-collapse:collapse; text-align:center"
|-
| style="border-bottom:1px solid black" | P => P<sub>1</sub> , { P<sub>1</sub> } <code>S</code> { Q<sub>1</sub> } , Q<sub>1</sub> => Q
|- 
|| { P } <code>S</code> { Q }
|
|}

== 例 ==

:{|style="text-align:left"
| style="background:silver;" colspan="4"|'''例 1'''
|-
|<math>\{x+1 = 43\}\!</math>
|<math>\ y:=x + 1\ \!</math>
|<math>\{ y = 43 \}\!</math>
|（代入の公理）
|-
|
|
|
|<math>( x + 1 = 43 \Leftrightarrow x = 42 )</math>
|-
|<math>\{x=42\}\!</math>
|<math>\ y:=x + 1\ \!</math>
|<math>\{y=43 \land x=42\}\!</math>
|（結果規則）
|-
| style="background:silver;" colspan="4"|'''例 2'''
|-
|<math>\{x + 1 \leq N \}\!</math>
|<math>\ x := x  + 1\ \!</math>
|<math>\{x \leq N\}\ \!</math>
|（代入の公理）
|-
|
|
|
|（<math> x < N \implies x + 1 \leq N</math> ここで ''x'' と ''N'' は整数型）
|-
|<math>\{x < N \}\!</math>
|<math>\ x := x  + 1\ \!</math>
|<math>\{x \leq N\}\ \!</math>
|（結果規則）
|}

== 脚注 ==
<references />

== 参考文献 ==
* Robert D. Tennent: "[http://www.cs.queensu.ca/home/specsoft/ Specifying Software]" (ホーア論理を紹介している最近の教科書) ISBN 0-521-00401-2 
* {{cite book | 和書 | title=プログラム仕様記述論 | author=荒木 啓二郎, 張 漢明 | publisher=オーム社 | year=2002 | series=IT Text | ref=荒木・張(2002) }}
* {{cite book | 和書 | title=プログラム検証論 | author=林 晋 | publisher=共立出版 | year=1995 | series=情報数学講座 | ref=林(1995) }}
* {{cite book | 和書 | title=算法表現論 | author=木村 泉, 米澤 明憲 | publisher=岩波書店 | year=1982 | series=岩波講座 情報科学 | ref=木村・米澤(1982) }}
* {{citation | author=R. W. Floyd | title=Assigning meanings to programs | url=http://www.cs.virginia.edu/~weimer/2007-615/reading/FloydMeaning.pdf | journal=Proceedings of the American Mathematical Society Symposia on Applied Mathematics | volume=19 | pages=19–31 | year=1967 | ref=Floyd(1967) }}
* {{citation | author=C. A. R. Hoare | title=An axiomatic basis for computer programming | journal=Communications of the ACM | volume=12(10) | pages=576-580,583 | year=1969 | doi=10.1145/363235.363259 | url=http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf | ref=Hoare(1969) }}
* {{cite book | 和書 | title=系統的プログラミング入門 | edition=第２版補訂 | author=N. Wirth | translator=野下 浩平, 筧 捷彦, 武市 正人 | year=1986 | publisher=近代科学社 | ref=系統的(1986) }}
* {{cite book | 和書 | title=演習 プログラムの証明 | author=ロバート B. アンダスン | translator=有澤 誠 | publisher=近代科学社 | series=ソフトウェア工学ライブラリ | year=1980 | ref=演習(1980) }}
== 関連項目 ==
* [[構造化プログラミング]] - [[公理的意味論]] - [[プログラム検証]]
* [[第一階述語論理]] - 自然演繹
* [[Pascal]]

* [[Communicating Sequential Processes]]
* [[契約による設計]]
* [[述語変換意味論]]
* [[静的コード解析]]
* [[カリー・ハワード同型対応]] - [[マーティン＝レーフの型理論]]<small>（表明の代わりに型を利用したもの）</small>
=== 関連人物 ===
* [[エドガー・ダイクストラ]]
* [[ニクラウス・ヴィルト]]
* [[ペール・マルティン＝レーフ]]
== 外部リンク ==
* [http://www.key-project.org/download/hoare/ KeY-Hoare] - [[:en:KeY|KeY]] という定理証明機上に構築された半自動検証システムで、ホーア論理を散りいれている。
* [http://j-algo.binaervarianz.de/index.php?language=en j-Algo-modul Hoare calculus] &mdash; アルゴリズム視覚化プログラム j-Algo におけるホーア論理視覚化モジュール

{{Normdaten}}
{{DEFAULTSORT:ほおあろんり}}
[[Category:プログラム論理]]
[[Category:計算機科学における論理]]
[[Category:形式手法]]
[[Category:ソフトウェア工学]]
[[Category:エポニム]]