VDM-SLによる仕様記述の具体例

VDM-SLの操作定義で用いる入出力変数や状態に関する名称の表記法を下図に示す。VDM-SLでは、シグネチャの引数と関数値によって入出力変数を識別している。名前の直後に「~」（チルダ記号）があれば事前オブジェクトだとみなす。また事後オブジェクトには何も付けない。

VDM-SLによる住所登録の記述例を上図にまとめて紹介する。図ではZと比較するため状態モデルに基づく記述例を示した。

VDM-SLでは、関数に基づく記述も可能だ。興味のある方は荒木先生の教科書を見ていただきたい。それではZ言語と同様に順番にを説明していこう。

型宣言

VDM-SLでは文字型charが基本型として用意されている。これによって仕様記述の抽象性を管理できる。

また列型「seq of」によって文字列型「String」を文字要素が順番に並んだ集合として宣言することができる。

Name型とAddress型はString型として宣言する。ここで「=」によって、右辺の型を左辺の識別子で新しく定義することができる。

状態宣言

AddressBookの状態定義では、bookが写像型「map Name to Address」を持つ変数として定義されている。つまり定義域をName型の集合、値域をAddress型の集合とする写像として定義する。

またbookの初期値が空写像{|->}で定義されている。ここで組構成子「mk_写像名()」によって、空写像から写像の定義域と値域の組を生成して初期化しているというわけである。

操作宣言

AddAddress操作では、シグネチャによって引数nameとaddressを宣言している。またbookを写像型の変数として定義している。ここで「wr」は変数bookの内容を変更できる操作モードであることを示している。変更しない場合は操作モードとして「rd」を指定する。

AddAddress操作が満たすべき条件を事前条件を示すpre式と事後条件を示すpost式で定義する。まず事前条件では、nameがbookの定義域の集合の要素として含まれていないことを求めている。また事後条件では、bookの事前状態の集合book~と、入力変数の値の組で写像の値を表す{name|-> address}との和集合がbookの事後状態の集合になるという制約条件を記述している。

まとめ

今回は、具体的な例題に基づいてZ言語とVDM-SLの記述例を紹介した。両者の共通点として、状態モデルによる仕様記述ができるという点がある。

次回の最終回では、Z言語とVDM-SLの基本的なデータ型や言語の違いを比較していく。また仕様記述言語の適用上の留意点についても紹介する。 タイトルへ戻る