"設計の信頼性は、主張ではなく証明によってのみ獲得される。"
ソフトウェアにおける「正しさ」は、しばしば開発者の感覚や慣例に依存している。
しかし、航空宇宙・防衛・医療のような領域では、「なんとなく動く」ことは許されない。
SPARKはこの世界において、“正しい”を証明できる設計を言語構造として提供する。
ここでは、SPARKが実現する「証明責任」とは何か、その背後にある思想を解き明かす。
証明責任：動くコードではなく、正しさを保証するコード
SPARKでは、関数や手続きに対して「この仕様を満たす」ことを宣言的に明記する。
function Compute_Average (X, Y : Integer) return Integer
with
Pre => X >= 0 and Y >= 0,
Post => Compute_Average'Result >= X and Compute_Average'Result <= Y;
このような記述は、単なるコメントや意図ではない。
**証明責任（proof obligation）**として、GNATproveによって数学的に検証される。
人間の責任から、機械の証明義務へ
従来、設計者は「これは正しいはずです」と主張する側だった。
SPARKの世界では、その主張が**「証明されなければ受け入れられない」構造**になっている。
- 設計者は仕様を明記する
- コンパイラが構文を確認する
- GNATproveがその通りかを論理的に証明する
ここにおいて、主張と根拠が一体化する。
エビデンスベースの開発：証明はドキュメントを超える
SPARKでは、コードがそのまま**検証可能な証拠（エビデンス）**となる。
別紙の文書やテスト結果ではなく、構文そのものが設計意図を語る。
この「自己証明可能なコード」は、認証・審査・監査の現場で強力な信頼を生む。
GNATproveによる義務の生成と検証
設計された仕様に対して、GNATproveは以下のような**証明義務（Proof Obligations）**を自動生成する：
- 事前条件が満たされるか
- 事後条件が常に真であるか
- 範囲外アクセスやオーバーフローが発生しないか
これにより、設計の論理的不備がコンパイル段階で発見される。
結語：「主張」ではなく「証明」の上に設計を築く
設計の信頼性とは、個人の技能でも、テストの網羅率でもない。
それは、「正しいと主張する構造」と「それを証明する機構」が一体となったときに初めて成立する。
SPARKは、ソフトウェアを数学的証明の対象とする唯一の舞台である。
"正しさを証明できないコードは、偶然動いているにすぎない。"