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