第二層: 仕様と実装の関係の数学

連載序論はこちら。仕様と実装を別々の数学的対象として置き、その間の「正しさを保存する関係」を定義する層。連載全体で一つだけ持ち帰るなら、この層の帰納的不変条件（2.2）だと思っている。

2.1 精緻化（refinement）[実績有〜実務厚（規制産業）]

概念: 抽象仕様から具体実装へ、正当性を保存しながら段階的に降りる関係（厳密には前順序で、振る舞い同値で商を取ってはじめて半順序とみなせる）。抽象データ表現と具体表現の対応は抽象化関数（Hoare 1972）または精緻化関係で与え、操作ごとに前方/後方シミュレーションを証明する。重要な性質は推移性——各段の精緻化を証明すれば全体が言え、巨大な一発証明を段階に分解できる。

代表的成果: 精緻化計算（Back, Morgan）。工学化の代表がB-method / Event-B（Abrial）: 抽象機械から実装まで精緻化を重ね、各段の証明義務を機械生成する。

実務実績: パリ地下鉄14号線（Météor、無人運転の安全制御をBで開発し、稼働後に安全系の欠陥ゼロと報告）、CDG空港シャトル、その後の欧州鉄道信号系。seL4の証明も抽象仕様→実行可能仕様→C実装の二段精緻化の構造。規制が証明を要求する領域で回っている。

刷新での適用: 「旧システムの観測挙動」を最上位の抽象仕様と置き、新実装がその精緻化であることを示す——刷新の正しさの最も素直な定式化。全面適用は重いが、勘定の核（残高計算・利息計算）だけ精緻化で守る部分適用が現実的。

2.2 帰納的不変条件 — この連載の主役 [実務厚（文化として）]

概念: 「初期状態で成り立ち、かつ、どの遷移でも保存される」述語。この二条件（開始・保存）を満たせば、帰納法により全到達可能状態で成立する。ポイントは、守りたい性質（例: 総残高保存）自体は帰納的でないことが多く、それを含意するより強い帰納的述語を発見する必要があること。安全性検証の実務は、大部分がこの発見作業に還元される。PaxosやRaftの正当性証明の本体も帰納的不変条件の束である。

代表的成果: Floyd–Hoare以来の中心概念。自動発見の系譜としてIC3/PDR（ハードウェアで標準）、IVy（分散プロトコル向け、不変条件発見を人間と対話的に行う設計）。近年はLLMによる不変条件候補生成も研究が活発。

実務実績: 「システムの不変条件を一枚に書き出す」文化は形式手法を名乗らない現場にも浸透している。データベースの制約、会計の貸借一致はその日常的な姿——厳密には、初期成立・全遷移での保存・制約を迂回する更新経路の不在まで確認して、はじめて帰納的不変条件になる。TLA+での検証実務も体感的には不変条件探しが主作業。

刷新での適用: 刷新の全期間を通じて守る不変条件（総残高保存、取引の単調追記、新旧系の対応関係）を最初に明文化する。移行ツール・並走照合・切替手順のすべてがこの不変条件の保存として設計・検査できる。

2.3 遷移系の同値: トレース同値・シミュレーション・双模倣 [理論先行（直接適用）/ 実務厚（概念として）]

概念: 「二つのシステムが同じ振る舞いをする」の精密な定義は一つではなく、スペクトラムをなす（van Glabbeekの線形時間–分岐時間スペクトラム）。粗い順に: トレース同値（観測列の集合が一致）→ シミュレーション（片方の遷移を他方が真似できる）→ 双模倣（互いに真似し合え、各時点の選択構造まで一致）。内部状態の分岐タイミングを区別するかどうかが実務上の分かれ目で、障害・非決定性が絡む挙動まで合わせるなら双模倣側、正常系の入出力だけならトレース同値で足りる。

代表的成果: MilnerのCCSと双模倣、Parkの共帰納的定義。余代数の視点では、状態機械は関手の余代数であり、双模倣は終余代数への写像の一致として統一的に定義される（Mealy機械・ストリーム・無限木が同じ枠に乗る）。

実務実績: プロトコル検証ツール（mCRL2等）はあるが、産業ソフトウェアで双模倣を直接証明する例は稀。ただし概念としての寄与は大きい——「新旧並走の差分ゼロ」が何の同値の経験的近似なのかを言い当てる語彙はこれしかない。

刷新での適用: シャドー実行による差分検証は「有限の実トレース集合上でのトレース同値の検査」であり、(a) 踏んでいない入力、(b) 分岐構造の差（同じ出力に至る内部経路の違い→障害時に露呈）、の二つを原理的に取りこぼす。この取りこぼしの言語化が、差分テストをどこまで信用するかの判断基準になる。また旧系をオラクルとして使う以上、旧系の既知不具合・意図的な仕様変更・許容差分を別台帳で管理しないと、旧系の誤りまで新仕様へ凍結してしまう。

2.4 抽象化写像とデータ精緻化 [実績有]

概念: 具体状態から抽象状態への写像（またはその逆向きの関係）で新旧のデータ表現を結び、「具体側の各操作が、写像を通して抽象側の対応操作と可換」であることを示す（可換図式）。前方シミュレーションで足りない場合（非決定性の解決タイミングが異なる場合）は後方シミュレーションが必要になる、という完全性定理まで整備されている。

刷新での適用: 新旧DBスキーマの対応表は、実はこの抽象化写像の非形式版である。対応表を写像として明示的に書き、移行前後で可換性を機械検査する——移行検証の最も数学に乗せやすい部分。第三層の関手的データマイグレーションはこの発想の圏論的一般化に当たる。

---

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

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