ホーア論理とプログラム検証

なぜテストの先にホーア論理があるのか

テストは「ある入力でバグが出た」ことは示せても、「あらゆる入力でバグがない」ことは示せません。入力空間は通常無限なので、有限のテストでは原理的にカバーしきれないからです。ホーア論理は、この穴を埋めるためにプログラムの正しさを数学の証明として与える枠組みです。1969年に C.A.R. ホーアが提案し、今日の形式検証ツール（Dafny、Frama-C、各種SMTベース検証器）の理論的土台になっています。

実務上の効きどころは、入力の網羅が現実的でない場所——金融計算、暗号、並行制御、コンパイラ最適化の正当性——にあります。テストの限界についてはテストの基礎も参照してください。

ホーアの三つ組と部分正当性

中心となる記法がホーアの三つ組 {P} C {Q} です。意味は次の通りです。

事前条件 P が成り立つ状態でプログラム C を実行し、もし C が停止するなら、停止後の状態で事後条件 Q が成り立つ。

ここで P（precondition）と Q（postcondition）は、プログラム変数についての論理式（表明、assertion）です。例えば {x > 0} y := x + 1 {y > 1} は妥当な三つ組です。

推論規則：三つ組を組み立てる文法

ホーア論理は、プログラムの構文要素ごとに「正しい三つ組を導く規則」を持ちます。これらを組み合わせて、プログラム全体の三つ組を証明します。

代入の公理が最も重要かつ直感に反します。{Q[E/x]} x := E {Q}。Q[E/x] は「Q の中の x をすべて E で置き換えた式」です。事後から事前へ後ろ向きに計算する点が要点で、例えば事後条件 y > 0 から x := x + 1 の事前条件を得るには、y を含む式に置換規則を当てはめます。

帰結規則は橋渡し役です。事前条件はより強い（厳しい）ものに、事後条件はより弱い（緩い）ものに置き換えてよい、というこの規則がないと、各文の三つ組をつなげられません。連接で必要になる中間表明 R の調整も、この規則が支えています。条件分岐の b はプログラムの分岐条件で、各枝の中では b の真偽が事前条件に加わります（制御構文 の分岐・ループに対応）。

最弱事前条件：証明を機械化する

規則を手で当てはめるのは大変です。エドガー・ダイクストラが導入した**最弱事前条件（weakest precondition, wp）**は、これを計算可能な関数に変えます。

wp(C, Q) とは「C を実行して Q を確実に成立させられる、最も緩い事前条件」です。「最も緩い」とは、Q を保証するどんな事前条件 P（{P} C {Q} が妥当なもの）に対しても P ⇒ wp(C, Q) が成り立つ、という意味です。したがって {P} C {Q} が妥当かどうかは、P ⇒ wp(C, Q) という論理式が恒真かを確かめる問題に帰着します。この最後の含意式を**検証条件（verification condition）**と呼び、現代の検証器はこれをSMTソルバに投げて自動判定します。

主要な計算規則は次の通りです。

wp(skip, Q)        = Q
wp(x := E, Q)      = Q[E/x]                  // 代入は後ろ向き置換
wp(C1; C2, Q)      = wp(C1, wp(C2, Q))       // 内側から外へ合成
wp(if b then C1 else C2, Q)
                   = (b ⇒ wp(C1, Q)) ∧ (¬b ⇒ wp(C2, Q))

連接の規則が示す通り、wp は事後条件から事前条件へ向かって、文を逆順に伝播します。直線的なコード（ループなし）なら、この計算は完全に機械的で、検証は決定可能な領域に収まります。

ループ不変条件：無限を有限の証明に畳む

ループは反復回数が入力依存で一般に未知なので、wp を素朴に展開できません。ここで鍵となるのがループ不変条件（loop invariant）I です。I は次の3つを満たす表明です。

1. 初期化：ループ突入前に I が成り立つ（P ⇒ I）。
2. 保存：ループ本体を1回回しても I が保たれる（{I ∧ b} body {I}、b はループ継続条件）。
3. 終了：ループを抜けた時点で目的の事後条件が出る（I ∧ ¬b ⇒ Q）。

数学的帰納法とまったく同じ構造です。「最初に成り立ち、1回回しても保たれる」なら、何回回った後でも成り立つ——だから反復回数を知らずに、無限個の状態をまとめて押さえられます。これが「無限を有限の証明に畳む」仕組みの核心です。

具体例として、0 から n-1 までの総和を求めるループを考えます。

{ n >= 0 }
s := 0; i := 0;
// 不変条件 I: s = (0 + 1 + ... + (i-1)) かつ 0 <= i かつ i <= n
while i < n do
    s := s + i;
    i := i + 1
{ s = 0 + 1 + ... + (n-1) }

ループを抜けると継続条件 i < n の否定、すなわち i が n 以上 が成り立ち、不変条件の i が n 以下 と合わせて i = n が確定します。これを I の総和式に代入すると、ちょうど事後条件 Q が得られます。

停止性証明：完全正当性へ

不変条件は部分正当性しか保証しません。「停止すれば正しい」を「正しく停止する」へ格上げするには、ループが必ず終わることを別に示します。使うのが変分関数（variant, ランク関数）V です。

V はプログラム状態から整礎な順序を持つ集合（典型的には自然数）への写像で、次を満たします。

• ループ本体を1回回すたびに V の値が真に減少する（{I ∧ b ∧ V = z} body {V < z}）。
• ループ継続中は V が下限を割らない（自然数なら I ∧ b ⇒ V >= 0）。

自然数は無限に減り続けられない（整礎性）ので、本体を回るたびに必ず減る量が下限付きで存在するなら、ループは有限回で停止します。先の総和ループでは V = n - i が変分関数です。毎回 i が1増えるので n - i は1ずつ減り、i が n 未満の間は非負——ゆえに停止します。

不変条件（部分正当性）と変分関数（停止性）がそろって初めて完全正当性が証明できます。これは「停止する」という性質そのものを扱うため、計算可能性と決定不能問題 で見た停止性問題の決定不能性と地続きです。停止性は一般には自動判定できないからこそ、人が変分関数を与えて個別に証明するのです。

形式検証の射程とテストとの補完

ホーア論理に基づく検証は、テストと役割が異なります。テストは具体的な実行で反例を探すのに対し、検証は全入力にわたる正しさを証明する。両者は補完関係で、プロパティベーステスト は「不変条件・事後条件を多数のランダム入力で叩く」点で、形式仕様と相性が良いアプローチです。

まとめ

• ホーアの三つ組 {P} C {Q} は部分正当性の主張で、代入・連接・条件・帰結の推論規則を組み合わせてプログラム全体の正しさを導きます。
• 最弱事前条件 wp(C, Q) は証明を機械化する道具で、検証を検証条件（論理式の恒真性）に還元します。直線コードでは完全に自動化できます。
• ループは不変条件で部分正当性を、整礎な変分関数で停止性を示します。不変条件は数学的帰納法と同型で、無限の反復を有限の証明に畳む装置です。両者がそろって完全正当性が言えます。

テストが「ある入力での観測」なら、ホーア論理は「すべての入力に対する証明」です。検証の難所が不変条件と停止性の発見に集約されることを理解すると、形式検証ツールがどこで人手を要し、どこを自動化できるのかが見通せるようになります。