TOPシステム開発> 【新・言語進化論】仕様記述言語を知っていますか?> 第3回:Z言語とVDM-SLの記述例 (3/3)

【新・言語進化論】仕様記述言語を知っていますか?

【新・言語進化論】仕様記述言語を知っていますか?

第3回:Z言語とVDM-SLの記述例

著者:NTTデータ 山本 修一郎

公開日:2007/11/21(水)

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の基本的なデータ型や言語の違いを比較していく。また仕様記述言語の適用上の留意点についても紹介する。 タイトルへ戻る




株式会社NTTデータ 山本 修一郎
著者プロフィール
株式会社NTTデータ 山本 修一郎
フェロー プリンシパルR&Dスペシャリスト 技術開発本部 システム科学研究所 所長
1979年日本電信電話公社入社、2002年NTTデータへ転籍、2007年4月NTTデータ 初代フェロー、技術開発本部システム科学研究所所長に就任。ソフトウェア工学、要求工学、Webデータベース連携、ICカードプラットフォーム、ユビキタスコンピューティング等の研究開発に従事し、最近は知識創造デザイン技術やサービスイノベーションの研究にも取組んでいる。


INDEX
第3回:Z言語とVDM-SLの記述例
  Z言語とVDM-SLの特徴
  Z言語による仕様記述の具体例
VDM-SLによる仕様記述の具体例