トニー・ホアの正しさの考え：論理から安全なコードへ

「正しさ」は「動いた」に留まらない

人がプログラムを「正しい」と言うとき、多くは「何回か実行して出力が良さそうだった」という意味で使います。それは有益なシグナルですが、正しさそのものではありません。平たく言えば、正しさとはプログラムが仕様を満たすこと：許容されるすべての入力に対して要求される結果を出し、状態変化やタイミング、エラー処理に関するルールを守ることです。

しかし「仕様を満たす」は思ったより難しいのが現実です。

正しさが難しい理由

まず、仕様はしばしば曖昧です。要件が「リストをソートする」と言っても、それは安定ソートを意味するのか？重複値や空リスト、非数値要素はどう扱うのか？仕様が明示しない場合、人によって解釈が分かれます。

次に、エッジケースは稀ではなく、単にテストされにくいだけです。null 値、オーバーフロー、オフバイワンの境界、異常なユーザー操作列、外部障害が「見た目は動く」コードを本番で壊します。

さらに、要件は変わります。昨日の仕様に対して正しかったコードが、今日の仕様では間違っていることがあります。

この記事で期待すべきこと

トニー・ホアの大きな貢献は「すべてを常に証明しろ」という主張ではありませんでした。彼の示したのは、コードが何をすべきかをより正確に書き、それについて規律立てて推論できるようにする考え方です。

この記事では三本のつながる糸を辿ります：

• ホア論理：前提と結果を使った軽量で構造化された推論。
• クイックソート：分割（partition）のような小さく「明白に見える」ステップが注意を要することを示す身近なアルゴリズム。
• 安全性の考え方：失敗が現実の被害につながるときの実務的な正しさ。

ほとんどのチームがすべてを形式的に証明するわけではありませんが、部分的な「証明スタイル」の思考でもバグが見つかりやすくなり、レビューの精度が上がり、出荷前に挙動が明確になります。

トニー・ホアを簡単に：日常のコードに浸透した考え方

トニー・ホアは、論文や講義室に留まらなかった稀有な計算機科学者の一人です。学界と産業界を行き来し、すべてのチームが直面する実践的な問い――特に利害が大きいときに「どうやってプログラムが想定どおり動くと分かるのか？」に取り組みました。

本稿で重要になる貢献

この記事は実際のコードベースで何度も現れるホアの考えを中心に扱います：

• ホア論理：前提、結果、そしてよく知られた ホア三重項 {P} C {Q} を使って振る舞いを記述する方法。
• ループ不変式：ループを「動いた」で片付けないための規律。
• クイックソート：特に パーティション 歩あり、正しさを明確に述べることで多くが見える例。
• 安全性（Safety）思考：正しさは贅沢ではなく、迷惑と危害の差になるという考え方。

この記事でしないこと

ここでは数学的な厳密性に深く踏み込んだり、クイックソートの機械検証済みの完全な証明を試みたりはしません。狙いは概念を平易に保つこと：あなたの推論を明確にするのに十分な構造を提示し、コードレビューを大学院セミナーにしないことです。

なぜ日常のプログラミングに効くのか

ホアの考え方は、関数が依存する仮定、呼び出し側に保証すること、ループ中に保つべきこと、レビュー中に「ほぼ正しい」変更を見抜く方法といった日常的な判断に落とし込まれます。{P} C {Q} を明示しなくても、その形で考えるだけで API、テスト、議論の質が上がります。

実務での「正しさ」の意味

ホアの見方は「いくつかの例で通った」より厳密です：正しさとは合意された約束を満たすことであり、少数の成功例で判断するものではありません。

要件 vs 仕様 vs 実装

• 要件 は平易なビジネス上の必要（ステークホルダーの望み）。
• 仕様 はその必要を正確かつ検査可能にしたもの（関数が何をしなければならないか）。
• 実装 はあなたが書いたコード（それがどうやってやるか）。

バグは多くの場合、中間の仕様を省略して要件から直接実装に飛ぶときに生じます。

