Z言語による仕様記述の具体例

まず下図にZ言語の操作定義で用いる入出力変数や状態に関する名称の表記法を示す。Z言語による住所登録の記述例もまとめて紹介する。

Z言語では変数名の直後に「?」がついていれば入力とし、「!」がついていれば出力とみなす。また名前の直後に「'」があれば事後オブジェクトであるとみなす。

それでは順番に説明していこう。

型宣言

所与の型「CHAR」では、その内容の詳細にはそれ以上立ち入らず、何かしら定義されていると仮定して、以下の仕様を記述しようというものである。これによって仕様記述の抽象性を管理できることになる。

列型「seq」によって文字列型「String」をCHARの列として宣言することができる。Name型とAddress型はString型として宣言する。ここで「==」によって、右辺の式を左辺の式で示すことができるようにしている。

状態宣言

AddressBookを定義するスキーマでは、addressBookという変数が型「Name -|-> Address」を持つ変数として定義されている。つまり定義域をName型の集合、値域をAddress型の集合とする写像として定義する。「-|->」は部分関数をあらわす演算子である。

InitAddressBookの述語部では、AddressBook型の初期状態満たすべき条件が空写像であるという制約条件を表現している。

操作宣言

AddAddress操作では、⊿AddressBookによって、addressBookの事前状態と事後状態がまとめて引用されている。このように「⊿」は型の変数の事前状態と事後状態が同時に引用されていることを示す記号である。また入力変数nameとaddressを宣言している。

AddAddress操作の述語部では、この操作に関する事前条件と事後条件を記述する。まず事前条件では、nameがaddressBookの定義域の集合の要素として含まれていないことを求めている。また事後条件では、addressBookの事前状態の集合と、入力変数の値の組（name, address）との和集合が、addressBookの事後状態の集合になるという制約条件を記述している。

このように、Z言語では集合や写像の概念を用いてソフトウェアの仕様を自然に記述することができる。

Z言語についてのさらに詳しい説明については、玉井先生の教科書が参考になる。またMike SpiveyのWebサイトから、Z言語の参照マニュアルをダウンロードできる。LinuxなどのUNIXか環境があればZ言語の型チェッカーをダウンロードして使うこともできるので参考にしていただきたい。

さて次にVDM-SLの具体例をみていこう。 次のページ