ホーア論理

ホーア論理（フロイド・ホーア論理、ホーア規則とも呼ばれる）は、コンピュータプログラムの正しさについて厳密に推論するための一連の論理規則を備えた形式体系である。1969年にイギリスのコンピュータ科学者で論理学者のトニー・ホーアによって提唱され、その後ホーアと他の研究者によって改良された。^{[ 1 ]}元々のアイデアは、フローチャート用の同様のシステム^{[ 2 ]}を発表していたロバート・W・フロイドの研究に端を発している。

ホーアトリプル

ホーア論理の中心的な特徴はホーア・トリプルである。トリプルは、コードの実行が計算の状態をどのように変化させるかを記述する。ホーア・トリプルは以下の形式をとる。

${\displaystyle \{P\}C\{Q\}}$

ここで、 とはアサーションであり、はコマンドです。^{[注 1 ]}は前提条件と事後条件と呼ばれます。前提条件が満たされた場合、コマンドを実行すると事後条件が成立します。アサーションは述語論理における式です。 ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle C}$ ${\displaystyle P}$ ${\displaystyle Q}$

ホーア論理は、単純な命令型プログラミング言語のあらゆる構成要素に対する公理と推論規則を提供します。ホーアの原論文に記載されている単純な言語の規則に加えて、その後、ホーアをはじめとする多くの研究者によって、他の言語構成要素に対する規則が開発されてきました。並行性、手続き、ジャンプ、ポインタに関する規則があります。

部分的な正しさと完全な正しさ

標準的なホーア論理を用いると、部分的な正しさしか証明できません。完全な正しさには、さらに停止性が必要ですが、これは別途、またはWhile規則の拡張版を用いて証明できます。^{[ 3 ]}したがって、ホーア・トリプルの直感的な解釈は次のようになります。の実行前の状態が であるときはいつでも、その後 が成立するか、またはは停止しません。後者の場合、「後」は存在しないため、 はどのような文でも成り立ちます。実際、 が停止しない ことを表現するために偽を選択することも可能なのです。${\displaystyle P}$ ${\displaystyle C}$ ${\displaystyle Q}$ ${\displaystyle C}$ ${\displaystyle Q}$ ${\displaystyle Q}$ ${\displaystyle C}$

ここで、そして本稿の残りの部分で言う「終了」とは、より広い意味で、計算が最終的に完了することを意味します。つまり、無限ループが存在しないことを意味します。実装上の制限違反（例えば、ゼロ除算）によってプログラムが途中で停止することがないという意味ではありません。1969年の論文では、ホーアはより狭義の終了の概念を用いており、これも実装上の制限違反が存在しないことを意味します。そして、アサーションを実装に依存しないままにしておくというより広義の終了の概念を好んでいました。

上で引用した公理と規則のもう 1 つの欠陥は、プログラムが正常に終了することの証明の根拠を提供していないことです。終了に失敗する原因は、無限ループである可能性があります。または、実装定義の制限 (数値オペランドの範囲、ストレージのサイズ、オペレーティング システムの時間制限など) に違反していることが原因の可能性があります。したがって、表記「」は、「プログラムが正常に終了する場合、その結果の特性は によって記述される」と解釈する必要があります。終了しないプログラムの「結果」を予測するために使用できないように公理を適応させることはかなり簡単です。しかし、公理を実際に使用するには、コンピュータのサイズと速度、数値の範囲、オーバーフロー手法の選択など、実装に依存する多くの機能に関する知識が必要になります。無限ループの回避の証明とは別に、プログラムの「条件付き」正しさを証明し、実装制限の違反の結果としてプログラムの実行を中止しなければならなかった場合に警告を出す実装に依存する方がおそらく良いでしょう。${\displaystyle P\{Q\}R}$ ${\displaystyle R}$

— ホーア 1969、578～579ページ

ルール

空文公理スキーマ

空文規則は、skip文がプログラムの状態を変更しないことを主張しており、したがってskip文の前に当てはまるものはskip文の後にも当てはまる。^{[注 2 ]}

${\displaystyle {\dfrac {}{\{P\}{\texttt {skip}}\{P\}}}}$

割り当て公理スキーマ

代入公理は、代入後、代入の右辺で真であった述語が変数に対しても成立することを述べています。正式には、変数x が自由であるという言明をPとします。すると、次のようになります。

