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

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

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

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

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

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

Z言語とVDM-SLの特徴

今回は、具体的な例題である「Webサイトの住所録」をZ言語とVDM-SLで記述することにより、両者の仕様記述言語としての類似点をみていこう。

例題「Webサイトの住所録」

本記事では、組織の名前とその組織が公開しているWebサイトのURLを住所として対応付けて管理するという「Webサイトの住所録」を用いる。住所はもちろん物理的なものを登録しても良い。

参考文献
本記事における例題は、九州大学の荒木先生の教科書に掲載されているものを先生の了解を得て使わせていただいた。荒木先生に感謝いたします。

プログラム仕様記述論
荒木 啓二郎 張 漢明共著
オーム出版局刊(2002)

さて、このような住所録のデータ構造は、プログラミング言語だと配列や表で定義することができる。これに対して形式的仕様記述言語では、集合と写像という数学的な概念によって、住所録をモデル化することになる。

今回の例題では、図に示すように住所録を写像、名前と住所の内容を住所録写像の定義域と値域の集合として表現することができる。



例えば、名前「Think IT」が「www.thinkit.co.jp」に写像される。このとき、名前の集合{ThinkIT, システム科学研究所}が住所録写像の定義域となる。同じように住所の集合{www.thinkit.co.jp, www.riss-net.jp}が住所録写像の値域になる。

しかし、写像だけでは住所録の状態を管理できない。そこで、具体的な集合の値の組を状態として表現する必要がある。例えば、集合の要素の組の集合{(ThinkIT、www.thinkit.co.jp),(システム科学研究所, www.riss-net.jp)}を状態に対する集合として表現する。また、この集合には名前と住所の組が追加される。つまり写像型によって対応付けられた値の組の集合によって状態を表現するのである。

このように、仕様記述言語ではデータ型、状態型、操作型を宣言し、それらの実体が満たすべき条件を定義していく。

では実際に、これらを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による仕様記述の具体例