Bメソッドには感動した。矛盾検出をしてくれるのは嬉しい。だけど、矛盾なく間違えたらどうなるの？→試験したい vdmは面白い。表現力も高いし、日本語も使えるし。でも、試験の数はこれまでと変わらないから、試験コードを作る手間が倍じゃね？→定理証明した…

今、すごく個人的にjavaで仕様を書けないか模索してます。目標はいろいろある。 動作する（テストできる）仕様 定理証明（仕様の矛盾検出とか）に使える仕様 開発環境のサポート（コード補完とか）を受けられる仕様 抽象化して書ける仕様 行数の少ない仕様 …