「Z言語」の歴史的背景

Z言語は1970年代の終わりにOxford大学プログラミング研究グループのAbrialらによって開発された。Z言語はOxford大学とIBMのHursley研究所がCICS（Customer Information Control System）の開発に適用したことで実用性が認められた。その後、Z言語はISOで2002年に標準化されている。

Abrialは1980年代になってB-Methodをフランスで開発した（B-Methodは開発手法全体の総称）。B-Methodでは形式仕様からコード生成でき、パリの地下鉄などへの適用実績もある。Bは1990年代末に時間制約を扱えるように拡張されたEvent-Bとして現在もなお発展している。

Z言語を中心としたこれらの仕様記述言語の発展の歴史は次のようになる。

「Z言語」の記述の特徴

仕様記述言語としてのZ言語の特徴は、スキーマ表記である。スキーマによりシステムの状態と操作を記述する。上図に示したように、スキーマは宣言部と不変式や条件式を記述する述語部の2つに仕切られている。

状態スキーマでは、宣言部で状態空間を構成する変数を記述し、述語部で変数が満たす性質を不変式を用いて記述する。

操作スキーマでは、宣言部で状態空間を構成する状態スキーマとシステム入出力を記述し、述語部でシステム入力に関する事前条件とシステム出力に関する事後条件を記述する。

では次に、VDM-SLについて解説していこう。 次のページ