"最も信頼できるバグは、実行される前に死ぬバグである。"
バグの多くは、**「書いた本人でさえ、気づいていない意図のズレ」**から生まれる。
これをテストで拾おうとする発想は、常に後手である。
Adaはその設計思想の中で、「静的解析」＝コンパイル時点での検証による保証を前提としている。
とくにSPARK Adaでは、GNATproveというツールを用いて、コードを数学的に証明可能な構造物へと昇華させる。
静的解析の本質：実行前に設計を証明する
静的解析は、以下の問いに答える：
- このコードは、定義された契約に違反していないか？
- この関数は、呼び出されたとき常に正しい状態にあるか？
- この変数は、未初期化状態で使われていないか？
これらを実行せずに検証する。
GNATprove：証明ツールではなく設計の鏡
SPARKの静的解析ツールである GNATprove は、以下の情報を用いてコードを解析する：
- Pre/Post条件
- 型制約と範囲情報
- アクセス可能なメモリ情報（Global/Depends）
- Loop不変式（loop invariant）
procedure Increment (X : in out Integer)
with
Pre => X < Integer'Last,
Post => X = X'Old + 1;
この定義により、GNATproveは「Xが上限を超えることはない」と数学的に保証する。
コンパイルの先にある「保証」の設計
コンパイルが通ること＝安全、ではない。
Adaの世界では、「構文が正しいこと」と「意図が正しいこと」は分けて考える。
静的解析は、構文上の正当性を超えて、設計意図が保証されているかどうかをチェックする。
設計段階で証明される世界
SPARKでは、コードが完成した瞬間にその正しさを機械的に証明できる。
これは「自動検査」ではなく、設計と仕様が数学的に整合していることの保証である。
結語：保証なき実行は、希望にすぎない
テストでは足りない。レビューも限界がある。
真に信頼されるソフトウェアは、論理的に破綻のない構造でのみ成立する。
静的解析とは、**開発者の主観を越えた“第三の目”**であり、Adaはそのための言語である。
"検証されない設計は、設計ではなく賭けである。"