javaで仕様の目的

Bメソッドには感動した。矛盾検出をしてくれるのは嬉しい。だけど、矛盾なく間違えたらどうなるの？→試験したい
vdmは面白い。表現力も高いし、日本語も使えるし。でも、試験の数はこれまでと変わらないから、試験コードを作る手間が倍じゃね？→定理証明したい。
jmlは便利。プログラムの問題を見つけくれるし、試験サポートもしてくれる。だけど、仕様をキチンと書こうとすると、プログラムと同じ量の記述が必要なのはどうよ？→もっと抽象的に書かせろ。
結果、ワガママな俺が満足するには、抽象的に書けて、動作して、しかも定理証明が出来る仕様記述方法が必要と分かった。