第一層: 仕様を書くための数学

連載序論はこちら。この層は、仕様を自然言語から形式言語に降ろすための語彙。この層の選択が、後続のすべて（何が検証でき、何が自動化できるか）を決める。

1.1 ホーア論理と最弱事前条件 [実務厚]

概念: プログラム片 C を事前条件 P・事後条件 Q で挟んだ三つ組 {P} C {Q}。「Pを満たす状態から C を実行して停止すれば Q を満たす」（部分正当性）。停止性まで込みなら全正当性。Dijkstraの最弱事前条件 wp(C, Q) は「停止まで込みでQを保証するために最低限必要な事前条件」を構文から機械的に計算する演算子で、検証条件生成の基礎（本来のwpは全正当性側であり、部分正当性側は通常wlpと呼び分ける）。

代表的成果: Hoare (1969)、Dijkstra『A Discipline of Programming』(1976)。ループにはループ不変条件が必要になる——これが第二層の帰納的不変条件の最小単位。

実務実績: Dafny（wp計算＋Z3で自動検証）、SPARK Ada（航空・防衛の認証案件で数十年の実績）、Why3、JML系。契約プログラミング（Eiffel、各言語のassert文化）はこの論理の軽量版。

刷新での適用: 移行バッチ・変換処理の一件単位の正当性。「この変換は残高総和を保存する」を事後条件として書き、機械検証する。

1.2 時相論理（LTL / CTL）[実務厚（HW）/ 実績有（SW）]

概念: 「いつか」「常に」「〜まで」を演算子に持つ論理。線形時相論理LTLは一本の実行系列上の性質、計算木論理CTLは分岐する未来の上の性質を書く。実務上最も効く語彙は safety / liveness の分離（Alpern–Schneider 1985: あらゆる線形時相性質はsafety性質とliveness性質の共通部分として表せる）。safetyは「悪いことが起きない」（有限反例で反証可能）、livenessは「良いことがいつか起きる」（無限実行でしか反証できない）。この分解は検証手段の選択に直結する——有限のテストで決着できるのは実質safety側のみで、無期限のlivenessは期限を切ってsafety化しない限りテストでは反証しきれない。

代表的成果: Pnueli (1977)、Clarke–Emerson–Sifakisのモデル検査（いずれもチューリング賞）。公平性（fairness）——「スケジューラが特定プロセスを永遠に飢えさせない」という仮定なしにlivenessはまず証明できない。

実務実績: ハードウェア検証ではSVA/PSLとして完全に標準化。ソフトウェアではTLA+（LamportのTLAは時相論理の一種）がAmazon・Microsoft・MongoDB等で採用。

刷新での適用: 切替手順・縮退設計の仕様化。「切替中いかなる時点でも二重引落しは起きない」（safety）と「障害後、最終的に全店舗が新系に収束する」（liveness＋公平性）は種類の違う主張であり、検証手段も別になる。

1.3 型理論と Curry–Howard 対応 [実務厚（軽量版）/ 実績有（重量版）]

概念: 「命題＝型、証明＝プログラム」。仕様を型として書けば、型検査が証明検査になる。依存型（値に依存する型:「長さnのリスト」）まで行くと任意の数学的仕様を型で表現できる。中間に篩型（refinement types:「0以上のint」のように既存型を述語で絞る）があり、SMTソルバで自動検査できる範囲に留めることで実用性を確保する。

代表的成果: Martin-Löf型理論、Coq/Lean/Agda。CompCert（Coqで検証されたCコンパイラ——Csmithによるファジングで、他のコンパイラが多数のバグを出す中、検証済み部分からバグが出なかったことで有名）。seL4（Isabelle/HOLで機能的正当性を証明したマイクロカーネル。C実装約8700行に対し証明約20万行・約20人年）。HACL/EverCrypt（Fで検証された暗号ライブラリ、Firefoxに搭載）。

実務実績: 重量級（フル依存型）は「小さく死活的なコア」で実績。軽量級はRustの型システム（所有権・ライフタイム）として大規模普及——これは次項の分離論理の親戚が型に埋め込まれた例と見なせる。

刷新での適用: 金額・通貨・口座状態のような業務量を型で区別する（幽霊型・newtype戦術）だけでも、単位混同・状態遷移違反のクラス全体を消せる。費用対効果は軽量側が圧倒的に高い。

1.4 分離論理 [実務厚]

概念: ヒープを扱うためのホーア論理の拡張。分離積 P ∗ Q（PとQが互いに素なヒープ領域で成立）と frame rule（局所的な証明が、触っていない残りの世界を保ったまま大域に持ち上がる）が核。「局所推論の合成で大域の正しさを得る」という思想の最も成功した実装。並行版（CSL）はロックが守る資源の所有権移転を扱う。

代表的成果: Reynolds–O'Hearn (2002)。研究最前線はIris（高階並行分離論理、Coq上）。RustBeltはRustの型システムの健全性をIrisで証明した。

実務実績: MetaのInferが代表——分離論理ベースの静的解析を毎日のCIで回し、null参照・メモリリーク類を差分解析で検出。「証明」ではなく「バグ検出」に振ったことで産業スケールに乗った点が教訓的。

刷新での適用: 直接にはC/C++資産の解析。思想としては「frame rule的に、変更の影響範囲を証明可能な形で局所化する」ことがモジュール分割の設計原理になる。

1.5 代数的仕様と性質ベーステスト [実務厚（テスト側）]

概念: データ型を操作と等式法則で仕様化する（例: pop(push(x, s)) = s）。始代数意味論により「法則を満たす最小のモデル」が仕様の標準的意味になる。等式推論はリファクタリングの正当性そのもの。

実務実績: 代数的仕様言語（CASL等）自体は普及しなかったが、性質ベーステスト（QuickCheck系）として実質的に生き残った——法則を書き、ランダム入力で反例を探す。法則の経験的検査であって証明ではないが、費用対効果が非常に高い。

刷新での適用: 逆生成した仕様の検収手段として最有力。「新旧システムは任意の取引列に対し同一の残高を返す」という差分性質を書き、生成した取引列で叩く——差分テストと性質ベーステストの合流点であり、現行システムをオラクルとして使う刷新戦略の数学的土台はここにある。

---

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

1. 序論 — 地図の全体像
2. 第一層: 仕様を書くための数学（この記事）
3. 第二層: 仕様と実装の関係の数学
4. 第三層: 合成の数学
5. 第四層: 不可能性と限界の数学
6. 横断層: 検証を実行する手段の数学
7. 総括: 実績濃淡マップと大規模刷新への適用