システム仕様を数式に変換――Z言語で要求仕様を厳密に記述する

Z言語をはじめとする要求仕様記述言語は、厳密さゆえに実用に適さないと言われる。何はともあれ、Z言語とはどんなものか。どのように厳密なのか。システム担当者なら、そのエッセンスを理解しておいたほうがよいだろう。

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

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

図1　Z言語における3つのスキーマ

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言語では、変数や集合名に「'」を付けることにより、操作を施した後の状態を表現する。

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

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

広告編集システムの仕様書をZ言語で書く

誕生日帳システムを例に、Z言語の用法や用語の概要を見てきた。このZ言語を使って、前回UMLで作成した広告編集システムの仕様をZ言語でも記述して比較する。

はじめに、各スキーマの記述に用いるデータ型を宣言する。

[CLIENTID, ORDERID, COPYID, BOOKID, VOLUMEID]

データ型を宣言する際はこのように、型の名称を角括弧（[ ]）でくくって示す。

次に、状態スキーマを記述する。具体的には、「顧客（Client）」「供給（Order）」「原稿（Copy）」「本（Book）」「号数（Volume）」の仕様をそれぞれ定義する。加えて、顧客または本のタイトルを示すための文字列NAME、校了済みフラグISOK、原稿ファイルへのパスを示すFILENAMEという3つのデータ型を宣言しておく必要がある。

[NAME, ISOK, FILENAME]

このうち、校了済みフラグISOKについてはさらに

ISOK:= not_ok | ok

と定義し、「未校了」「校了済み」のどちらかの値をとることを示しておく。

こうして定義したデータ型を用いて、広告編集システムの状態スキーマを記述すると、以下のようになる。

状態スキームで、このシステムが常に満たすべき制約条件を記述した。続いて、広告編集システムの初期化スキームを示す。

この初期化スキーマでは、「初期状態ではシステムにレコードは登録されていない」ということを、空集合の記号０を使って定義している。

続いて、操作スキーマの記述例を挙げる。ここでは、「原稿を入稿する（RecieveCopy）」という処理を対象としている。宣言部にある「△」という記号は、変数OrderとCopyが操作RecieveCopyによって変化しないことを示している。「≡」は変数Client、Book、VolumeがRecieveCopyによって変化することを表す。

UMLとZ言語を比較する

前回はUML、今回はZ言語を解説し、それぞれの手法を用いて広告編集システムの仕様を作成した。その結果を基に、両者を比較したのが表1である。これを見れば、2つの手法のおおよその特徴や相違点をつかんでもらえることと思う。

Z言語は、システムの初期状態や操作について制約条件を詳しく積み重ねて仕様を記述するため、UMLに比べて記述量がどうしても多くなる。このほか、読解する際に集合論や述語論理の知識が不可欠である点に加えて、記述を支援するツールがまだ少ない。Z言語がなかなか普及しないのは、これらの要因によるところが大きい。

しかし、要求仕様におけるあいまいさを排除するというZ言語のメリットは計り知れない。実際、原子力発電所や航空機の制御プログラムといった、より厳密性を求められるシステムの要件定義書は、Z言語を用いて作成されるケースが多い。一般のシステム開発においても、要求定義の段階である程度の工数をかけて厳密な仕様を作成すれば、結果として障害や手戻りの少ないシステムを作り出せる。何かしらのしきい値を設けて記述量を抑えるなど工夫し、Z言語を要求仕様作成にうまく取り入れるべきだろう。

次回、この連載は最終回を迎える。これまで1年あまりにわたって伝えてきた事柄を振り返りながら、要求仕様技術のありようを鳥瞰してみよう。