http://itpro.nikkeibp.co.jp/article/COLUMN/20120719/410078/
仕様記述言語のVDMを使うことで、仕様外の動作をするバグは防げる、
という理解で良いのかしら。
問題は仕様に問題がある場合だけど、仕様外の動作が防げれば、
仕様の問題も洗い出しやすいし、仕様を直した後の実装への反映も楽か？
Wikipedia - VDM
この辺の記事が参考になるかな。
誰でも使える形式手法：ライトウェイトな形式手法で高品質な仕様をこの手に！
http://monoist.atmarkit.co.jp/mn/articles/0809/17/news125.html
同じ用な考え方の言語として Coq なんかも面白い。
プログラミング Coq 〜絶対にバグのないプログラムの書き方〜
http://www.iij-ii.co.jp/lab/techdoc/coqt/
LL魂(Lightweight Language Spirit)のときの今井さんのプレゼン
http://ll.jus.or.jp/2007/show/Event/Session/#H-dh4f51
こういうメタプログラミング的なものは、使いこなれば、
便利そうなんだけど、理解するハードルは高い気はする。
高校や大学で使う数学記号はとても便利なんだけど、
理解しないと使いこなせない、というのに似てる気がする。