KAOS (101) 状態ベースの仕様 (4.4.3-2)

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

ここでの例題は,図書館管理システムである(定番とも云える).

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

[Book, BookCopy, Author, Topic, Person]

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

スキーマ

Z言語では,スキーマ(図式)によって,部品を作る.スキーマには,データスキーマと操作スキーマの2種類がある.

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

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

データスキーマ

ここでは,Directory(索引,昔の検索用カードが相当)のデータスキーマを考える.スキーマという位であり,半図的に表現する 2

z_directory

Directory のデータスキーマ

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

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

宣言部

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

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

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

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

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

述語部

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

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

(nil)

Notes:

  1. ISO/IEC 13568:2002
    Information technology — Z formal specification notation — Syntax, type system and semantics
  2. 今回は,Common Z Tools を使い,LaTex出力している
  3. ISOでは,単に関数としている