TL;DR
ルーチンが満たすべき条件を表明（アサーション）としてコードに書き、ルーチンと呼び出し側の間の「契約」として扱う設計手法。英語では Design by Contract（DbC）と呼ぶ。
なぜ必要か
仕様をコードそのものに書くので、仕様書とコードを別々に保守する必要がなくなる。契約は実行時に検査できるので、違反があればすぐに例外として分かる。
仕組み
Eiffel のドキュメントでは、契約を次の表明で表す。
- 事前条件: ルーチンを実行する前に成り立っていなければならない条件。呼び出し側が守る。違反するとルーチンの本体は実行されず、呼び出し側に事前条件違反が返る
- 事後条件: ルーチンが正しく終わったあとに成り立つべき条件。ルーチン側が守る
- クラス不変条件: そのクラスのインスタンスが常に満たすべき状態。不変条件を参照
例
Eiffel のドキュメントにある set_second は、秒を設定するルーチンである。事前条件で引数が 0 以上 59 以下であることを求め、事後条件で second が受け取った引数と等しくなっていることを確かめる。