[要求仕様の美学]

2009年10月2日(金)福田 修

　Z言語は1970年代に生まれた代表的な要求仕様記述言語であるが、誕生から40年近くたった今もその知名度はなぜか低い。論理学や数学で用いる特殊な記号を多用することから、敷居が高いと感じるITエンジニアも少なくないようだ。

　しかし、誤解のない要求仕様書作成を目指すには、Z言語は避けて通れない技術といっても過言ではない。そこで今回は、Z言語の概要と使用例、さらに有効性について述べる。

　Z言語においては、「スキーマ」と呼ぶ表記法に基づいてシステムの仕様を表す。その際に用いられるスキーマの種類は、主に3つある。「状態スキーマ」 「初期化スキーマ」「操作スキーマ」で ある。

　状態スキーマには、システムが常に満たしていなければならない条件を記述する。初期化スキーマには、システムの初期状態で満たしておかなければならない条件を記述する。

　さらに操作スキーマでは、システムに対する操作の仕様を記述する。操作を行った際にシステムの状態がどのように変化するか、また操作の前後でシステムが満たしていなければならない制約条件を表す。

　スキーマは、スキーマ名と上下に分割された箱を使って表記する。箱の上部は「宣言部」と呼び、スキーマ中で使用する変数や関数を定義する。スキーマの下部は「述語部」と呼び、変数や関数の制約や操作を記述する。さらに、集合論や述語論理の用語・記号を用いて数式で記述することもZ言語の特徴である。

　以下ではZ言語の用語や記述イメージを概観するために、人の名前と誕生日を組み合わせて登録する誕生日帳システムの仕様を見ていこう。

誕生日帳システムの仕様をZ言語で記述する

　まず、誕生日帳システムの状態スキーマ「BirthdayBook」の例を示す。

　宣言部1行めは、birthdayがNAME型からDATE型への部分関数であることを表している。つまり、NAME型の値「n」を与えれば、DATE型の値「d」が一意に定まるということだ。このとき、nとdの組み合わせを「対」と呼び、その関係を

nd

と表す。

　状態スキーマの宣言部2行目は、変数known がNAMEのべき集合であることを表している。「」は、べき集合を示す記号である。べき集合とは、ある集合の部分集合すべてを集めた集合のことだ。例えば、集合Sが整数1、2、3から成るとき、集合Sのべき集合（S）は、

(S) = { {}, {1}, {2}, {3}, {1, 2}, {2, 3}, {1,3}, {1, 2, 3} }

である。

　Z言語では、関数の定義域（domain）を「dom」という記号で表現する。従って、スキーマの述語部にある

known = dom birthday

　という記述は、known に含まれる要素はbirthdayという関数を使って値を得られる「システムに登録済みの対」であること、およびknownに含まれない要素は関数birthdayでは値の得られない「システムに未登録の対」であることを示す。

　誕生日帳システムの初期化スキーマでは、システムの初期状態では登録されている名前と誕生日の対がないことを定義する。

この初期化スキーマは、以下のようにも記述できる。「∅」は、空集合を意味する記号である。

　続いて、操作スキーマである。ここでは、誕生日帳に名前と誕生日の組み合わせを新たに追加する操作「AddBirthday」を記述する。

　宣言部の1行目にあるΔBirthday Bookは、AddBirthdayにより状態スキーマBirthdayBookが変化することを宣言している。続く2〜3行めは、変数nとdの宣言である。変数名の後ろの「?」は、その変数が入力変数であることを示す。これに対して、出力変数を示す記号は「!」である。

　AddBirthdayの述語部には、この操作を施す前後の制約条件を記述する。

n? ∉ known

は、入力された名前がシステムに登録されていない状態を表す。述語部2行めの

birthday' = birthday ∪ {n? d?}

は、操作前のbirthday変数の集合と、入力変数n、dの値の組との和集合が、操作後の集合birthday'になるという条件を示している。Z言語では、変数や集合名に「'」を付けることにより、操作を施した後の状態を表現する。

　このほか、誕生日帳からレコードを削除する操作スキーマは、以下のようになる。

　「」は、集合から任意のレコードを削除することを示す記号である。