>>403
どうゆう意味で実行可能なの？
他のプログラムの外付けアサート的な動作しかできないのかと思いこんでいたが。
VDM単体で動くの？

>>404
俺をおだてても木には登れんぞ。
集合論プログラムのコンパイラを作るなんて俺の実力じゃとても出来そうもない。
ユーザーとしてなら使ってみたいが。

>>405
仕様を詳細にするのはやり方がまずいと柔軟性のないプログラムになると思う。
抽象度の高いプログラムで仕様を満たせるならそっちの方がいいと思う。