長所と短所
前回までで，Z言語を用いた記述法に関して，教科書に沿った内容を記述した（もちろん全部ではない）．
最後にまとめである．
以下の良い点を持つ素直なアプローチだとしている．
- システムの状態空間を説明するための数学的記法を持ち，不変条件を用いた集合および集合間の条件を記載することができる
- 集合に対する操作に関して，次を記述することができる；操作が実行可能であるための事前条件．操作による効果を説明する事後条件（変数の変化として示す）
- スキーマ単位に分割ができる．組み合わせによって，大きなシステムの仕様を作ることができる
- 型検査・演繹推論・一貫性検査・不変条件の証明・表明（事前条件・事後条件）の反例付き検証が可能である
要求の記述として不足している点は以下の通りである．
- 非機能要件（速度や使い勝手など）を記述することができない
- どういう場合に操作を実行できるかを事前条件として記述することができるが，遂行義務（obligation）を書くことができない（例えば，エラーを検知したらエラー状態に遷移しなければならないといったこと，次のイベントベースを参照のこと）
- 履歴の記憶を表現することが簡単ではない（例えば，「図書館で最後に特定の本を借りた人」）
次回からは，イベントベースの仕様について，SCRを用いて記述する．
(nil)
貸出操作スキーマ
今回は，操作スキーマを定義する．これまでのデータスキーマは，時間によって変化しないものを示している．操作スキーマが与えるのは，操作による動的な変化である．
貸出操作（CheckOut）スキーマ
操作スキーマでも，既に定義しているデータスキーマを利用することができる．但し，先頭に新たな記号が付くことになる．∆は，操作によってスキーマ中の状態が変化することを示している．
例を見てみよう．述語部に，以下の記述がある（p4）．
Available’ = Available \ {bc?}
統合左側のプライムは，変化後の値を持つことを示している．本を貸し出すと，貸出可能な本の集合から（Available），貸し出した本（bc）分は減ることになる．Availableは，LibraryShelvesで定義しているのだが，それはLibrarySystemに包含されているので，その状態が変化するとして，∆の記号を持つ．状態変化を伴わない場合は，Ξの記号を用いる (d2, d3)．
記述部のうち，最初の3つ（p1〜p3）は，事前条件に相当する．後半の3つ (p4-p6) は，先に見たように状態変数の変化を示している．この部分は，事後条件に相当する．
さて，順番に見ていく．
疑問符が付いている状態変数は，入力を示している(d4,d5)．ここでは，借りに来る人（p）とその人が持っている本（bc）を示す変数である．借りに来る人は，利用者として登録している人か，或いは図書館のスタッフである（即ち，それ以外の人は対象外である）(p1)．本は当然利用可能でなくてはならない（貸出中であれば，持っているハズがない）(p2)．
(p3) は少し問題がある．以前にも出てきた▷は，値域制限（range restriction）である．BorrowedByは，LibraryShelvesスキーマで，BookCopyからPersonへの部分関数であり，貸出数に制約を与えるが，不変条件の記述と矛盾しているので，実際には不要である．
(p4) は，先に説明した．(p5) では，貸出を行うので，貸出中（OnLoan）が，貸し出した分だけ増えることを示している．
(p6) 誰に貸しているか関係では，本と借りた人の関係を新たに追加している．
(nil）
図書館システムデータスキーマ
これまで準備したスキーマを用いて，図書館システム（LibrarySystem）を定義する．
図書館システム（LibrarySystem）データスキーマ
宣言部では，以前に作成したスキーマを利用している（Directory は，101回目で，Libraryは，前回（103回目）に定義している）．即ち，図書館システムは，本の基本情報を示すDirectoryと，書架LibraryShelves（ここには，図書館利用者を定義したLibraryAgentsも含む）からなるとしている．
述語部には，不変条件を一つだけ記載している．WhichBookは，物理的な実体を持つ本から，論理的な本への関数であった．domは，定義域を表す．従って，対応関係の元である物理的な実体を持つ本を指している．この本は，利用可能集合（Available）と貸出中集合（OnLoan）の和となっている．即ち，いま図書館の書庫にあるか否かに関わらず，その図書館が持っている全ての本を指している．
もちろん，それ以外の状態（例えば，破損したので修復中である）も取り得るが，ここでは，利用可能か貸出中かの2つに分けている．書架スキーマにおいては，利用可能集合と貸出中の積は，空集合だった．従って，実際には，どちらかにしか属さないことになる．
(nil）