昨日は某所で行われた形式仕様記述言語VDM++の基礎を学ぶセミナーに参加してきた。講師は「VDM++によるオブジェクト指向システムの高品質設計と検証」の翻訳者としても著名な酒匂寛氏。VDM++の書籍に目を通して、そのサンプルを動かす程度の経験しか無かった…

形式手法（モデル検査）の勉強用として購入。SPINやLTSAについては基礎知識を持っていたけれど、VDM++については全く初めてなので紹介されている例を興味深く読んだ。識別子に日本語が使えるのでソースコードに少々違和感を感じたりするが、「そもそもVDMを…