長所と短所
前回までで，Z言語を用いた記述法に関して，教科書に沿った内容を記述した（もちろん全部ではない）．
最後にまとめである．
以下の良い点を持つ素直なアプローチだとしている．
- システムの状態空間を説明するための数学的記法を持ち，不変条件を用いた集合および集合間の条件を記載することができる
- 集合に対する操作に関して，次を記述することができる；操作が実行可能であるための事前条件．操作による効果を説明する事後条件（変数の変化として示す）
- スキーマ単位に分割ができる．組み合わせによって，大きなシステムの仕様を作ることができる
- 型検査・演繹推論・一貫性検査・不変条件の証明・表明（事前条件・事後条件）の反例付き検証が可能である
要求の記述として不足している点は以下の通りである．
- 非機能要件（速度や使い勝手など）を記述することができない
- どういう場合に操作を実行できるかを事前条件として記述することができるが，遂行義務（obligation）を書くことができない（例えば，エラーを検知したらエラー状態に遷移しなければならないといったこと，次のイベントベースを参照のこと）
- 履歴の記憶を表現することが簡単ではない（例えば，「図書館で最後に特定の本を借りた人」）
次回からは，イベントベースの仕様について，SCRを用いて記述する．
(nil)