"設計とは、未来の自分との契約である。"
関数は入力を受け取り、出力を返す。
しかしその「期待される動作」が、設計者の頭の中にしか存在しないとしたら、コードはいつか裏切る。
Adaは、設計意図を明示し、構文の中に取り込む。
それが Contract-Based Programming（契約によるプログラミング） である。
契約とはなにか
契約とは、「この関数は、○○が成り立つ前提で呼ばれ、△△を必ず満たして終わる」という、明示された前提と保証のこと。
function Divide (A, B : Integer) return Integer
with
Pre => B /= 0,
Post => Divide'Result * B = A;
この構文が意味するのは：
- Bが0でないことを前提とする
- 返却値は、AをBで割った結果であることを保証する
これが曖昧な言語設計との決定的な差である。
Pre/Post条件の意義
- Pre（事前条件）：呼び出す側の責務
- Post（事後条件）：実装する側の責務
この分離によって、「契約の破綻」がどこにあるのかを明確にできる。
呼び出し側が契約違反をすれば、それは「仕様を守らなかった側の責任」になる。
契約とSPARK：証明可能性への拡張
SPARKでは、これらの契約を数学的に証明可能な仕様として定義できる。
function Abs (X : Integer) return Integer
with
Post => Abs'Result >= 0;
このPost条件は、Abs の結果が必ず非負であることを証明可能な約束として構文化している。
契約は「コメント」ではない
多くのプロジェクトでは、設計書にしか存在しない制約が、
数か月後には開発者の記憶から消え、コードは仕様に反する形で改修される。
Adaの契約構文は、設計意図を「構文」に変えることで、設計の寿命を延ばす。
結語：信頼は、契約の上にしか成り立たない
契約なき関数は、使用者を裏切る可能性を常に持っている。
信頼性の高いシステムを作るということは、契約を明示し、それを破れないように縛る設計をすることだ。
Adaはそのための言語である。
"仕様がコードに宿るとき、バグは構文エラーになる。"