${\displaystyle {\dfrac {}{\{P[E/x]\}x:=E\{P\}}}}$

ここで、xの各自由出現が式Eに置き換えられたアサーションPを表します。 ${\displaystyle P[E/x]}$

代入公理スキームは、 の真は代入後のPの真と等価であることを意味します。したがって、代入前に が真であった場合、代入公理により、の後にP は真となります。逆に、代入文の前に が偽（すなわち真）であった場合、代入文の後にはP は必ず偽となります。 ${\displaystyle P[E/x]}$ ${\displaystyle P[E/x]}$ ${\displaystyle P[E/x]}$ ${\displaystyle \neg P[E/x]}$

有効なトリプルの例は次のとおりです。

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

式によって変更されないすべての事前条件は、事後条件に引き継がれます。最初の例では、代入によってという事実は変わらないため、両方の文が事後条件に現れる可能性があります。正式には、この結果は、 Pが (および)である公理スキームを適用することで得られ、 が(および) となり、これをさらに与えられた事前条件 に簡略化できます。 ${\displaystyle y:=x+1}$ ${\displaystyle x+1=43}$ ${\displaystyle y=43}$ ${\displaystyle x+1=43}$ ${\displaystyle P[(x+1)/y]}$ ${\displaystyle x+1=43}$ ${\displaystyle x+1=43}$ ${\displaystyle x+1=43}$

代入公理スキームは、前提条件を見つけるには、まず事後条件を取り、代入の左辺のすべての出現を右辺に置き換える、ということになります。この誤った考え方に従って、これを逆順に行おうとしないように注意してください。この規則は、次のような無意味な例につながります。 ${\displaystyle \{P\}x:=E\{P[E/x]\}}$

${\displaystyle \{x=5\}x:=3\{3=5\}}$

一見魅力的に見えるもう一つの誤ったルールは です。これは次のような無意味な例につながります。 ${\displaystyle \{P\}x:=E\{P\wedge x=E\}}$

${\displaystyle \{x=5\}x:=x+1\{x=5\wedge x=x+1\}}$

与えられた事後条件P は、事前条件 を一意に決定しますが、その逆は成り立ちません。例えば、 ${\displaystyle P[E/x]}$

• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge x\leq 9\}}$ 、
• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge y\cdot y\leq 9\}}$ 、
• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge x\leq 9\}}$ 、 そして
• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge y\cdot y\leq 9\}}$

割り当て公理スキームの有効なインスタンスです。

ホーアが提唱した代入公理は、複数の名前が同じ格納値を参照する場合には 適用されない。例えば、

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

は、代入公理スキームの適切な例（ と が両方とも ）ですが、xとyが同じ変数を参照している場合（エイリアシング）は間違っています。 ${\displaystyle \{P\}}$ ${\displaystyle \{P[2/x]\}}$ ${\displaystyle \{y=3\}}$

構成のルール

補助変数なしで スワップコードを検証する

以下の3つの文（2行目、4行目、6行目）は、補助変数を必要とせずに変数aとbの値を交換します。検証証明では、 aとbの初期値はそれぞれ定数AとBで表されます。この証明は7行目から逆順に読むのが最適です。例えば、5行目は7行目からa（6行目のターゲット式）を（6行目のソース式）に置き換えることで得られます。暗黙的に算術的な簡略化が用いられています。例えば、（5行目→3行目）、（3行目→1行目）などです。 ${\displaystyle ab}$ ${\displaystyle a-(ab)=b}$ ${\displaystyle a+bb=a}$ 番号 コード アサーション 1：       ${\displaystyle \{a=A\wedge b=B\}}$ 2: ${\displaystyle a:=a+b;}$       3: ${\displaystyle \{a-b=A\wedge b=B\}}$ 4: ${\displaystyle b:=a-b;}$ 5: ${\displaystyle \{b=A\wedge a-b=B\}}$ 6: ${\displaystyle a:=a-b}$ 7: ${\displaystyle \{b=A\wedge a=B\}}$

ホーアの合成規則は、連続して実行されるプログラムSとTに適用され、SはTより先に実行され、次のように記述される（Qは中間条件と呼ばれる）。^{[ 4 ]}${\displaystyle S;T}$

${\displaystyle {\dfrac {\{P\}S\{Q\}\quad ,\quad \{Q\}T\{R\}}{\{P\}S;T\{R\}}}}$

