Eiffel "Design by Contract" - 『契約による設計』

[id:lethevert:20050715:p1]にいただいたid:emeitchさんのコメントを見て、Eiffelというプログラミング言語を調べてみました。でも、あまり情報がないようです。"Design by Contract"についても、Eiffelでどのように実装されているかよりも、Javaでどのように取り込むかという話がちらほらとあるだけで、いまいちよく分からないです。
で、少ない情報から、ちょっと強引に要約してみます。間違っていたら、突っ込んでください（→詳しい人）。

事前条件、事後条件、不変表明という３つに類型化して、条件を表明する。

表明した条件に従って、assertを自動生成して、自動的にブラックボックステストケースを作成して、単体テストにより条件を保証する

"Design by Contract"に対応していない言語で、その概念を取り込もうとすると、２つ目のテストの部分は人力で行う必要がある。
で、これは、僕の考えていたものとは、一部同じですが、一部違いますね。つまり、１点目の条件の類型化は、僕のイメージとほぼ同じでしたが、それを保証する方法がassertとテストを利用するということが全く違います。
Haskellなどの関数型言語は、型推論ができるので、その技術を発展させることで、テストではなく、推論によって保証できるのではないかと思います。あと、Javaの例外のように関数のプロトタイプに条件の宣言をつけることで、推論の範囲を、関数の内側に限定できるのではないかと思います。
でも、"Design by Contract"の実装が、こういう方向に進んでいるということは、おそらく、僕のイメージしているものは、実在しないんだろうな。