テストの限界と形式手法 — 「不在」を証明するもう一つの道

第 1 話 で、 テストという営みの原点として ひとつの警句を置いた。 エドガー・ダイクストラ (Edsger W. Dijkstra) が、 1969 年の NATO ソフトウェア工学会議での議論を経て、 1970 年の論文 「Notes on Structured Programming」 (EWD249) にこう書き残している。

“Program testing can be used to show the presence of bugs, but never to show their absence!” (プログラムテストはバグの存在を示すのには使えるが、 バグの不在を示すことは決してできない)

テストは 有限個の入力・経路を実行した結果でしかない。 無限の入力空間を持つプログラムについて、 「試した範囲でバグが出なかった」 ことは示せても、 「試していない範囲にバグがない」 ことは 原理的に何も保証しない。 これは テストを丁寧にやれば解決する問題ではなく、 テストという方法そのものが持つ 構造的な限界である。

この記事は、 その限界を どう埋めるかという 半世紀にわたる回答 —— 形式手法 (Formal Methods) を辿る。 数学的に厳密な記法でシステムを記述し、 そのシステムが仕様を満たすことを 数学的に証明・検証するアプローチの総称である。

テストが届かない領域

形式手法は 「テストの上位互換」 ではない。 両者は 得意な領域が異なる。

	テスト	形式手法
対象	実際に動くコード	仕様 (モデル) またはコード自体
保証の性質	サンプリング的	網羅的
欠陥不在の証明	できない	条件付きで可能
コスト	相対的に低〜中	相対的に高い
得意領域	統合部分・実環境依存・UI	並行性・プロトコル・分散整合性

形式手法が特に力を発揮するのは、 テストでは検出しにくい 並行性のバグ・分散システムの整合性・プロトコルの安全性 (safety) と生存性 (liveness) といった性質である。 実務では、 核となるアルゴリズムやプロトコルにのみ形式手法を適用し、 周辺は従来のテストで担保するという 「使い分け」 が一般的になっている。

モデル検査 — すべての状態を機械的に洗いつくす

モデル検査 (Model Checking) は、 システムの振る舞いを有限状態機械としてモデル化し、 そのモデルが取りうる すべての状態 を網羅的に探索して、 指定した性質が常に成り立つかを 自動的に検証する手法である。

理論的基盤は 1980 年代初頭、 エドムンド・クラーク (Edmund Clarke) と アレン・エマーソン (E. Allen Emerson)、 そして独立に ジョセフ・シファキス (Joseph Sifakis) によって確立された。 3 人は この功績により 2007 年に ACM チューリング賞を受賞している。

最大の課題は 状態爆発問題 (State Explosion Problem) —— 並行プロセス数やデータの取りうる値が増えるほど、 状態空間が指数的に増大する。 これに対処するため、 ケン・マクミラン (Ken McMillan) らによる 二分決定図 (BDD) を用いた記号的モデル検査や、 有界モデル検査といった技術が発展した。

SPIN と TLA+ — 並行性を検証する 2 つの代表格

SPIN は、 ベル研究所の ゲラード・ホルツマン (Gerard Holzmann) が開発したモデル検査ツールで、 並行システムの検証に特化している。 仕様記述言語 Promela (Process Meta Language) を用い、 通信プロトコルやマルチスレッドプログラムの 安全性・デッドロックの有無を検証する。

TLA+ (Temporal Logic of Actions) は、 分散システム研究の第一人者で Paxos アルゴリズム の考案者としても知られる レスリー・ランポート (Leslie Lamport、 2013 年 ACM チューリング賞受賞) が開発した 形式仕様記述言語である。 集合論と時相論理に基づき、 システムの状態遷移を数学的に記述する。 付随するモデル検査器 TLC を使えば、 有限の範囲でモデルを網羅的に検証できる。 プログラマに親しみやすい擬似コード風の記法 PlusCal も用意されており、 これは TLA+ へと変換される。 ランポートは著書 『Specifying Systems』 (2002 年) で TLA+ を体系的に解説している。