たとえば、割り当て公理の次の 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\}}$

別の例を右のボックスに示します。

条件付きルール

${\displaystyle {\dfrac {\{B\wedge P\}S\{Q\}\quad ,\quad \{\neg B\wedge P\}T\{Q\}}{\{P\}{\texttt {if}}\ B\ {\texttt {then}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}\{Q\}}}}$

条件規則は、thenとelse部分に共通する事後条件Qは、if...endif文全体の事後条件でもあることを規定している。 ^{[ 5 ]} then部分とelse部分では、それぞれ否定されていない条件Bと否定された条件Bを事前条件Pに追加することができる。条件Bは副作用を持ってはならない。次の節で例を示す。

この規則はホーアの元の出版物には含まれていませんでした。^{[ 1 ]} しかし、

${\displaystyle {\texttt {if}}\ B\ {\texttt {then}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}}$

1回限りのループ構造と同じ効果があります

${\displaystyle {\texttt {bool}}\ b:={\texttt {true}};{\texttt {while}}\ B\wedge b\ {\texttt {do}}\ S;b:={\texttt {false}}\ {\texttt {done}};b:={\texttt {true}};{\texttt {while}}\ \neg B\wedge b\ {\texttt {do}}\ T;b:={\texttt {false}}\ {\texttt {done}}}$

条件文のルールは、他のホーアルールから導出できます。同様に、forループ、do...untilループ、switch、break、continueといった他の派生プログラム構造のルールも、プログラム変換によってホーアの原論文のルールに簡略化できます。

結果ルール

${\displaystyle {\dfrac {P_{1}\rightarrow P_{2}\quad ,\quad \{P_{2}\}S\{Q_{2}\}\quad ,\quad Q_{2}\rightarrow Q_{1}}{\{P_{1}\}S\{Q_{1}\}}}}$

この規則は、事前条件を強化したり、事後条件を弱めたりすることを可能にします。例えば、 then部分とelse部分の事後条件を文字通り同一にしたい場合に用いられます。 ${\displaystyle P_{2}}$ ${\displaystyle Q_{2}}$

例えば、

${\displaystyle \{0\leq x\leq 15\}{\texttt {if}}\ x<15\ {\texttt {then}}\ x:=x+1\ {\texttt {else}}\ x:=0\ {\texttt {endif}}\{0\leq x\leq 15\}}$

条件付きルールを適用する必要があり、そのためには

${\displaystyle \{0\leq x\leq 15\wedge x<15\}x:=x+1\{0\leq x\leq 15\}}$ 、または簡略化された

${\displaystyle \{0\leq x<15\}x:=x+1\{0\leq x\leq 15\}}$

thenの部分については、

${\displaystyle \{0\leq x\leq 15\wedge x\geq 15\}x:=0\{0\leq x\leq 15\}}$ 、または簡略化された

${\displaystyle \{x=15\}x:=0\{0\leq x\leq 15\}}$

else部分の場合。

しかし、 then部分の割り当て規則ではPを次のように選択する必要がある。したがって、規則を適用すると、 ${\displaystyle 0\leq x\leq 15}$

${\displaystyle \{0\leq x+1\leq 15\}x:=x+1\{0\leq x\leq 15\}}$ これは論理的には

${\displaystyle \{-1\leq x<15\}x:=x+1\{0\leq x\leq 15\}}$ 。

結果ルールは、割り当てルールから取得された前提条件を条件ルールに必要なものに強化するために必要です。 ${\displaystyle \{-1\leq x<15\}}$ ${\displaystyle \{0\leq x<15\}}$

同様に、else部分では、代入規則 により、

${\displaystyle \{0\leq 0\leq 15\}x:=0\{0\leq x\leq 15\}}$ 、または同等

${\displaystyle \{{\texttt {true}}\}x:=0\{0\leq x\leq 15\}}$ 、

したがって、前提条件を再度強化するために、と がそれぞれと である場合に結果規則を適用する必要があります。非公式には、結果規則の効果は、else部の入口で既知であるを「忘れる」ことです。これは、 else部で使用される代入規則がその情報を必要としないためです。 ${\displaystyle P_{1}}$ ${\displaystyle P_{2}}$ ${\displaystyle \{x=15\}}$ ${\displaystyle \{{\texttt {true}}\}}$ ${\displaystyle \{x=15\}}$

