"仕様とは希望ではなく、契約であり証明である。"
プログラムにおける正しさとは何か。
「例外が起きない」ことではない。「なんとなく動いている」ことでもない。
あらゆる入力に対して、定められた動作が保証されること——それが形式手法の定義する「正しさ」だ。
Ada、とりわけSPARKにおいて、その中核を成すのがPre/Post条件である。
Safe_Divide：小さな関数に宿る設計の緊張感
function Safe_Divide (X, Y : Integer) return Integer
with
Pre => Y /= 0,
Post => Safe_Divide'Result * Y = X;
一見シンプルなこの関数に、Adaは2つの「契約」を与える。
- Pre（事前条件）：除数が0であってはならない
- Post（事後条件）：返却値に除数を掛ければ元の被除数になる
これにより、この関数は自分が何を受け取り、何を返すべきかを、構文的に保証する。
Pre/Postで変わる設計思考
通常の言語では、以下のように書くことが多い：
function Divide (X, Y : Integer) return Integer is
begin
if Y = 0 then
raise Constraint_Error;
end if;
return X / Y;
end Divide;
これは「間違った呼び出し」に備えた実行時防御だが、
SPARKでは「そもそもそのように呼び出されること自体が設計違反」として捉える。
契約を持つコードは検証可能である
GNATproveなどの検証ツールは、Safe_Divide を使う箇所が
必ず Y /= 0 を満たしているかを静的に解析する。
それにより、「例外が起きないこと」ではなく、仕様が破綻しないことを保証する。
形式手法とは、「全体性」への設計
契約が1つあるとき、それを破る呼び出しは明確な契約違反となる。
テストに頼らず、言語レベルで設計者の意図を“義務化”するこの仕組みこそ、形式手法の本質である。
結語：正しさを語るとは、仕様を記述すること
仕様がなければ正しさは主張できない。
設計意図をPre/Postという形式化された記述で埋め込むことで、
コードは「動く」から「保証された構造」