契約による設計
概要
契約による設計 とは、Bertrand Meyer が Eiffel に初めて導入された 設計手法。 ソフトウェアシステム内のあるルーチンは、実行前にはその世界に対して何らかの想定を起き、実行後にはその世界の状態に対してなんらかの確約を行うことができるはず。このような想定や確約を、Meyer は以下のように解説した。
事前条件 (pre condition)
ルーチンを呼び出す側が成立させておかなければならないこと
事後条件 (post condition)
ルーチンが終了した後にルーチンが保証すること
不変条件 (invariant)
ルーチンが保証する、ルーチンの呼び出し前/呼び出し後で、常に真となる条件
呼び出し中には保証されない
事前条件、事後条件は、ある 処理 が呼び出された前後の条件であり、処理の正しさ を判定する。一方、処理対象となるデータには呼び出しの前後という概念はないため、不変条件という１つの条件で データの正しさ を判定する。
ルーチンが 事後条件や不変条件を満たせなかった場合 には、事前に合議された救済策が実施されるべき。これは、具体的には例外のスローやプログラムの終了といった形で実現される。
事前条件が満たされない ままルーチンが呼び出されてしまった場合に、それをどうかするのは誰の責任になるのか？ルーチンの呼び出し側がチェックすべきなのか？ルーチン側がチェックするべきなのか？
言語の一部として実装される場合 には、そのどちらでもなく、呼び出し側がルーチンを起動したタイミングと、ルーチンが実際に処理される、その間に暗黙的にチェックされる。
言語の一部として実装されていない場合 には、表明のチェックを行うプリアンブル/ポストアンブルで、ルーチンを囲んでおく、とか、呼び出し側で例外をスローしたり、プログラムを停止したり、事前条件を満たすように入力値を変換したり、等の対応が必要となる。いずれにせよ、ルーチン側には事前条件が満たされているかどうかをチェックする「責務」は存在せず、それを呼び出す側、もしくは言語自体に事前条件のチェックの責務は存在する。
ただし、事前条件にルーチン側の状態が含まれていた場合、事前条件を満たしているかどうか確認するための API が必要 となる。例えば、Stack クラスにおける pop メソッドの事前条件が「stack の length が 0 以上であること」であったなら、それを確認するための empty メソッドを、ルーチンの実装側が用意しておく必要がある。
21 契約による設計 123p
Andrew Hunt・David Thomas (2016-11-30). 新装版 達人プログラマー 職人から名匠への道 . 384p.
DbC と例外設計
実用
なんか実用的なツールとかの例があればあとでかく (使うかどうかは別)
Java だと iContract みたいなのがあるらしい