このほか、 MIT の Daniel Jackson が開発した Alloy は、 一階述語論理に基づく関係論理でデータモデルや構造的制約を記述する軽量な言語で、 付属の Alloy Analyzer が指定範囲内のすべてのインスタンスを探索し反例を見つけ出す。 ハードウェアや有限状態プロトコルの検証に使われる NuSMV、 C/C++ を直接対象に SAT/SMT ソルバーで検証する CBMC など、 抽象度の異なるレイヤーをカバーするツール群が 用途に応じて使い分けられている。

AWS の実践 — 実装前にバグを潰す

形式手法が学術的関心にとどまらず 産業実務で成果を上げた事例として、 Amazon の AWS チームによる TLA+ 活用 が広く知られている。 クリス・ニューカム (Chris Newcombe) らによる論文 「How Amazon Web Services Uses Formal Methods」 (Communications of the ACM、 2015 年) は、 DynamoDB・S3・EBS など複数の中核サービスの設計に TLA+ を適用し、 テストや設計レビューだけでは発見が極めて困難だった 微妙な並行性バグ (レアなタイミングでのみ発生するデータ不整合など) を、 実装前の設計段階で複数発見できたと報告している。 「大規模分散システムの正しさは、 実装後のテストだけでは担保しきれない」 ことを示す実例として、 今も頻繁に引用される。

定理証明 — 証明そのものをプログラムとして書く

モデル検査が有限の状態空間を自動的に網羅探索するのに対し、 定理証明 (Theorem Proving) はより表現力の高い論理体系 (高階論理・型理論など) を用いて、 多くの場合人間が補助しながら 数学的な証明を構築するアプローチである。 無限の状態を持つシステムの正しさも、 有限の証明手順によって示せる。

代表的な 証明支援系 (Proof Assistant):

ツール	開発元・関係者	理論的基盤
Coq	INRIA (フランス)、 Thierry Coquand らが基礎理論を考案	帰納的構成の計算
Isabelle/HOL	ケンブリッジ大学の Larry Paulson、 ミュンヘン工科大学の Tobias Nipkow ら	高階論理
Lean	Leonardo de Moura (Microsoft Research で開発開始、 後に AWS 等が支援)	依存型理論

これらのツールは カリー・ハワード対応 (「命題は型であり、 証明はプログラムである」 という対応関係) に基づき、 証明を書くことがプログラムを書くことと 数学的に等価になる点が特徴である。

CompCert と seL4 — 「バグがゼロ」であることの証明

著名な応用例として、 CompCert (Xavier Leroy らによる Coq で形式検証された C コンパイラ) と、 seL4 (NICTA、 後の CSIRO・Data61 が 2009 年に発表した、 機能的正しさを完全に形式検証したマイクロカーネル。 Isabelle/HOL を使用) が挙げられる。 これらは 「コンパイラや OS カーネルの中核部分にバグが一切ない」 ことを数学的に証明した数少ない実例であり、 通常のテストでは到達不可能な保証水準を示している。

契約による設計 — Eiffel というもう一つの道

契約による設計 (Design by Contract, DbC) は、 バートランド・メイヤー (Bertrand Meyer) が 1986 年に開発した言語 Eiffel で導入した設計手法で、 形式手法とテストの中間に位置する 「軽量形式手法」 の代表例である。

• 事前条件 (precondition) —— 呼び出し側が保証すべき条件
• 事後条件 (postcondition) —— 実装側が実行後に保証する条件
• 不変条件 (invariant) —— オブジェクトのライフサイクルを通じて常に成り立つべき条件

これらを 表明 (assertion) としてコードに明示し、 実行時にチェックすることで、 契約違反を即座に検出できる。 Eiffel 以外にも、 Java (旧 JML)、 Python (assert 文や icontract ライブラリ)、 Racket (contract 機構)、 Ada/SPARK など多くの言語に 同様の考え方が取り入れられている。