ルール中

${\displaystyle {\dfrac {\{P\wedge B\}S\{P\}}{\{P\}{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}\{\neg B\wedge P\}}}}$

ここでPはループ不変式であり、ループ本体Sによって保持されます。ループ終了後もこの不変式Pは保持され、さらにループの終了を引き起こしたはずです。条件規則と同様に、B は副作用を持ってはなりません。 ${\displaystyle \neg B}$

例えば、

${\displaystyle \{x\leq 10\}{\texttt {while}}\ x<10\ {\texttt {do}}\ x:=x+1\ {\texttt {done}}\{\neg x<10\wedge x\leq 10\}}$

whileルールによって証明する必要がある

${\displaystyle \{x\leq 10\wedge x<10\}x:=x+1\{x\leq 10\}}$ 、または簡略化された

${\displaystyle \{x<10\}x:=x+1\{x\leq 10\}}$ 、

これは割り当て規則によって簡単に得られます。最終的に、事後条件はと簡略化されます。 ${\displaystyle \{\neg x<10\wedge x\leq 10\}}$ ${\displaystyle \{x=10\}}$

別の例として、while 規則を使用すると、 xが整数変数でaが平方数でない 場合でも、任意の数aの正確な平方根xを計算する次の奇妙なプログラムを正式に検証できます。

${\displaystyle \{{\texttt {true}}\}{\texttt {while}}\ x\cdot x\neq a\ {\texttt {do}}\ {\texttt {skip}}\ {\texttt {done}}\{x\cdot x=a\wedge {\texttt {true}}\}}$

Pが真である間に規則を適用した後、証明する必要があるのは

${\displaystyle \{{\texttt {true}}\wedge x\cdot x\neq a\}{\texttt {skip}}\{{\texttt {true}}\}}$ 、

これはスキップルールと結果ルールから導き出されます。

実際、この奇妙なプログラムは部分的には正しい。もしプログラムが偶然に終了したのであれば、x には（偶然に）aの平方根の値が含まれていたに違いない。それ以外の場合にはプログラムは終了しないので、完全に正しいわけではない。

完全な正確さのルール

上記の通常のwhile規則を以下の規則に置き換えると、ホーア計算は部分的な正しさだけでなく、完全な正しさ、つまり停止性を証明するためにも使用できます。プログラムの正しさの概念が異なることを示すため、ここでは中括弧ではなく角括弧が一般的に使用されます。

${\displaystyle {\dfrac {<\ {\text{is a well-founded ordering on the set}}\ D\quad ,\quad [P\wedge B\wedge t\in D\wedge t=z]S[P\wedge t\in D\wedge t<z]}{[P\wedge t\in D]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[\neg B\wedge P\wedge t\in D]}}}$

この規則では、ループ不変条件の維持に加えて、ループバリアントと呼ばれる式tによって終了が証明されます。この式は、各反復処理において、あるドメインセットD上のwell-founded 関係<に関して厳密に減少します。<は well-founded であるため、 Dのメンバーの厳密に減少するチェーンは有限の長さしか持つことができず、t が永久に減少し続けることはできません。(例えば、通常の順序<は正の整数については well-founded ですが、整数や正の実数については well-founded ではありません。これらの集合はすべて数学的な意味で意味され、計算上の意味では意味されません。特に、これらはすべて無限です。) ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {Z} }$ ${\displaystyle \mathbb {R} ^{+}}$

ループ不変式Pが与えられた場合、条件BはtがDの最小元ではないことを意味している必要がある。そうでなければ、本体S はt をそれ以上減少させることができないため、規則の前提は偽となる。（これは完全な正しさを表す様々な表記法の1つである。） ^{[注 3 ]}

前のセクションの最初の例を再び取り上げると、

${\displaystyle [x\leq 10]{\texttt {while}}\ x<10\ {\texttt {do}}\ x:=x+1\ {\texttt {done}}[\neg x<10\wedge x\leq 10]}$

完全な正しさのwhile規則は、例えばDが通常の順序の非負整数であり、式tが で ある場合に適用でき、次に次のことを証明する必要がある。 ${\displaystyle 10-x}$

${\displaystyle [x\leq 10\wedge x<10\wedge 10-x\geq 0\wedge 10-x=z]x:=x+1[x\leq 10\wedge 10-x\geq 0\wedge 10-x<z]}$

