「VDM-SL」の歴史的背景

VDM（Vienna Development Method）は1960年代から1970年代にかけてIBMのウィーン研究所で開発された。VDMの仕様記述言語がVDM-SL（Specification Language）である。VDMには海外で原子力発電、日本ではフェリカネットワークスでのICカードへの適用事例などがある。またVDM-SLは、1996年にISOで標準化されている。

VDM-SLとともに解説される仕様記述言語に、「VDM++」がある。VDM++はVDM-SLにオブジェクト指向概念を追加して拡張された仕様記述言語だ。

「VDM-SL」の記述の特徴

VDM-SLの仕様記述言語としての特徴の1つは、ASCII表現でも論理的な数学記号を記述できる点だろう。「∀」や「∃」などをforallやexistsなどで表記する（注1）。

VDM-SLでは、データ型、状態、値、関数、操作を定義することができる。型定義では、その型の変数が満たす不変式を記述する。状態定義では、状態に関する不変式と初期化条件を記述する。関数定義と操作定義では事前条件と事後条件を記述する。

九州大学の荒木 啓二郎先生と南山大学の張 漢明先生の教科書「プログラム仕様記述論」（オーム社、2002）には、VDM−SLの記述例が豊富に載っているので、詳しく知りたい方は参考にするとよいだろう。

形式的仕様記述言語の分類

• 状態モデル「VDM-SL」「Z言語」「B」
• 代数的仕様「LOTOS」「OBJ」

Z言語の特徴

• スキーマ表記

VDM-SLの特徴

• 論理的な数学記号を記述可能

最後に、その他の仕様記述言語「LOTOS」と「SpecC」について解説しよう。これらは適用分野が明確なドメイン指向の仕様記述言語である。

LOTOS（Language of Temporal Ordering Specification）の特徴

LOTOSは最初ISOのOSI（オープンシステム相互接続）プロトコルを形式的に記述するための形式記述技法（FDT）の1つとして開発された。その後1989年にISO8807でLOTOS自体が分散システムのためのFDTとして標準化されたのである。

LOTOSではデータ構造を抽象データ型で記述し、システムの動的振る舞いをプロセス代数によって記述する。LOTOSの抽象データ型の記述は、代数的仕様記述言語ACT ONEに基づいている。これに対してLOTOSのプロセス代数の記述は、MilnerのCCSとHoareのCSPを組み合わせている。

LOTOSでは、外部環境とイベントによって相互作用するプロセスとしてシステムを記述する。またイベントの実行順序によってプロセスの動的振る舞いを記述する。相互作用点であるゲートとデータのリストによってイベントを定義する。イベントのデータを用いることで相互に通信するプロセスがデータを交換する。

LOTOSは開発の経緯からわかるように、通信プロトコルの形式的な仕様記述が主な適用分野である。

SpecC（Specification description language based on C）の特徴

カリフォルニア大学アーバイン校のGajski教授らが1997年に開発したSpecCは、ハードウェア（回路設計仕様）を記述できるようにC言語を拡張した仕様記述言語である。SpecCでは、並列処理、データパス付き有限状態機械(FSMD)、信号処理、チャネルクラス、割り込み処理、同期並行処理、タイミング機構などが追加されている。

システムLSI設計ではハードウェアとその上で実行されるソフトウェアを同時並行開発する。SpecCを用いることによりハードウェアとソフトウェアからなるシステムを上流から一貫して設計するだけでなく、検証できるような開発環境としてSCE（System-on-Chip Environment）が提供されている。

SpecCの標準化団体としては、1999年にSTOC（SpecC Technology Open Consortium）が設立されている。またSpecCコンパイラはSTOCのホームページから無償ダウンロードできる。

さて次回は、仕様記述言語、Z言語とVDM−SLの具体例についてみていこう。 タイトルへ戻る