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）

ここからしばらくは，仕様記述言語Zについてである．この言語は，ISOで定義されている ¹

ここでの例題は，図書館管理システムである（定番とも云える）．

最初に，無条件に使える集合を宣言しておく．

［Book, BookCopy, Author, Topic, Person]

BookとBookCopyの違いを示すための日本語として，適切ないい方を思いつかない．Bookは，抽象的な概念（LamsweerdeさんのRequirements Engineering）の本であり，BookCopyは，今，手元にあるボロボロになった物理的な本である．

スキーマ

Z言語では，スキーマ（図式）によって，部品を作る．スキーマには，データスキーマと操作スキーマの2種類がある．

• データスキーマ：システムを表現するために必要な状態変数のうち，関連するものをまとめたもの．状態変数間の関係は，不変条件として記述する．
• 操作スキーマ：システムに対する操作によって，システムは変更を受ける．このことを，状態変数の値の変化として示す．事前条件と事後条件を記述する．

先ずは，データスキーマから見ることにする．

データスキーマ

ここでは，Directory（索引，昔の検索用カードが相当）のデータスキーマを考える．スキーマという位であり，半図的に表現する ²．

Directory のデータスキーマ

最初に いくつかの記号の記号の説明を行う．

罫線で囲まれている部分が，スキーマである．全体は，2つに分かれている．前段が宣言部で，後段が述語部と呼ばれる．宣言部で準備した用語を用いて，述語部で記述を行う．

宣言部

宣言部では，集合自身の宣言と，ある集合から別の集合への関係を考える．Zは，2つの集合の関係を表現するのに多様な表現を持っている．また，集合同士の関係のうち，関係の元になっているのが，定義域（domain）であり，関係先の集合が，値域（range）と呼ばれる．いま，リンゴ型とミカン型を考えたときに，リンゴ型の変数とミカン型の変数を区別せずに演算することはできない（例えば，足し合わせる）．代わりに何らかの関係を定めることで，必要な演算を行うことになる．

 ⇸は，（部分）関数を示している．いま，何の本（WhichBook）では，物理的な本（BookCopy）と概念上の本（Book）の対応付けを考える．部分関数としているのは，全ての物理的な本が，必ずしも全ての概念上の本と関係づけられているわけではないということを意味している（国会図書館といえども全ての本を持っているわけではない）．ただ，定義域の各値が，単一の値域の値に紐付けばよく，ここでは標準的な関係である ³．全て対応付けをすることができる場合には，全関数（total function）と呼ばれる．

 ℙは，巾集合（power set）を示している．集合の集合である．X = {0, 1} とするときに 巾集合 ℙX は，次の様になる．{∅, {0}, {1}, {1,2}} である．著者は，一人とは限らず，複数の場合もある．従って，著者の巾集合が値域となる．ちなみに∅は，空集合を示す．著者が∅というのは，考えにくいが規格のような組織によって発行されているものは，明示的な著者がいないと考えることができる（現実がどうかは別にして，そういうモデルを考えるということになる）．

本のメタ情報（Cover）は，同様に複数のトピック（Topic)を持ち得る．やはり，値域はトピックの巾集合となる．

ここまでが，スキーマの仕切り線の上部にある宣言部である．仕切り線の下側は述語部と呼ばれる．

述語部

述語部の最初，部分関数 WrittenBy の定義域である Book は，WhichBook の値域 Book と等しいか，含まれるということを示している．また，2行目は，Covers の定義域 Book は，WhichBookの値域 Book と等しいか含まれるということを示している．WrittenBy や Cover といった部分関数は，特定の Book から検索するため，全てが対象にならないかもしれない位の意味である．

宣言部分では，データにおける制約（invariant, 不変条件）を示している．書き方という意味では重要である．

(nil)