KAOS (103) 状態ベースの仕様 (4.4.3-4)

書架データスキーマ

次に,書架データスキーマ(LibraryShelves)を定義する 1

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)

Notes:

  1. 一部原著から書き換えた(エラーを避けるために,LoanLimitを宣言したのと,述語部の最後の式を分かりやすくした)