ホーア論理 | Nola's Backyard

ホーアトリプルを導くための公理と推論規則からなる体系。公理的意味論を与える代表的な方法の1つ。

各構文要素に対応する規則を使い、部分的なプログラムについての性質から、プログラム全体についての性質を導く。

Example

例えば、while文には次の推論規則を使う。

\frac{ \{I\land b\}\;C\;\{I\} }{ \{I\}\;\mathbf{while}\ b\ \mathbf{do}\ C\;\{I\land\neg b\} }

$I$ はループ不変条件であり、「条件 $b$ が真のときに本体 $C$ を実行しても $I$ が保たれる」ことから、while文全体の実行後には $I\land\neg b$ が成り立つと導く。