契約とはなにか

契約とは、「この関数は、○○が成り立つ前提で呼ばれ、△△を必ず満たして終わる」という、明示された前提と保証のこと。

function Divide (A, B : Integer) return Integer
  with
    Pre  => B /= 0,
    Post => Divide'Result * B = A;

この構文が意味するのは：

これが曖昧な言語設計との決定的な差である。

Pre/Post条件の意義

この分離によって、「契約の破綻」がどこにあるのかを明確にできる。

呼び出し側が契約違反をすれば、それは「仕様を守らなかった側の責任」になる。

SPARKでは、これらの契約を数学的に証明可能な仕様として定義できる。

function Abs (X : Integer) return Integer
  with
    Post => Abs'Result >= 0;

このPost条件は、Abs の結果が必ず非負であることを証明可能な約束として構文化している。

多くのプロジェクトでは、設計書にしか存在しない制約が、
数か月後には開発者の記憶から消え、コードは仕様に反する形で改修される。

Adaの契約構文は、設計意図を「構文」に変えることで、設計の寿命を延ばす。

契約なき関数は、使用者を裏切る可能性を常に持っている。
信頼性の高いシステムを作るということは、契約を明示し、それを破れないように縛る設計をすることだ。

Adaはそのための言語である。

"仕様がコードに宿るとき、バグは構文エラーになる。"