Z言語とVDM-SLの振る舞い記述の違い

Z言語とVDM-SLの振る舞い定義を比較した表を示す。前回「第3回：Z言語とVDM-SLの記述例」では状態モデルの操作について解説したので、今回は関数について解説していく。

Z言語では関数の定義形態には下図のような方法がある。定義域の変数が制約条件式を満たす値のとき、式に代入した結果が関数の値になる。λ抽象による定義についても下図のように記述できる。またZ言語では、汎用定義（Generic Definition）という関数や型を引数にできる機構が用意されている。

VDM-SLでは、関数の値を本体で明示的に記述する「陽関数」表現と、関数の値を事後条件として満たすべき制約条件式で暗黙的に記述する「陰関数」表現の2つが用意されている。

ここまで、仕様記述言語のZ言語とVDM-SLを取り上げ、その基本と違いについてみてきた。最後に、仕様記述言語を実際に活用した例を紹介しつつその効果をみていきたい。

仕様記述言語の効果

本記事では2007年11月21日に開催された「高信頼性システム開発手法フォーラム」から、パネルディスカッションで盛り上がった論点を紹介しつつ、その効果を探っていく。

仕様記述を書くことと読むことのどちらが難しいか

議論の中で、「仕様記述を書くことは難しいが、読むことはやさしい」と「仕様記述を書くことはやさしいが、読むことは難しい」という一見すると対立する意見が交わされていた。

これは、問題領域についてのよい論理的なモデルができていて、それを仕様記述言語によって表現する「お手本」が用意されていれば、経験者でなくても容易に仕様を記述できる。また、記述された仕様の意味をきちんと理解するには、経験が必要である。この両者を実現するのは、なかなか難しいということだ。

テストと仕様検証

ある人が「組み込み開発に従事しているのだが、今年から仕様記述言語に取り組んで、現場でのバグ取りに大きな効果が出てきた。現場が本気になってきている」と話しておられた。同様のことをフォーラムで講演していただいた講師の方々全員が指摘しており、仕様記述言語により仕様を客観的に記述することの効果が組み込み開発の現場レベルで出はじめているようだ。

しかし、ここで注意しておかなければいけないことがある。それは「従来のテストを仕様記述による仕様検証にすべて置き換えられるか」という点だ。結論からいえば、すべては置き換えられない。

仕様記述を開発対象システムに対して全面適用したとしても、仕様記述は抽象的な記述であるため、実装するプログラム言語やOSなど、実装時に決定された内容についてのテストは必要になる。

さらに、仕様記述言語の検証環境の制約によって、すべての場合について検証ができない可能性もあるだろう。例えば、仕様記述言語を開発対象の一部に限定して部分適用した場合、適用対象外の部分については検証されないためテストする必要がある。また、適用対象部分についても外部に依存した部分は、必ずしも十分な検証ができるわけではない。

なお、テスト記述の膨大な増加（状態爆発）を避けるためには適切なまとまりにテストを分解する必要がある。しかし最初の適用時にはそのような分け方を発見しにくいため、モデル化と並行して繰り返し分析することが重要であるという指摘があったことを付記しておく。 次のページ