risk = nil;

書架データスキーマ

次に，書架データスキーマ（LibraryShelves）を定義する ¹．

書架（LibraryShelves）データスキーマ

書架という名前は難しい．貸出可能な本が，書架にあることは期待して良いかもしれない．しかし，貸出中の本は書架にはない．その部分は，書架においては空き間となっている．ここでは，仮想的に貸出中の本があるとして，本の状態を「書架」という名前で管理しようとしている．

宣言部

最初の LibraryAgents は，前回のスキーマ呼び出しである．これはスキーマ包含（Schema Inclusion)と呼ばれる．この記法により，スキーマ単位のモジュール化が可能になっている．

貸出可能な本（Available）および貸出中の本（OnLoan）は，BookCopyの巾集合である．これは一般的な本の状態を示している．Zでは，ある集合に含まれるということで，状態を表す．ここでのタイトルが，状態ベースとなっているのも，この表現に由来する．

貸出関数（BorrowedBy）は，物理的な本（BookCopy）から人（Person）への部分関数である．部分関数になっているのは，全ての人に貸し出せないからである．その人は，例えば，利用登録をした図書館利用者でなくてはならないはずである．では，図書館利用者（OrdinaryPatron）としても良さそうであるが，述語部で見るように，図書館スタッフも借りることができるので，ここでは，単に人（Person）となっている．

これで，道具立てはできたので，次にこのスキーマにおいて主張したいことの説明に移る．

述語部分

（述語部1行目）貸出可能本（Available）と貸出中本(OnLoan)の積を，空集合としている．物理的な実体が，両方の状態を持つことはない．

（述語部2行目）貸出関係は，定義部で見たように，本から，人への部分関数であった．その定義域（dom, dominant）は本であり，即ち貸し出されることになるので，（貸出が成立したときには）貸出中となっている．

（述語部3行目）借りる人は，通常の利用者かスタッフである．

（述語部4行目）最後の文にでてくる▷は，値域制限（range restriction）と呼ばれる．貸出関係（本と人の関係）の値域を特定の人で制約したことを示す．そのときの数（#）は，貸出限度（LoanLimit）以下であることを示している．”#”は，集合の要素の数を示している．ここでは，通常の利用者には，貸出制限があることを示している．

(nil）