日経ソフトウェア2007年1月号

形式手法とは関係ないかもしれませんが、事前条件、事後条件、不変条件を
記述できる言語、Eiffelの記事が載ってました。
http://software.nikkeibp.co.jp/software/backno/2007/0701indexc.html
特集１：フリー言語で真のプログラミングを学ぶ
Part4　Eiffelに学ぶ「正しいオブジェクト指向」
Eiffelの記事なんて珍しいなぁ〜、と思ったら、VDMにかかわっている人でした。どひゃー＼（＾ｏ＾）／