部分的正しさと全体的正しさ

しばしば混同される二つの主張：

• 部分的正しさ：コードが戻ればその結果は正しい。
• 全体的正しさ：コードは必ず戻り、その結果は正しい（終了性も含む）。

現実のシステムでは、終了しないことが「誤動作」と同じくらい有害なことがあります。

正しさは常に仮定に依存する

正しさの主張は普遍的ではなく、次のような仮定に依存します：

• 入力（例：リストがメモリに収まる、要素が比較可能）
• 制約（例：時間制限、整数範囲）
• 環境（例：並行性、I/O 障害、設定）

仮定を明示することで「自分のマシンで動いた」が他人にも意味を持つようになります。

小さな仕様例

関数 sortedCopy(xs) を考えます。

有用な仕様の例：「新しいリスト ys を返す。(1) ys は昇順にソートされている、(2) ys は xs と同じ要素（同じ個数）を含む、(3) xs は変更されない。」

ここで「正しい」とは、上の三点が述べられた仮定の下で満たされることを意味します。単に出力がざっと見てソートされているだけではありません。

ホア論理の基本：前提・結果・三重項

ホア論理はコードについて、契約のような明快さで話す方法です：「もしある状態が前提を満たしていて、このコード片を実行すれば、ある保証が成立する」。

中心になる表記は ホア三重項 です：

{precondition} program {postcondition}

前提（precondition）：何を仮定するか

前提は 実行前に真でなければならない 事実を述べます。それは希望ではなく、コードが必要とする条件です。

例：ある関数がオーバーフロー検査なしで二つの数の平均を返す場合。

• 前提: a + b が整数型に収まること
• プログラム: avg = (a + b) / 2
• 結果: avg は a と b の数学的平均に等しい

前提が満たされないと、結果の保証は成り立ちません。三重項はそれを明示させます。

結果（postcondition）：何を保証するか

結果は 実行後に真である べきことを述べます（前提が成り立っていることを条件に）。良い結果は具体的で検査可能です。「結果が有効」はなく、「ソートされている」「非負である」「特定のフィールドだけが変更される」といった形で書きます。

代入と逐次実行（記号を増やさずに）

ホア論理は小さな文から複数ステップのコードまで拡張できます：

• 代入 は状態を正確に変えます。x = x + 1 の後に x についてどんな事実が成り立つかを考えます。
• 逐次実行（「まずこれをやり、次にそれをやる」）は保証をつなぎます：ステップ1 がステップ2 の前提を満たしていれば、ブロック全体をより信頼しやすくなります。

目的は波かっこをコード中にばらまくことではなく、意図を読みやすくすることです：明確な前提、明確な結果、そしてレビューでの「動いたっぽい」議論を減らします。

実務で書けるループ不変式

ループ不変式 は、ループが始まる前、各反復後、ループ終了時に真である文です。単純な考え方ですが効果が大きく、反復の各段階で実際にチェックできる主張に置き換えます。

なぜ不変式が曖昧な推論を止めるのか

不変式がないとレビューは「リストを反復してだんだん直す」といった曖昧な説明になりがちです。不変式は「今この時点で何が既に正しいか」を明確にします。これが明確になるとオフバイワンや見落としは、不変式が破られる瞬間として分かりやすくなります。

再利用できる不変式テンプレート

日常の多くのコードは、いくつかの信頼できるテンプレートで扱えます。

1. 境界／インデックス安全

インデックスを安全な範囲に保つ。

• 0 <= i <= n
• low <= left <= right <= high

この不変式は範囲外アクセスを防ぎ、配列の議論を具体化します。

2. 処理済みと未処理の項目の分割

データを「済んだ領域」と「まだ」の領域に分ける。

• 「a[0..i) のすべての要素は検査済み」
• 「result に移したすべての要素はフィルタ述語を満たす」

これにより漠然とした進捗が「今何が済んでいるか」という契約に変わります。

3. ソート済みプレフィックス（またはパーティション済みプレフィックス）

