　VDM-SLは、VDMの基礎となった仕様記述言語であり、ISO標準にもなっています。VDM++は、VDM-SLを基にオブジェクト指向拡張を行った言語であり、現在VDMの中で主に使われている言語です。VICEは、2007年にリリースした言語であり、VDM++の構文定義に加え、リアルタイム性と並行性のモデリングを可能にし、非同期イベントをシミュレーションするようなモデルを構築できます。

VDMの特長

　VDMの特長の1つは“仕様をテストできる”という点です。VDMは検証の手法に「仕様アニメーション」という手法を用います。仕様アニメーションとは、仕様の実行を通して検証を行う手法であり、その考え方はプログラムの「動的テスト」と似ているため、現場の技術者も理解しやすい手法といえます。

　仕様アニメーションは、仕様における状態遷移や条件分岐のすべてを網羅的に実行することが困難であるため、ほかの形式手法が持つ証明やモデル検査に比べ、検証の完全さという面では劣っています。しかし、シナリオとしての“テストケース”とその“検証結果”を示すことで、VDMを知らなくても仕様の妥当性を確認できるといったメリットがあります。

　前述のとおり、VDMは検証に仕様アニメーション（簡単にいうと仕様をテストする手法）を用いますが、形式手法の中には、検証の手法として数学的証明を用いるものがあります。数学的証明の検証力は大変強力で、すべての仕様が証明可能であれば、仕様に関しては完全であるといえます。数学的証明を用いる手法では、おおよそツールの機能を用いて証明すべき課題を抽出します。この証明すべき課題をツールによって自動的に証明できるケースもありますし、自動では証明できないケースもあります。自動で証明できる場合はツールに任せることができますので労力は掛かりませんが、手動で証明しなければならない場合は大変多くの労力を要します。

　一方、モデル検査は検証したい対象を正しくモデリングすることと、検証したい性質を抽出することが難しく、多くの労力を要します。VDMはテストによる検証を行うため、証明やモデル検査の検査性質抽出に比べて労力が少なくて済み、かつシナリオをベースとした正当性検証を行うため、費用対効果のバランスに優れます。

　VDMの構文の特長は、「不変条件」「事前条件」「事後条件」といった制約条件を明示的に記述できる点にあります。不変条件はクラスや変数、型に対してシステムが存在する限り必ず成立すべき条件です。事前・事後条件は、関数に対して関数を実行する前の状態と実行後の状態で成立すべき条件です。なお、この不変条件、事前条件、事後条件はVDM固有の考え方ではなく、例えばBメソッドにも不変条件、事前条件が存在します。

　また、VDMをはじめとする形式手法には「陰仕様」と「陽仕様」という記述方法があります。VDMにおける陰仕様は関数のシグネチャ（入出力、制約条件）のみを記述し、関数の本体部分は「is not yet specified」という予約語を用いて、“まだ定義しない”という宣言を記述します。これはいい換えると「要求（Requirement）」を表現しているといえ、その機能が「どうなっているべきか？」を端的に記述できます。

　陰仕様では、「VDMTools（VDMを用いた開発を支援するツール）」を用いた動的テストは実施できず、静的チェックのみ可能となります（注）。要件定義の初期段階において、システムが有する機能の一覧とその入出力・制約条件を明らかにするときに使用します。

※注：VDMToolsについては、次ページで解説しています。

　一方の陽仕様は、陰仕様で「is not yet specified」とした部分にアルゴリズムを記述し、VDMToolsによるテストができるように記述した仕様です。これはいい換えると「仕様（Specification）」を表現しているといえ、その機能を「どのように」実現するのかを記述します。この辺りの開発プロセスにおいて、「どこでどうVDMを使うか？」といった話は次回詳しく解説したいと思います。

　次ページで、VDMToolsとVDMによる仕様の記述例を紹介します。