"実装と仕様が同じファイルに宿るとき、ソフトウェアは語り始める。"
従来のソフトウェア開発では、「仕様書」と「ソースコード」は別物だった。
仕様は人間が読み、コードは機械が処理するものとして、両者はしばしば乖離してきた。
SPARK Ada はそれを統合する。
仕様が構文となり、実装と共に同じファイルに記述されるこの設計思想は、
開発におけるドキュメントと保証の構造を根底から変える。
コードに宿る形式仕様：Pre/Postの再定義
SPARKでは、関数や手続きに 契約（Pre/Post） を付与することで、
仕様を明示的に文法化できる。
procedure Transfer (From, To : in out Account; Amount : Positive)
with
Pre => From.Balance >= Amount,
Post => From.Balance = From'Old.Balance - Amount and
To.Balance = To'Old.Balance + Amount;
これにより、設計意図・制約・責務がすべて1つの構文ブロックにまとまり、
実装が仕様から逸脱する余地がなくなる。
一貫性と自動検証：仕様は嘘をつかない
- 仕様が記述されていないコードは、設計意図が読み取れない
- コメントは信頼できない
- テストは限定的な証拠にすぎない
SPARKの形式仕様は、これらを乗り越える。
仕様＝形式的条件として定義され、それが自動検証ツールで証明対象になる。
設計変更と“正しさの継承”
仕様がコードに含まれていることで、変更時の検証も可能になる。
function Abs (X : Integer) return Integer
with
Post => Abs'Result >= 0;
このようなPost条件を持つ関数を改修しても、
GNATproveがその正しさを証明し直す。
これにより、「変更＝不安定化」という常識を構造的に排除できる。
実装と仕様の分離は、もはや古い
かつては、仕様を別紙で書くことが「丁寧な開発」だった。
だが、仕様と実装の同期は崩れやすく、
「いつのまにかコードが仕様と乖離する」ことは珍しくない。
SPARKは、その乖離を構文的に禁止する世界を提案する。
結語：コードが語る仕様、仕様が動かすコード
ソフトウェアが巨大化し、人の記憶や理解を超える今、
正しさは設計者の脳内にあるべきではない。
コードそのものが語る世界へ。
SPARKは、**「正しいソフトウェアは、書かれた時点で証明されるべきだ」**という思想を体現する。
"仕様がコードに寄り添うとき、バグは設計段階で死ぬ。"