ホアの論理

空文ルールは、 skip文はプログラムの状態を変更しないと主張しており、したがってskip文の前に真であったことは、その後も真であり続ける。^{[注2 ]}

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

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

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

どこ${\displaystyle P[E/x]}$これは、 xの各自由出現が式Eに置き換えられた主張Pを表します。

割り当て公理スキームは、${\displaystyle P[E/x]}$これは、 Pの割り当て後の真理値と同等である。したがって、${\displaystyle P[E/x]}$代入前に真であれば、代入公理により、代入後にはPが真となる。逆に、${\displaystyle P[E/x]}$偽（つまり${\displaystyle \neg P[E/x]}$代入文の前に P が true であれば、その後はPは false でなければならない。

有効なトリプルの例としては、以下のようなものがあります。

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

式によって変更されないすべての前提条件は、事後条件に引き継ぐことができます。最初の例では、${\displaystyle y:=x+1}$それは事実を変えない${\displaystyle x+1=43}$、したがって、両方のステートメントが事後条件に現れる可能性があります。形式的には、この結果は、 Pが (である公理図式を適用することによって得られます。${\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\}}$

これらは、代入公理スキームの有効なインスタンスである。

Hoare が提案した代入公理は、複数の名前が同じ格納値を参照する可能性がある場合には適用されません。たとえば、

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

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

ホアの合成規則は、逐次実行されるプログラムSとTに適用され、S はTより先に実行され、次のように記述されます。${\displaystyle S;T}$( Qは中間条件と呼ばれる): ^{[ 4 ]}

${\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}}}$

ワンタイムループ構造と同じ効果を持つ

${\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}\}}}}$

このルールは前提条件を強化することを可能にする${\displaystyle P_{2}}$および／または事後条件を弱める${\displaystyle Q_{2}}$例えば、 then部分とelse部分で文字通り同一の事後条件を実現するために使用されます。

例えば、

${\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\}}$

当時の部分については、

${\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\}}$

その他部分について。

しかし、 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\}}$、

したがって、結果ルールを適用する必要がある${\displaystyle P_{1}}$そして${\displaystyle P_{2}}$いる${\displaystyle \{x=15\}}$そして${\displaystyle \{{\texttt {true}}\}}$それぞれ、前提条件を再び強化する。非公式には、結果ルールの効果は、${\displaystyle \{x=15\}}$else部分で使用される代入規則はその情報を必要としないため、 else部分の開始時点では が既知です。

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

ここでPはループ不変量であり、ループ本体Sによって保持されるべきものです。ループが終了した後も、この不変量P は依然として有効であり、さらに${\displaystyle \neg B}$ループを終了させる原因となったに違いない。条件ルールと同様に、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 ルールを使用すると、任意の数aの正確な平方根xを計算する次の奇妙なプログラムを形式的に検証できます。ただし、xは整数変数であり、aは平方数ではありません。

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

Pが真である状態でwhileルールを適用した後、証明すべきことは

${\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によって終了性も証明します。この式 t の値は、各反復中に、あるドメイン集合D上の整礎関係<に関して厳密に減少します。 <は整礎であるため、Dの要素の厳密に減少する連鎖は有限の長さしか持ち得ません。したがって、t は永遠に減少し続けることはできません。（例えば、通常の順序<は正の整数に対して整礎です。）${\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は見つからないため、終了性を証明することはできません。