既存システムの実装を「事実上の仕様」とみなし、それを形式化することで 「テストでは踏めないバグ」と「実装が暗黙に決めている仕様」を炙り出すための手順書。 仕様書が無い / あてにならない / 仕様と実装がずれている、という現場を前提にする。
仕様書ではなく 実装が現に何をしているか を仕様の源にする。やることは3段:
- 吸い出し (extract): コードから「実装が主張している仕様」と「暗黙に決めている挙動」を分けて抜く
- 形式化して反例探索 (refute): 主張をモデル化し、それが全入力/全順序で本当に成り立つかを機械に攻撃させる
- 突き合わせ (reconcile): 出た反例を「これは意図か?」とドメイン知識のある人にぶつける → 意図なら仕様として明文化、意図でないならバグ
反例は「バグ報告」であると同時に 認識合わせの会話の起点 になる。ここが一番効く。
| Z3 (SMT) | TLA+ (TLC / モデル検査) | |
|---|---|---|
| 問い | 全入力に対して、ある一瞬 | 時間を通じて、全順序・全 interleaving |
| 得意 | 純粋述語 / 設定・ルールの整合性 | ステートフルなプロトコル / 並行 / 逐次の状態遷移 |
| 例え | 巨大なパズルを一発で解くソルバー | 起こりうる全シナリオを総当たりする探偵 |
| model↔code gap | 狭い (対象がデータなら実データを直接食える) | 広い (命令型を手で抽象する) |
| 置き場所 | 保存時 validator / CI の静的検査 | 設計レビューの成果物・回帰ガード |
判定フロー:
- 「この条件、どんな入力でも成り立つ?」「この設定、配信され得る?」→ 述語が 区間+集合+等式の decidable fragment なら Z3。
- 「どの順番で起きても大丈夫?」「同時に来たら?」「クラッシュ後は?」「いつか必ず〜する?」 → 状態遷移 + 非決定性 → TLA+。
- 状態空間が有限で決定的なら、素の全列挙 (プログラムで直積を回す) が一番安い。 ツールを持ち出す前に「有限か? 決定的か?」を問う。
実装から吸い出すと、経験上この型が繰り返し出る。チェックリストとして使う。
- 矛盾設定 (dead config): 条件の連言が充足不能 = どんな入力でも通らない。 「A のみ ∧ A を除外」「開始 > 終了」「x>20 ∧ x<18」。UNSAT で検出。
- 冗長・内包 (subsumption): 片方の条件が他方を含意し、設定されているのに効いていない。 「上限10回 ∧ 上限1回」→ きつい方が支配。「実効値」を算出して警告。
- 被覆の穴 / dead branch: どの選択肢にもマッチしない入力がある / どの入力でも選ばれない枝がある。
- 変更の差分影響: 設定を編集したとき「誰の判定が変わるか」を反転する入力として記号的に摘出。
- 表現の等価性: 旧形式↔新形式、リファクタ前後が同じ意味かを全入力で証明。
- read-modify-write レース / TOCTOU: 読んで判定して書く、が分離していると、同時実行で 古い値を両者が読み両方通る。上限超過・二重処理。「条件付き書き込み(atomic)なら防げる」を対比で示す。
- 判定と記録の分離: 判定は今すぐ、記録は後で非同期。判定時点で記録がまだ無い→上限をすり抜ける。
- 結果整合 (staleness): 書いた値が読み手に見えるまでの遅延だけで、並行が無くても 上限が破れる。
- 原子性 / torn read: 共有リソース (ファイル・スナップショット) の途中状態を読む。 「別ファイルに書いて rename (atomic)」vs「in-place 上書き」の対比。
- カウンタの不変条件: 重複配信・並行下でカウンタが負にならないか。ガード条件の必要十分性。
- 収束 / runaway (停止性): 引き上げ・リトライ・再試行のループが有界回で止まるか、 外部条件 (期限など) だけが唯一のブレーキになっていないか (= その条件が load-bearing)。
- 伝搬 / 最終整合: commit した変更がいつか必ず反映されるか。crash+再起動で更新が失われないか (edge-trigger は失いうる / level-trigger は追いつく)。
- 冪等性: リトライで二重カウントしないか。ID の生成が「送信毎ランダム」だと重複記録。
- fail-open / fail-close の非一貫: 情報が取れないとき、ある機構は全落ち、別の機構は素通り。 「エラー時にどう振る舞うか」を機構ごとに列挙すると不整合が見える。
- エラーを boolean に畳む × 否定: 「不一致 と エラー を同じ false に畳む」実装で、否定(NOT/inverse)を かけると エラー時にマッチに化ける。壊れた入力ほど通る。最も見落とされやすい。
- 空集合の意味: 空の AND=真(常時マッチの backdoor)、空の OR=偽、要素ゼロ=真、が階層で不整合。
- 信頼境界と詐称: ユーザーが自由に付けられる入力 (クエリ param, ヘッダ) が、検証を経ずに 「信頼された値」として採用される経路。優先順位の高い位置に無検証採用があると詐称可能。
- クロス境界の表現契約: 2つのシステムが同じビット列/enum/レイアウトを共有するとき、 片方が hourly・片方が15分、片方が MSB-first・片方が LSB-first、のような齟齬。展開・変換の全単射性。
- クライアント側だけの検証: UI/フロントだけが弾き、サーバー/API は素通し → API 直叩きで不正状態が作れる。
- 欠けた前提条件: 負のサイズ・空配列で panic。ガードが呼び出し側にしか無い。
実装を読むとき、「宣言された仕様」と「暗黙の挙動」を必ず分けて メモする。
- コメント、特に「なぜ」を語るもの。
// 〜のときは全部OK,// 溢れないかチェックは仕様の宣言。 「元のコードがそうなっていた」「理由は分からない」系のコメントは 化石(fossil) の印 — 仕様か惰性か要確認。 - テスト名・アサーション:
NG if count equal the capのようなテスト名は境界仕様そのもの。期待値の並びも仕様。 - ガード節・panic・error 返し: 前提条件と fail-mode を宣言している。
if n < 0 { ... }の有無。 - enum 定義・定数テーブル・スキーマ制約: 取りうる値と、値↔意味の対応。
- default 値・空/nil の扱い: 未設定が「全許可」か「全拒否」か。empty collection の真偽。
- エラー時の分岐: missing / parse 失敗 / タイムアウトで、true/false/例外 のどれに倒れるか。
- 順序依存と短絡: 適用順で結果が変わるか (副作用があるか)、短絡が結果に効くか理由コードだけか。
- 値が「決定される」場所: フォールスルーの優先順位、複数ソースからどれを採るか、信頼判定の位置。
- クロス境界の変換: シリアライズ / ビットレイアウト / 単位 / タイムゾーン / 曜日始まり。
- 誰が制御できる入力か: infra が付ける値 vs ユーザーが自由に付けられる値 (信頼境界)。
- 空/未設定のとき何が起きる?
- エラー/取得失敗のとき true か false か例外か? (fail-open/close)
- 否定 (NOT/除外/inverse) をかけると、上の答えはどう化ける?
- 境界はどっち向き? (
>か>=か、端点を含むか) - 同時に2つ来たら? 片方の結果がもう片方に間に合うか?
- この値は誰が決める? 信頼できない相手が差し替えられるか?
- このループ/引き上げは何で止まる? 止めているのは本質的な条件か、たまたまか?
- 2つのシステムがこのデータで合意しているか? (レイアウト・enum・単位)
観測可能な入力 → 結果 の 純粋関数 predict(state) を、実装の配管を剥がして書く。
これが「仕様そのもの」の数学的表現になる。配管 (I/O, フレームワーク, DB) はモデルに持ち込まない。
「〜のとき 5xx を返さない」のような否定的ガードと、「こう操作したら こう結果になる」という 振る舞い仕様 を分けて書く。振る舞い仕様は肯定形・決定的・ドメイン語彙で。「箱を閉じる」 (実装の内部語彙を隠し、ドメインの言葉だけで読めるようにする) と、仕様として通用する。
NeverOverCap == served <= cap、NoTornRead == 読んだスナップショットは常に単一版。
証明したい性質に名前を付ける。名前が付くと、レビューでも「この性質は満たす?」と会話できる。
「配信は当初 target を超えない」と invariant で主張し、TLC がそれを破る反例を出す → 「target は総量を縛らない」という実装の含意が可視化される。証明(成立)と反例(不成立)は 同じ道具の裏表。成立を証明したいのか、反例が欲しいのか を意識して invariant を立てる。
全入力は無限でも、判定が変わる 同値類と境界 は有限。それを列挙集合として定義すると、 手書きテストを「モデルからの生成」に一般化できる。境界 (cap-1, cap, cap+1) は必ず入れる。
- 反例が出た → バグ or 仕様の食い違い → issue / 確認質問
- 成立を証明できた → 契約 (regression guard) としてロック → 将来どちらかが変わったら赤くなる 両方が揃うと「何が保証され / 何が穴か」の台帳になる。
- self-check 化: 各モデルに「期待する判定 (VIOLATE / OK) と一致するか」を assert する 実行モードを持たせる。一度きりのデモでなく、CI で回る回帰ガードにする。
- broken-variant テスト: わざと壊した実装 (ガードを外す, 反転を省く) を用意し、 検査がそれを赤で捕まえることを確認する。これをやらないと「常に緑=何も検証してない」に陥る。 検査が load-bearing であることの証明。
- 依存を宣言的に固める: ソルバー・モデル検査器・ランタイムを1ファイルで宣言し (例: nix flake / lockfile)、「ネットワークとローカル環境に依存せず誰でも同じ結果」を担保。 ローカル・CI が同一のハーネスを叩くようにする (実行経路を1つにする)。
- 人間可読な出力 + 機械可読な exit code の両方を出す。デモ用と CI 用を兼ねる。
形式手法は「書いたモデル」を検証するのであって、コードそのものではない。ギャップの扱い:
- 対象がデータ (設定・ルール) なら gap は狭い: モデルが実データを直接読めるので、 「実際の設定を validator に流す変換層」を書けば、証明対象と本番がほぼ一致する。
- 対象が命令型・並行コードなら gap は広い: 手で抽象するので乖離が残る。価値は 「設計の妥当性を実装前/非依存に示す」こと。
- trace-checking でギャップを詰める: 実システムの操作ログ (実際のイベント列) を採取し、 「その観測列がモデルの正当な振る舞いか」を replay で検査する。 「実装は naive/atomic どちらの仕様を refine しているか」を実データで確定できる。 抽象モデルと実挙動を繋ぐ最も強い一手。
全部を形式化しない。限界効用を見て止める。
向くもの: 全入力/全順序で成り立つべき性質、境界・エッジが多い、並行、クロス境界契約、 「設定ミスが事故になる」もの、信頼境界。
向かないもの・やめ時:
- 確率的性質 (期待値・分布) → Z3/TLC 不適合 (整数演算の丸め誤差だけは Z3 可)。
- 制御理論的 (PID の収束など) → ゲイン/誤差の忠実モデル化が重く割に合わない。
- 既に単体テストで brute-force 済み の最適化アルゴリズムの再検証 → spec でなくテストの領分。
- 大物を出し切った後の 確認的なだけの命題 の量産 → CI を重くするだけ。
- 主要な不変条件・危険な穴・クロス境界契約を押さえたら、次は新規形式化より、溜まった 反例・確認質問をドメインと捌く方がレバレッジが高い。
anti-pattern:
- 直列依存を無理に並行モデル化する。
- 実装を読まずに要約・記憶からモデルを組む (変換テーブルを1つ取り違えると偽の証明になる)。
- broken-variant を用意せず「緑だから OK」とする (何も検証していない緑)。
- ネットワーク/手動セットアップに依存した検証 (再現しない)。
対象領域を選ぶ (バグの型カタログ §2 で「ありそう」を当てる)
↓
実装を読む: 宣言された仕様 / 暗黙の挙動 を分けて抽出 (§3 の問いを機械的に投げる)
↓
決定関数 predict と invariant を書く (§4)。証明したいのか反例が欲しいのか決める
↓
Z3 (全入力) or TLA+ (全順序) or 全列挙 で回す (§1)
↓
反例が出た → witness 付きで「これは意図か?」をドメインに問う (§0 突き合わせ)
成立した → 契約 (regression guard) としてロック (§4, §5)
↓
self-check + broken-variant + 宣言的依存で CI に載せる (§5)
↓
model↔code gap が気になるなら trace-checking で実ログと突き合わせる (§6)
↓
限界効用を見て止める (§7)。台帳 (実装の主張 / 検査結果 / 確認質問) を残す
最終成果物は「証明の山」ではなく、「実装の主張 / 機械検査の結果 / ドメインへの確認質問」の 台帳 である。形式手法はバグを出すためだけでなく、仕様と認識を揃えるための共通言語 として使う。