図書館システムデータスキーマ
これまで準備したスキーマを用いて，図書館システム（LibrarySystem）を定義する．
図書館システム（LibrarySystem）データスキーマ
宣言部では，以前に作成したスキーマを利用している（Directory は，101回目で，Libraryは，前回（103回目）に定義している）．即ち，図書館システムは，本の基本情報を示すDirectoryと，書架LibraryShelves（ここには，図書館利用者を定義したLibraryAgentsも含む）からなるとしている．
述語部には，不変条件を一つだけ記載している．WhichBookは，物理的な実体を持つ本から，論理的な本への関数であった．domは，定義域を表す．従って，対応関係の元である物理的な実体を持つ本を指している．この本は，利用可能集合（Available）と貸出中集合（OnLoan）の和となっている．即ち，いま図書館の書庫にあるか否かに関わらず，その図書館が持っている全ての本を指している．
もちろん，それ以外の状態（例えば，破損したので修復中である）も取り得るが，ここでは，利用可能か貸出中かの2つに分けている．書架スキーマにおいては，利用可能集合と貸出中の積は，空集合だった．従って，実際には，どちらかにしか属さないことになる．
(nil）