非公式に言えば、ループ サイクルごとに距離が減少し、常に非負のままであることを証明する必要があります。このプロセスは、有限数のサイクルでのみ実行できます。 ${\displaystyle 10-x}$

これまでの証明目標は次のように簡略化できる。

${\displaystyle [x<10\wedge 10-x=z]x:=x+1[x\leq 10\wedge 10-x<z]}$ 、

これは次のように証明できます。

${\displaystyle [x+1\leq 10\wedge 10-x-1<z]x:=x+1[x\leq 10\wedge 10-x<z]}$ 割り当て規則によって得られ、

${\displaystyle [x+1\leq 10\wedge 10-x-1<z]}$ 結果ルールによって強化することができます。${\displaystyle [x<10\wedge 10-x=z]}$

前のセクションの 2 番目の例では、もちろん、空のループ本体によって減少する式tは見つからないため、終了は証明できません。

参照

• アサーション（ソフトウェア開発）
• 表示的意味論
• 契約による設計
• 動的ロジック
• 形式検証
• ループ不変
• 述語変換子の意味論
• 静的プログラム解析
• 分離ロジック

注記

1. Hoare は元々「」ではなく「」と書いていました。${\displaystyle P\{C\}Q}$ ${\displaystyle \{P\}C\{Q\}}$
2. この記事では、規則について自然演繹法の表記法を用いています。例えば、 は非公式には「 αとβの両方が成り立つならば、 φも成り立つ」という意味です。αとβは規則の前提（前件）、 φは後件（後件）と呼ばれます。前提のない規則は公理と呼ばれ、 と表記されます。${\displaystyle {\dfrac {\alpha ,\beta }{\phi }}}$ ${\displaystyle {\dfrac {}{\quad \phi \quad }}}$
3. Hoareの1969年の論文では完全な正しさの規則は示されていませんでした。p.579（左上）の彼の議論を参照してください。例えば、Reynoldsの教科書^{[ 6 ]}では、次のような完全な正しさの規則が示されています： zがP、 B、 S、 tのいずれにも自由に出現しない整数変数であり、 tが整数式である 場合（Reynoldsの変数名は本論文の設定に合わせて変更されています）。${\displaystyle {\dfrac {P\wedge B\rightarrow 0\leq t\quad ,\quad [P\wedge B\wedge t=z]S[P\wedge t<z]}{[P]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[P\wedge \neg B]}}}$

参考文献

1. ホーア 1969 .
2. フロイド 1967 .
3. レイノルズ、2009 年、セクション。 3.4、p. 64.
4. Huth & Ryan 2004 .
5. Apt & Olderog 2019 .
6. レイノルズ 2009 .

参考文献

• Apt, Krzysztof R.; Olderog, Ernst-Rüdiger (2019年12月). 「Hoareの論理の50年」 . Formal Aspects of Computing . 31 (6): 759. doi : 10.1007/s00165-019-00501-3 . S2CID  102351597 .

• フロイド, RW (1967). 「プログラムへの意味の付与」(PDF) .アメリカ数学会報. 応用数学シンポジウム. 19 : 19–31 .

• Hoare, CAR (1969年10月). 「コンピュータプログラミングの公理的基礎」 . Communications of the ACM . 12 (10): 576– 583. doi : 10.1145/363235.363259 . S2CID  207726175 .

• Huth, Michael; Ryan, Mark (2004年8月26日). 『コンピュータサイエンスにおける論理：システムのモデリングと推論』（第2版）. Cambridge University Press . pp. XIV, 427. ISBN 978-0521543101。

• レイノルズ、ジョン・C. (2009) [1998].プログラミング言語理論.ケンブリッジ大学出版局. ISBN 9780521106979。

• テネント、ロバート・D. (2002). 『ソフトウェアの仕様』ケンブリッジ大学出版局. pp. XII, 289. ISBN 9780521004015ホーア論理の入門を含む教科書

外部リンク

• KeY-Hoareは、 KeY定理証明器をベースに構築された半自動検証システムです。シンプルなwhile言語のためのHoare計算を備えています。
• j-Algo Hoare 計算モジュール( GitHubのj-Algo、SourceForgeのj-Algo ) – アルゴリズム視覚化プログラム j-Algo での Hoare 計算の視覚化。