ソートやマージ、パーティションで一般的。

• 「a[0..i) はソートされている」
• 「a[0..i) の全要素は <= pivot、a[j..n) の全要素は >= pivot」

配列全体がまだソートされていなくても、何が確定しているかが定まります。

終了性を平易に主張する：縮む測度

正しさは単に正しいことだけでなく、ループが 終わる ことも含みます。簡単な主張方法は、各反復で縮む測度（バリアント）を名付けることです。

例：

• 「n - i は毎回 1 ずつ減る」
• 「未処理項目の数が減る」

縮む測度が見つからなければ、それは無限ループの実際的リスクを示しています。

Quicksort：コードを推論するためのケーススタディ

Quicksort の約束はシンプルです：配列の区間を与えられれば、その要素を非減少順に並べ替え、要素を失ったり新しく作ったりしないこと。アルゴリズムの高レベルは簡潔にまとめられます：

1. pivot 値を選ぶ。
2. 範囲を パーティション して「pivot より小さい」要素は片側に、「大きい」要素は反対側へ移す（等しい要素の扱いのルールを含む）。
3. 左右の部分範囲に 再帰 を掛ける。

Quicksort は教示用に優れています：頭に収まる大きさでありながら、非形式的な推論が失敗する箇所を浮き彫りにします。ランダムテストで「動いた」ように見えても、特定の入力や境界で間違うことがあります。

「明白に見える」実装を壊す落とし穴

典型的な問題は次の通りです：

• 重複：パーティションが「等しい」要素を一貫して扱わないと、部分範囲が縮まらず無限再帰になったり、パーティションのルールを破ったりする。
• 空や一要素の範囲：基本ケースが曖昧だと範囲外アクセスや無限再帰を招く。
• オフバイワン：二つポインタを使うアルゴリズムでは、比較やインクリメントの1つの誤りが要素のスキップや範囲外スワップを生む。

何を証明する必要があるか

ホア風に正しさを主張するには、通常証明を二つに分けます：

• パーティションの正しさ：パーティション後、左側の各要素は pivot に対して指定された関係を満たし、右側の各要素は逆の関係を満たし、結果は元の要素の置換であること。
• 再帰の正しさ：再帰呼び出しはより小さな範囲に対して行われ（終了性）、それぞれがソートされると仮定すれば全体がソートされること。

この分離により証明は扱いやすくなります：まずパーティションを正しくして、そこからソートの正しさを積み上げます。

パーティションの正しさ：Quicksort の核心

Quicksort の高速さは一見小さなルーチン、partition に依存しています。partition が少しでも間違うと、Quicksort は誤ソート、無限再帰、あるいは境界外アクセスでクラッシュします。

パーティションの契約（保証すべきこと）

ここでは古典的な ホアのパーティション方式（両端から内側へ進む二つのポインタ）を使います。

入力: 配列スライス A[lo..hi] と選ばれた pivot 値（多くの場合 A[lo]）。

出力: インデックス p を返し、以下を満たすこと：

• A[lo..p] の各要素は <= pivot
• A[p+1..hi] の各要素は >= pivot

ここで注意すべきは約束されないこと：pivot が必ず p に収まるとは限らず、pivot と等しい要素はどちらの側にも現れる可能性がある点です。それでも Quicksort は正しい分割を得れば十分です。

走査とスワップ中に保つべき不変式

アルゴリズムが左から i、右から j の二つのインデックスを進めるとき、良い推論は「既に固まったもの」に注目します。実務的な不変式のセットは：

• A[lo..i-1] の要素はすべて <= pivot（左側はクリーン）
• A[j+1..hi] の要素はすべて >= pivot（右側はクリーン）
• A[i..j] は 未分類（まだチェックされていない）

A[i] > pivot と A[j] < pivot を見つけてスワップすれば、不変式は保たれ、未分類領域が縮みます。

カバーすべき境界ケース

