形式手法

formal-methodscomputer-science

数学的な手法でソフトウェアの正しさを保証する技術の総称。

プログラマ向けの一言

テストは「バグがある」ことを示せるが、「バグがない」ことは示せない。形式手法は「バグがない」ことを数学的に証明する。

テストとの違い

// テスト: 有限個の入力を試す
test("add", () => {
  expect(add(1, 2)).toBe(3);
  expect(add(0, 0)).toBe(0);
  expect(add(-1, 1)).toBe(0);
  // ...でも全部の入力は試せない
});

// 形式手法: 「すべての入力に対して」正しいことを証明する
// ∀ x, y ∈ Int: add(x, y) === x + y
// これはテストでは不可能。数学的証明が必要。

3つのアプローチ

// 1. 定理証明 (Theorem Proving)
// 「この関数は仕様を満たす」ことを人間が証明を書いて示す
// → 詳細は [[theorem-proving|定理証明]] を参照

// 2. モデル検査 (Model Checking)
// 状態を全探索して「違反がないか」を自動で調べる
// → 詳細は [[model-checking|モデル検査]] を参照

// 3. 型による検証
// プログラマにとって最も身近な形式手法
// TypeScript の型システムも（限定的な）形式検証

function divide(a: number, b: number): number {
  return a / b; // b === 0 のとき？ → 型では防げない
}

// より強い型（篩型）があれば:
// function divide(a: number, b: NonZero<number>): number
// → コンパイル時に b !== 0 を保証
// → 詳細は [[refinement-type|篩型]] を参照

使い分け: テスト / モデル検査 / 定理証明

同じ「正しさの保証」でも、保証の強さ・自動化・適用場面が違う。カバレッジ（どこまで保証するか）と自動化（人手をどこまで使うか）のトレードオフで並ぶ:

手法保証の強さ自動化コスト適用場面・強み限界
テスト有限個の入力のみ（バグの存在は示せるが不在は示せない）完全自動（書けば走る）低回帰検出・最も普及・どんなコードにも効く試した入力の外は何も言えない
Property-based testing多数のランダム入力 + 縮小。ほぼ全称だが確率的自動（性質は人間が書く）低〜中テストと形式手法の中間。不変条件の発見に強い反例が「無い」ことは保証しない
型による検証型が表す範囲で全入力を静的保証自動（篩型は SMT、依存型は要証明）低〜中日常的・コンパイラに常駐。境界・整合性に強い型で表せる性質に限る
モデル検査状態空間内の全パスを網羅（時相性質・並行性）完全自動（モデル化は人手）中並行・分散プロトコル、デッドロック/レース。反例トレースが出る状態爆発。無限状態は抽象化が要る
定理証明すべての入力に対し数学的に証明（無限状態も可）対話的（人間 + tactic）高最強の保証。アルゴリズム正当性・数学・OS/コンパイラ核証明労力が膨大。専門知識が要る

選び方の指針:

実用されている場所

// 形式手法は「ミスが許されない」領域で使われている:
// - AWS:   S3, DynamoDB の分散プロトコルを TLA+ でモデル検査
// - 航空:  Airbus のフライト制御ソフトウェア
// - 暗号:  TLS 1.3 のプロトコル検証
// - CPU:   Intel の浮動小数点演算の検証（Pentium バグの再発防止）
// - 鉄道:  パリ地下鉄の自動運転システム

// プログラマにとって身近な例:
// - TypeScript の型チェック
// - Rust の借用チェッカー
// - Property-based testing（fast-check 等）← テストと形式手法の中間

押さえどころ（カード化候補）

関連

Graph

Backlinks