システム設計と大規模刷新のための数学（序論）— 地図の全体像

Claudeと大規模システム刷新の失敗談を肴に話していたら、「刷新に使える数学」の話が思いのほか面白い形にまとまったので、連載として整理しておく。素材はClaudeとの対話だが、切り出しの判断と間違いの責任はこちらにある。

この連載は、システム設計・大規模刷新・仕様の正しさに使える数学的な考え方を、四つの層＋横断層に整理した地図である。各項目は原則として「概念 / 代表的成果 / 実務実績 / 大規模刷新での適用箇所」の四点で書く。

まず一番大事な区別: Verification と Validation

数学が直接扱えるのは verification（実装が仕様を満たすか）である。validation（仕様が本当に望んだものか）にも形式化できる部分はあるが、その中核——形式モデルが利用者の目的と運用環境を十分に表しているかという対応関係——は内部証明だけでは閉じない。仕様は形式体系と現実の境界面であり、その妥当性の最終判断は人間に残る。上位目的を形式化すれば一段をverification側へ移せるが、モデル妥当性の問いはさらに外側へ移るだけである。Boehmの言い換えで言えば「Are we building the product right?」がverification、「Are we building the right product?」がvalidation。

ただし仕様「自体」にも形式的に検査できる性質がある。

無矛盾性（充足可能性）: 書いた性質群を同時に満たすモデルが存在するか。矛盾した仕様はあらゆる実装を排除する。SATソルバ・モデル検査器で機械検査できる。

実現可能性（realizability）: 環境がどう振る舞っても仕様を満たし続ける実装（戦略）が存在するか。Pnueli–Rosner（1989）がopen systemに対して定式化した。充足可能でも実現可能とは限らない——「環境が都合よく動けば満たせる」仕様は、実装としては書けない。

空虚性（vacuity）: 「Aならば必ずB」型の性質が、Aが一度も起きないせいで自明に成立していないか。仕様が「通っているのに何も検証していない」状態の検出。ハードウェア検証では標準的な検査。

カバレッジ: 書いた性質群が、想定シナリオや変異させた実装をどれだけ区別できるか。仕様の網羅度の経験的測定で、mutation testingの仕様版に相当する。

「仕様の正しさも数学でいける」の代表的な範囲がこの四つ（網羅ではない——完全性・追跡性・仮定の無矛盾性なども形式検査の対象になる）。仕様が業務として正しいかは、依然として人間の裁定事項である。

地図の全体像

第一層: 仕様を書くための数学 — ホーア論理、時相論理、型理論、分離論理、代数的仕様
第二層: 仕様と実装の関係の数学 — 精緻化、帰納的不変条件、双模倣、抽象化写像
第三層: 合成の数学 — rely-guarantee、振る舞い部分型、セッション型、CRDT/CALM、圏論的データ移行
第四層: 不可能性と限界の数学 — Rice、FLP、CAP、状態爆発
横断層: 検証を実行する手段の数学 — モデル検査、抽象解釈、SMT、定理証明、経験的手法
総括: 実績濃淡マップと大規模刷新への適用

較正方針

各項目に実務実績の濃淡を明記する。[実務厚]（産業で継続運用）、[実績有]（著名事例はあるが採用は限定的）、[理論先行]（理論は成熟、産業採用ほぼなし）の三段階。理論として綺麗なだけか、現場で回っているかの濃淡自体を記録することが、この地図の価値の半分だと思っている。

なお、各記事の「刷新での適用」はこの連載独自の対応付けであり、実プロジェクトでの検証実績があるものではない。仮説として読んでほしい。

連載: システム設計と大規模刷新のための数学