安全重要システムという最前線

形式手法が最も早くから 制度的に要求されてきた領域が、 人命に直結する 安全重要システム (safety-critical system) である。

パリメトロ 14 号線 (Météor) は、 ジャン・レイモン・アブリアル (Jean-Raymond Abrial) が考案した形式仕様記法 B-Method を用いて、 無人運転の自動列車制御システムが開発・検証された事例として知られる。 1998 年に開業したこの路線は、 形式手法が実際の商用大規模システムで実用化された代表例として 頻繁に引用される。

SPARK (Ada 言語のサブセットに事前条件・事後条件・データフロー契約を付加した言語) は、 静的解析によってランタイムエラー (配列範囲外・オーバーフローなど) の不在を数学的に証明でき、 航空・防衛分野で広く使われている。 民間航空機ソフトウェアの認証基準 DO-178C は、 開発と検証の厳格なプロセスを要求するが、 近年の版では モデルベース開発や SPARK のような形式的解析手法の活用も 認証エビデンスとして認められるようになっている。

軽量形式手法という第三の道

Daniel Jackson は、 Alloy のような 「完全な証明までは目指さないが、 有限範囲を網羅的にチェックすることでバグの多くを発見できる」 アプローチを 軽量形式手法 (Lightweight Formal Methods) と呼んだ。 Coq や Isabelle のような 「完全な証明 (heavyweight)」 との対比で、 導入コストと効果のバランスを取るための重要な区分である。

プロパティベーステスト も、 この軽量形式手法の系譜に位置づけられる。 仕様 (プロパティ) を形式的に記述する点は形式手法と共通するが、 網羅的探索ではなく ランダムサンプリングによって検証する点で モデル検査とは異なる。

型システムという身近な形式手法

静的型システムも、 広い意味では 「軽量形式手法」 の一種と見なせる。 型検査は コンパイル時にプログラム全体を対象に、 ある種の不整合 (型不一致) が存在しないことを 機械的に保証する。 これは テストが持つ 「サンプリング的」 な性質とは対照的である。

ただし型システムが検証できるのは 「型が合っているか」 という限られた性質にとどまり、 ビジネスロジックの正しさや並行性の安全性までは通常カバーしない。 依存型 (Dependent Types) を持つ言語 (Idris・Agda・Lean など) では、 型そのものに任意の論理命題を埋め込めるため、 型検査がより強力な証明の役割を果たすこともある。

型システムが軽量形式手法として 広く実務に浸透した近年の例が、 Rust の所有権システム (ownership) とボローチェッカー (borrow checker) である。 コンパイル時の静的検査によって、 メモリ安全性 (解放済みメモリへのアクセスや二重解放など) と データ競合 (data race) の不在を保証する仕組みであり、 形式手法的な発想が 主流言語のコンパイラに組み込まれた事例として位置づけられる。

テストと形式手法、 対立ではなく相補

多くの現場では、 まずモデル検査で設計レベルの誤りを安価に洗い出し、 特に保証水準の高い中核コンポーネントにのみ 定理証明を適用するという 段階的なアプローチが取られる。 SPIN や TLA+ は並行システムやプロトコルの安全性検証に、 Coq・Isabelle・Lean は コンパイラや OS カーネルなど 極めて高い保証が要求される領域に、 それぞれ強みを持つ。

第 1 話のダイクストラの警句は、 テストという営みを否定するものではない。 「テストで届く範囲」 と 「数学でしか届かない範囲」 の境界線を引いただけである。 その境界線の向こう側を、 モデル検査と定理証明が半世紀かけて埋めてきた —— それが この記事の結論である。

次記事では、 視点を 「どう検証するか」 から 「品質は誰の仕事か」 へと移す。 専任テスターから全員品質へ —— 正しさの証明を超えて、 性能・セキュリティを含む品質を 組織全体でどう担うようになったかを辿る。