• すべて pivot より小さい：i は右へ走り、パーティションは終了して妥当な p を返す必要がある。
• すべて pivot より大きい：j は左へ走り、同様に終了しなければならない。
• 多くの等しい要素：比較に < と <= を混ぜるとポインタが停滞する。ホアの方式は一貫したルールで進行を保証する。
• 既にソート済み / 逆順ソート：性能は劣化しても契約を破らないこと。

Lomuto、Hoare、3-way といった異なるパーティション方式がありますが、重要なのは一つを選び、その契約に対してコードを一貫してレビューすることです。

再帰の推論：基本ケースと終了性

再帰は次の二つが明確に答えられると信頼しやすくなります：「いつ止まるか？」と「各ステップはなぜ有効か？」ホア風の思考は呼び出し前に何が真であるべきか、戻った後に何が真であるかを明示させます。

基本ケースは正確に書く

再帰関数は少なくとも一つの 基本ケース を持ち、そこでは再帰呼び出しを行わずに約束を満たさねばなりません。ソートでは典型的に「長さ 0 または 1 の配列は既にソート済みである」が基本ケースです。ここで「ソート済み」は明示的に：任意の i < j に対して a[i] <= a[j] が成り立つこと。等しい要素の元の順序を保持する性質は安定性と呼ばれ、Quicksort は設計しない限り通常は安定ではありません。

サブ問題が縮むこと

各再帰ステップは厳密に小さい入力に対して自己呼び出しを行うべきです。これは終了性の議論になります：サイズが小さくなり 0 未満にはならないなら、無限再帰は起き得ません。

縮小はスタック安全の観点でも重要です。正しいコードでも再帰深度が大きすぎればクラッシュします。Quicksort では偏った分割が深い再帰を生むので、最悪深さを考慮すべきです。

正しさが先、性能が後

Quicksort の最悪計算量は分割が偏ると O(n^2) に悪化しますが、それは性能の問題であって正しさの欠如ではありません。推論の目標は、パーティションが要素を保存し pivot に従った分割を行うなら、部分範囲の再帰ソートにより全体が定義どおりにソートされる、ということです。

証明スタイルの思考とテスト：両者の関係

テストと証明スタイルの推論は同じ目標――信頼性――に向かいますが、アプローチが異なります。

テストはバグを見つける；推論はバグのクラスを排除する

テストは具体的な間違いを見つけるのが得意です。一方、証明スタイルの推論（特にホア風）は、仕様から出発して「前提が満たされるなら常に結果が成り立つか」を問います。これをうまくやると、境界外アクセスや不変式破壊、終了性問題といったバグのクラスをまとめて排除できます。

仕様はより良いテストケースを生む

明確な仕様はテストの自動生成器になります。ポストコンディションが「出力はソートされ、入力の置換である」と書かれていれば自動的にテスト案が出ます：

• 境界ケース：空リスト、要素1、既にソート済み、逆順
• 不変式：中間プロパティ（例：パーティションが pivot 以下を左に保つ）
• 無効入力：null、NaN、範囲外インデックス、比較子の不整合

仕様は「正しい」とは何かを教え、テストは現実がそれに合っているかを検査します。

プロパティベーステストは実務的な橋渡し

プロパティベーステストは証明と事例テストの中間に位置します。手でいくつかの場合を選ぶ代わりに、性質を表明してツールに多くの入力を生成させます。

ソートに対して有効な二つの性質：

• ソート済み性：結果が非減少順であること。
• 置換性：結果が入力と同じ要素の集合（同じ個数）であること。

これらの性質は実行可能なポストコンディションです。

チームが実際に使えるワークフロー

スケールする軽量な手順：

1. まず仕様を書く（前提、結果、主要不変式）。
2. 厄介な部分について推論する（ループ、パーティション、再帰境界）。
3. 仕様をテストに変える（境界ケース＋プロパティベースチェック）。
4. それらをコードとレビューで一緒に保持する（将来の変更が元の意図を静かに破らないように）。

