形式仕様記述VDM++を学ぶセミナーに参加してきた

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

VDM++の細かい文法は書籍を読めば分かるものの、実際のところは落とし穴が色々あるし、些細な疑問で行き詰まったりすることが珍しくない。今回のセミナーではそのような疑問にも講師の酒匂氏が丁寧に答えてくれたので、参加した甲斐が有った。本を読んだだけでは分からない「実際のところはこう使ったほうが便利」といった細かなノウハウを学べるのはセミナー参加のメリットだと思う。

今回のセミナーの対象範囲は、仕様記述言語としてVDM++の基礎を学び、VDMToolsを用いたモデルの評価を行うところまでだった。VDM++を利用した本格的な仕様記述はまた次回行う予定と言うことなのでこちらも期待しておきたい。以下、講義のメモより個人的に参考になったポイントを抜粋してみた。

• functionsはインスタンス変数にアクセスできないが、operationsはインスタンス変数にアクセス可能（オブジェクトの状態を変更出来る）。但し、実際にはoperationsを使うとオブジェクトに影響（副作用）を及ぼして検証が面倒になるので、出来るだけfunctionsを使う方が良いだろう。
• 集合演算に慣れるまでは大変だが、自分でループを回して処理するよりは簡便な記述となり便利。SQLのような処理を思い浮かべるとイメージしやすいだろう。
• 直ぐに状態数が爆発してしまい検証範囲が限られるSPINに比べると、VDM++の場合は仕様全体を包括的に取り扱えるのが特徴。大規模な仕様でも記載して検証可能。
• 開発導入にはプロセスを含めた改善が必要。単に「VDM++で仕様書を書きましょう」と言うだけでは、普通の（自然文を書き連ねる）仕様書と何も変わらなくなってしまう。
• VDM++の考え方（事前条件、事後条件、不変条件等）を意識して取り組むだけでも、既存の開発現場では役立つことが多いかも知れない。

VDM++全般については下記の書籍が詳しいのでお勧めだ。

VDM++によるオブジェクト指向システムの高品質設計と検証 (IT architects’ archive)

VDMを使うからと言って開発現場の問題が解決するとは思えないけど、一つの方法論として知っておいて損はしないと思っている。

形式手法(Formal Methods)とは1970年代から始められたソフトウエア開発手法の1つです。 形式手法は、従来まで自然言語を用いて記述していた仕様を、形式仕様記述言語を用いて 言語のルールに則った厳密な記述をすることによって、上流工程からソフトウエアの品質を高めていきます。

vdmtools.jp -&nbspvdm リソースおよび情報

---

関連

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