暑い日の読書〜形式手法の技術講座

形式手法（モデル検査）の勉強用として購入。SPINやLTSAについては基礎知識を持っていたけれど、VDM++については全く初めてなので紹介されている例を興味深く読んだ。識別子に日本語が使えるのでソースコードに少々違和感を感じたりするが、「そもそもVDMを使ってどのような検証が可能になるのか？」という考え方が実例と共に示されるので有り難い。特に「形式手法の細かな理屈はともかく、ソフトウェア工学の一つとして導入したい」と考えているエンジニアには役立つ本だろう。参考になったのは下記の点。

• 主な形式手法と各言語の位置付けが説明されている。例えば、SPINは適用範囲が限定されるが完全な検証が可能であり、VDMは適用範囲が広く検証は簡易なものになる。
• 形式手法の導入例が説明されている。どのような進め方なら上手く導入出来るか、フェリカネットワークスでの実例などと合わせて説明が載っている。

適用範囲は限定されるのだろうが「C++コードの90%はVDM++から生成」（オランダ・チェス社の例）とはすごいね。一体どんなシステムなのだろう？

なお、下記の記述は名言。昔ながらのソフトウェア開発しか知らず、現在のソフトウェア開発技術を知らない上司から同じ質問を受けた事がある。今度、この文句をぶつけてみよう。

「仕様を書いたら、プログラムを自動生成するようなツールは無いですか？」という質問も良く受けるが、こういう質問をすること自体、現在のソフトウェア開発技術に対する無知を公言しているようなものである。そのような技術は現在存在しないし、今後可能になる目処も全く立っていない。

形式手法の技術講座―ソフトウェアトラブルを予防する