ホーア論理

ホーア論理（フロイド・ホーア論理またはホーア規則とも呼ばれる）は、コンピュータプログラムの正しさについて厳密に推論するための一連の論理規則を備えた形式体系である。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 年の論文で、ホーアは、実装の制限違反がないことも意味する、より狭い終了の概念を使用していました。そして、アサーションを実装に依存しないようにするより広い終了の概念を好みました。^[4]

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

空文ルールは、 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\}}$

ホーアの合成規則は、連続して実行されるプログラムSとTに適用され、SはTより先に実行され、次のように記述される（Qは中間条件と呼ばれる）。^[5]${\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文全体の事後条件でもあることを規定している。 ^[6] 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}}}$

条件ルールは、他の Hoare ルールから派生できます。同様に、forループ、do...untilループ、switch、break、continue などの他の派生プログラム構造のルールも、プログラム変換によって Hoare の元の論文のルールに簡略化できます。

${\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 は見つからないため、終了は証明できません。

• Robert D. Tennent. Specifying Software (2002 年に書かれた Hoare 論理の入門を含む教科書) ISBN 0-521-00401-2 

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