Model Base
A.1.3 モデリング時の関係的性質
最終更新：
modelbase
更新日 2011-09-03
[ Alloy Analyzer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題 解答例 ]
これらは、問題領域の用語解釈によって答えが変わってくる。
( a ) sibling：同じ両親を持つ子供の間の兄弟関係
議論領域を"ある両親から生まれた子供たち全員"と考える。
一人っ子のケースは除外する。
以下、兄弟関係rに制約を与える性質を検討すると、 (ここでは、姉や妹も兄や弟と呼ぶことにする)
- 同じ両親から生まれた子供のペアは兄弟関係なので、rは非空的でない
- 自分自身のことを自分の兄弟とは呼ばないので、rは非反射的
- 自分の兄(or弟)にとって自分は兄弟なので、rは対称的
- 自分の兄の弟が自分の場合、自分自身を兄弟と呼ばないので、rは推移的でない(rが非反射的かつ対称的なら、同時に推移的になれないので、推移性に言及する必要はない)
- 自分に兄や弟が複数人数いる場合も考えられるので、rが関数的か否かや、単射的か否かには言及できない。
- 誰もが兄弟を持つので、rは全域的
- 誰もが誰かの兄弟なので、rは全射的
関係rの制約をあらわすのに必要な性質は、
非空的、非反射的、対称的、全域的、全射的
となる。
解答を検算してみよう。
-- 構造の記述
sig C{
sibling: set C
}
fact{ #C > 1 }
-- 子供たちは皆兄弟
pred anyone_is_sibiling{
all disj c1,c2: C | c1->c2 in sibling
no (iden & sibling)
}
-- 定義が適切かどうか様子を見る
run show{
anyone_is_sibiling
}for 4
-- 解答
-- 兄弟関係が持つべき性質
pred property{
let r = sibling, U = C{
-- nonempty
(some r)
-- irreflexive
(no iden & r)
-- symmetric
(~r in r)
-- total
(U in r.U)
-- onto
(U in U.r)
}
}
-- 検算
check valid{
anyone_is_sibiling => property
}for 4
( b ) links：ネットワーク上の１ホストと、そのホストにリンクする複数のホストとの間のリンク関係
スキップ
"ホストにリンクする"という表現だけでは、自分の常識の範囲では期待されている制約を想定できないので、"リンク関係"と呼ばれる関係に与える制約には、どの性質が必要になるのかわからない。
(実際の業務ならそのドメインの専門家にヒアリングしたいところ。。。)
( c ) contains：ファイルシステムにおけるディレクトリとその中身との関係
Unixのファイルシステムを想定。ルートディレクトリ以外に1つ以上ファイルがあるとし、シンボリックリンクは想定外とする。 議論領域は"ファイル"と考える。
以下、ディレクトリとその中身の関係rに制約を与える性質を検討すると、
- ルートディレクトリ以外にもファイルがあるので、rは非空的
- 孫ディレクトリは親ディレクトリの中身と言わないことにすれば、rは推移的でない。と、検算前は推移的でないと思ったが、ルートディレクトリの直下にファイルがあるだけの場合は推移的になるので、結局、rが推移的か否かに言及できない
- 通常"ディレクトリの中身"というとき、そのディレクトリ自身は含まないので、rは非反射的
- 親ディレクトリを中身にできないので、rは対称的でない
- ディレクトリの中のファイル数には制約がないので、rが関数的か否かに言及できない
- 同時に複数のディレクトリの中身となるファイルはないので、rは単射的
- 必ずファイルは中身を持たないファイルがあるので、rは全域的でない
- ルートディレクトリは親ディレクトリが無いので、rは全射的でない
関係rの制約をあらわすのに必要な性質は、
非空的、非反射的、対称的、単射的、全域的、全射的
となる。
解答を検算してみよう。(というか、Alloyの解析結果をみながら解答を手直しした)
open util/graph[File] as gr
-- 構造の記述
sig File{
contains: set File
}
sig Dir extends File{}
one sig Root extends Dir{}
pred fileSystem{
let r = contains{
-- graphライブラリを使って記述を省略
gr/tree[r]
gr/rootedAt[r, Root]
(File - Dir) in leaves[r]
some (File - Root)
}
}
-- ファイルシステムの定義が適切かどうか様子を見る
run show{
fileSystem
}for 4
-- 解答
-- ファイルシステムが持つべき性質
pred property{
let r = contains, U = File{
-- nonempty
(some r)
-- irreflexive
(no iden & r)
-- Not symmetric
not (~r in r)
-- injective
(r.~r in iden)
-- Not total
not (U in r.U)
-- Not onto
not (U in U.r)
}
}
-- 検算
check valid{
fileSystem => property
}for 4
反例が出ないので自分が考える"ファイルシステム"においては、必要な性質記述になっていると思う。
( d) group：ドローツール中の図的要素とグループ（同時に選択・非選択されている要素の集まり）との間のグループ関係
スキップ
( e ) sameGroup：同じグループ内での図的要素間の関係
スキップ
( f ) supersedes：あるファイルシステム内のファイルと別のファイルシステム内のファイルとの関係で、前者のファイルが後者のファイルの新バージョンになっているような関係
スキップ
( g ) substitutableFor：ある規格に準拠した任意のシステムにある2 つの部品間で、前にある方が後ろにある方で置き換え可能な関係（例えば電源は、同電圧で、同等以上の電力を供給する別の電源と置き換え可能である。）
規格は1種類以上あり、部品は複数存在し、部品は必ず何かの規格に準拠している、と想定する。
以下、部品間の置き換え可能な関係rに制約を与える性質を検討すると、
- 置き換え不能な部品もあるので、rが非空的か否かに言及できない
- 置き換え可能な部品は、被置換部品のすべての規格に準拠しているので、rは推移的
- 同じ部品で置き換えしてもよいので、rは非反射的でない
- 常識的には部品は交互に交換可能でないのでrは対称的でないが、全て万能部品(規格間に排他な関係がないとして、全規格に準拠した部品)にできれば、常に交互に交換可能であるから、rが対称的か否かに言及できない
- ある部品の置き換え可能な部品の数は限定できないので、rが関数的か否かに言及できない
- ある部品が幾つの被交換部品へ交換されるか、その数は限定できないので、rが単射的か否かに言及できない
- すべての部品について交換可能な部品の有無は限定できないので、rが全域的か否かに言及できない
- すべての部品について被交換部品の有無は限定できないので、rが全射的か否かに言及できない
関係rの制約をあらわすのに必要な性質は、
推移的、非反射的
となる。
解答を検算してみよう。
-- 構造の記述
some sig Standard{}
some sig Component{
based: some Standard,
substiutableFor: set Component
}
fact{ #Component > 1 }
-- 部品交換の可能性についての定義
pred component_compatibilty{
all c1,c2: Component | c1.based in c2.based <=> c1->c2 in substiutableFor
}
-- 定義が適切かどうか様子を見る
run show{
component_compatibilty
}for 4
-- 解答
-- 部品間の置き換え可能な関係が持つべき性質
pred property{
let r = substiutableFor{
-- transitive
(r.r in r)
-- irreflexive
not (no iden & r)
}
}
-- 検算
check valid{
component_compatibilty => property
}for 4
反例はなし。