これを制度化するなら、PR テンプレートやコードレビューのチェックリストに「仕様＋推論ノート＋テスト」を入れると良いでしょう（参照: /blog/code-review-checklist）。

チャットベース生成ワークフロー（vibe-coding 等）を使う場合も同じ規律が必要です。例えば Koder.ai では、実装前に Planning Mode で前提／結果を固め、スナップショットやロールバックを使いながらプロパティベーステストを追加できます。ツールは実装を速めますが、速さが「脆弱さ」に変わらないようにするのは仕様です。

安全性思考：現実世界の影響を考えた正しさ

正しさは単に「正しい値を返す」だけではありません。安全性思考は別の問いを投げかけます：『許容できない結果は何か、それをどう防ぐか――コードが過負荷にさらされたり、誤使用されたり、一部が故障している場合でも？』』実務では、安全性は優先順位付きの正しさです：ある失敗は迷惑に留まり、別の失敗は金銭的損失、プライバシー侵害、身体的危害に繋がる可能性があります。

ハザードとバグ：影響が重要な理由

バグ はコードや設計の欠陥です。ハザード は受け入れがたい結果に至る状況です。一つのバグは文脈によって無害にも危険にもなり得ます。

例：写真ギャラリーのオフバイワンは画像のラベルを誤るかもしれませんが、投薬用量計算の同じミスは患者に危害を及ぼす可能性があります。安全性思考はコード挙動を結果に結びつけることを強制します。

最悪の結果を防ぐ簡単な技術

重い形式手法を導入しなくても即効性のある安全対策が取れます：

• Fail-safe のデフォルト：システムが確信できない場合は安全な振る舞いを選ぶ。例：認可チェックでエラーが起きたら許可するのではなく拒否する。
• 境界での入力検証：ユーザー入力、ファイル、ネットワークデータは信頼せず、型・範囲・フォーマット・不変式を早期に検証する。
• 上限とタイムアウト：メモリ使用、リクエストサイズ、再帰深度、リトライ回数、実行時間に上限を設ける。多くのインシデントは「正しい」コードが過度な入力に対して動いた結果です。

これらの技術はホア式の推論と自然に合います：前提を明示し（どの入力が許容されるか）、結果に安全性の性質（絶対に起きてはならないこと）を含めます。

トレードオフ：チェックは無料ではない

安全チェックにはコストがあります――CPU 時間、複雑さ、あるいは誤検出による拒否の発生頻度。

• 性能 vs チェック：ホットパスは高速であるべきですが、重要な境界には検証、レート制限、タイムアウトを置くべきです。
• 厳格さ vs 使いやすさ：不完全な入力を完全に拒否するとユーザーの不満を招きます。一方で何でも受け入れると曖昧さや悪用を招く。実務的な折衷は「コアでは厳格に、端では寛容に」し、端的なケースの頻度をログと測定で追うことです。

安全性思考は優雅さを証明するより、許容できない故障モードを防ぐことに重きを置きます。

コードレビューでホア式推論を使う方法

コードレビューは正しさ思考の投資対効果が最も高く現れる場です。ホアの基本的な動き――「何が実行前に真であるべきか」「実行後に何が真になるか」を述べる――はレビュー時の問いにそのまま使えます。

ホアのアイデアをレビュー質問に変える

変更を読むとき、主要な関数を小さな約束としてフレーム化してみてください：

• 仮定（前提）：入力、状態、環境について何が真であるべきか？（例：「リストは空でない」「ユーザーは認証済み」「ロックが保持されている」）
• 保証（結果）：終了後に何が真か、戻り値や副作用を含めて？（例：「残高が金額だけ減る」「レコードが一度だけ挿入される」）
• 不変式：ループやリトライ、複数ステップのワークフロー中に何が保たれるか？（例：「processed_count ≤ total」「これまでの借方の合計は貸方の合計に等しい」）
• 障害時の挙動：エラー時にシステムは安全な状態で残るか？部分更新はロールバックされるか？

簡単なレビューハビット：前提／結果を一文で言えないなら、コードは構造が曖昧か注釈が必要です。

