Z言語とVDM-SLの特徴と仕様記述言語の効果を探る

今回はZ言語とVDM-SLの言語的な特徴を比較する。次いで、仕様記述言語を最先端で活用している方々によって得られた有効性や課題についての議論を紹介しよう。

Z言語とVDM-SLのデータ型の違い

まず、Z言語とVDM-SLの型定義の比較表を図に示す。Z言語では集合と関数に基づいて、データ型を定義する。VDM-SLでは関数の代わりに写像を用いる。

仕様記述言語では、データ型の詳細を決めなくても、そのようなデータ型があると仮定して仕様を抽象的に記述することができる。この抽象性が重要である。

Z言語の所与集合では、[Address]のように記述して、Addressの詳細なデータ型の内容を隠して抽象化することができる。同じようにVDM-SLではオプション型を用いることで抽象化できる。またVDM-SLにはトークン型がある。トークン型はトークンと呼ばれる値を持つが、それがどのようなものかを定義する必要はない。

このような考え方は仕様記述では非常に重要である。もし仕様定義段階で値の詳細を決めてしまうと、設計段階までそれを引きずることになり、設計の自由度を低下させてしまうことになるからだ。

つまり、下流工程で決めればいいことは先に延ばし、上流工程で決める必要のあることだけを定義するのが重要である。

またZ言語では要素の値を列挙することで集合からなる単純データ型を定義できる。

VDM-SLでは列型があらかじめ用意されており、Z言語では列型seqを上図のように定義する。上図の「●」は右辺の制約式が成立するような左辺の変数を宣言している。また、「1..n」は1からnまでの集合である。このように、Z言語ではVDM-SLのデータ型を集合と関数を用いて定義できるのである。一方で、VDM-SLでは、集合をset of型として用意している。

Z言語では直積とべき集合で複数の集合の関係を定義しておき、特殊な性質を持つ関係として写像を定義する。VDM-SLでは写像型map 〜 to 〜を持っていることを前回の「第3回：Z言語とVDM-SLの記述例」で紹介した。

レコード構造については、Z言語ではスキーマで記述する。VDM-SLでは複合型を用いて記述できる。

次に、Z言語とVDM-SLの振る舞い記述の違いについて解説しよう。 次のページ