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でどのように記述するのかを説明していこう。ただし今回は住所の登録操作だけを紹介する。住所の検索については、荒木先生の教科書に掲載されているので参考にしていただきたい。 次のページ