重要な関数に「契約コメント」を付ける

リスクの高い関数には署名直上に小さな契約コメントを追加しましょう。具体的に：入力、出力、副作用、エラーを列挙します。

def withdraw(account, amount):
    """Contract:
    Pre: amount is an integer > 0; account is active.
    Post (success): returns new_balance; account.balance decreased by amount.
    Post (failure): raises InsufficientFunds; account.balance unchanged.
    """
    ...

これらは形式的な証明ではありませんが、レビュアーがチェックすべき明確な基準を与えます。

危険コードに対する軽量チェックリスト

パース／検証（不正入力経路、境界ケース）、並行処理（ロック、競合、冪等性、リトライ）、金銭／クォータ（丸め、二重課金、オーバーフロー）、権限（誰が何をできるか）を扱うコードをレビューするときは特に明示的にします。

変更がこれらに触れる場合は「前提は何で、どこで強制されているか？」と「失敗したときでもどんな保証を提供するか？」を必ず確認してください。

形式手法を使うべき時と実務的チェックリスト

形式的推論を全コードベースに導入する必要はありません。やるべきは、普通のレビュー＋テストだけでは足りない「差し迫った箇所」に工夫を注ぐことです。

形式手法が最も効く場所

すべてが依存する小さなクリティカルモジュール（認証、決済ルール、権限、セーフティインターロック）、あるいはオフバイワンの間違いが何ヶ月も隠れる厄介なアルゴリズム（パーサ、スケジューラ、キャッシュ／エヴィクション、パーティション型コード、境界に敏感な変換）に適しています。

実用的なルール：バグが「実害」「大きな金銭損失」「沈黙のデータ破壊」を引き起こす可能性があるなら、普通のレビュー＋テスト以上が必要です。

検討すべきツール（高レベル）

軽量から重い手法まで選択肢があります。多くの場合は組み合わせが効果的です：

• 型システム（非 null、単位／量の型を含む）: 無効な状態の大域的予防。
• 静的解析：怪しい経路、API の誤用、データ競合、汚染された入力フローを検出。
• 契約（前提／結果／アサーション）：ホア風の文を実行可能にしたもの。
• モデル検査：状態機械を探索（プロトコル、並行性、シーケンス検証に有効）。
• 形式検証：最高保証が必要な部分の機械検証された証明。

どこまで踏み込むべきか

踏み込む深さは次を天秤にかけて決めます：

• リスク：影響 × 発生確率。高リスクは強い保証を正当化する。
• コスト：仕様化・証明・保守の時間。
• 変更頻度：頻繁に変わるコードは形式化しにくい。まずインターフェースを安定させる。
• チームスキル：証明が開発速度を落とすなら、まずは契約と静的解析から始める。

実務では「形式度」は段階的に増やせます：明確な契約と不変式から始め、自動化で整合性を保つのが現実的です。Koder.ai のようなツールを使うチームでは、React フロント、Go バックエンド、Postgres スキーマといった複数部分を短いループで生成しつつ、スナップショット／ロールバックで安定性を確保し、CI で契約と静的解析を回すといった運用ができます。

実務的チェックリスト

計画やレビューの段階で「もっと形式化すべきか？」を判断する簡単な門番として使ってください：

1. 最悪の現実的な失敗は何で、誰が被害を受けるか（ユーザー、運用、規制当局）？
2. テストで重要な境界と状態を現実的にカバーできるか？
3. 論理は状態性があるか、並行性があるか、不変式や境界が多いか？
4. 公開エントリポイントに対して明確な前提／結果を書けるか？
5. 小さなコアに分離してより深く検証できるか？
6. どのツールが最もリターンが大きいか（型、静的解析、契約、モデル検査、証明）？
7. 次四半期に何が変わるか、そのとき保証がどう維持されるか？

参考トピック：設計による契約（design-by-contract）、プロパティベーステスト、状態機械のモデル検査、言語向け静的解析、証明支援系の入門資料。