契約によるプログラミングとQuickCheckは相性がいいんじゃないだろうか

EffeleとD言語ぐらいしかサポートしている言語は知らないけれど、契約によるプログラミングというのがある。(噂によるとassertさえあれば、契約によるプログラミングだ、と言いはってもいいらしいけど。)
これを使うと、関数に入るときに満しているべき事前条件と、返り値が満しているべき事後条件が書ける。

double sqrt(double x)
in{
  assert(x >= 0);
}
out{
  assert(result*reuslt - 0.1 < x && x < result*result + 0.1);
}
body{
  ...
}

で、それとは別にHaskellのライブラリでQuickCheckというのがある。これは、条件を満すデータを生成して、自動でテストしてくれる。(参考:QuickCheckを試す - みずぴー日記)。

sqrtCheck x = 
    x >= 0 ==>
      let s = sqrt x in
      s**2 - 0.1 < x  && x < s**2 + 0.1

この2つは、結構相性がいいんじゃないだろうか。QuickCheckのテストデータに課す条件と事前条件が、テスト本体が事後条件に対応している気がする。
事前条件と事後条件をちゃんと書けば、あとは自動でテストしてくれる枠組みがあったら、嬉しいかもしれない。