Alloy で形式手法を始めてみた!~集合の演算・発展編~
ここでは,集合に対する発展的な演算を説明します.
集合と関係式の演算
集合と関係式の演算には,ドットジョインがあります.
ドットジョイン
Alloy では,集合と関係式,あるいは関係式同士に定義される,ドットジョインという演算子があります.
Java や C# では,あるクラスのオブジェクトの public なメンバにアクセスするには object.member のようにドットを使ってメンバを指定しますが,Alloy のドットジョインはそれとは似て非なるものです.
イメージとしては,RDB における JOIN に近いです.
以下,r = {(a, b), (a, c), (b, d), (c, d)}, A = {a, b}, D = {d} とします.
このとき,ドットジョイン A.r は以下のような演算になります.
つまり,集合 A の要素を先頭に持つ関係式を選び,キーとなった要素を落としたもののことです.
同様に,ドットジョイン r.B は以下のようになります.
要素と関係式の演算
要素と関係式の演算には,ボックスジョインがあります.
ボックスジョイン
要素 e と関係式 r に対し,r[e] を e.r と定義します.ここで,単一の要素 e は,唯一の元 e をもつ集合 {e} とみなされています.
これにより,例えば関係式 r の第一成分に重複がない場合,r を関数または部分関数とみなして r[e] という関数的な表示が可能になります.
関係式と関係式の演算
関係式と関係式の演算にもドットジョインが定義できます.
ドットジョイン
r1 = {(a, b), (a, c), (b, c)}, r2 = {(a, c, d), (b, d, e)} の場合,r1.r2 を以下のように定義します.
このとき,r1.r2 は以下のようになります.
つまり,r1 の最後の成分と r2 の最初の成分が一致するものを,キーになった要素を落としてつなげたもののことです.
二項関係に対する演算
二項関係に対する演算には,転置(~),推移閉包(^),反射的推移閉包(*)があります.
二項関係とは,各要素が (a, b) のように二つの要素のペアになっているような集合を指します.
転置(~)
関係式の各要素を逆順に並べ替えたものです.
r = {(a, b), (b, c)} とすると,~r = {(b, a), (c, b)} となります.
推移閉包(^)
推移閉包とは,二項関係を何度か適用して到達可能なペア全体の集合のことです.
例えば,r = {(a, b), (a, c), (b, d)} とすると,この二項関係だけでは a から d へ到達できませんが,
(a, b) と (b, d) の二つを使えば,つまり,{(a, b)}.{(b, d)} = {(a, d)} により,(a, d) という要素が得られ,a から d まで到達可能であることがわかります.
図で表すと,以下のようになります.
- a から到達可能なのは b, c, d なので,(a, b), (a, c), (a, d) が ^r に入ります.
- b から到達可能なのは d なので,(b, d) が ^r に入ります.
- c, d から到達可能な点はありません.
よって,^r = {(a, b), (a, c), (a, d), (b, c)} となります.
言い換えると,ドットジョインを何度か使って到達できれば良いわけですから,
^r = r + r.r + (r.r).r + … となります.
反射的推移閉包(*)
これは,推移閉包に加えて自分自身との関係式を追加したものです.
先程の例だと,^r + {(a, a), (b, b), (c, c), (d, d)} となります.
言い換えると,*r = ^r + iden となります.
関係式の制限
始集合の制限(<:)
集合 A と関係 r に対し,A <: r で,r の第一成分を集合 A に制限したものを表します.
終集合の制限(:>)
集合 B と関係 r に対し,r :> B で,r の最後の成分を集合 B に制限したものを表します.
始集合と終集合の制限をまとめると,以下のようになります.
抽象シグネチャ Airport は,Airport 同士の関係式として route を持つとします.ここでは,route は,空港間に直行便の航空路があるかどうかを意味することとします.
また,Airport は国際空港(羽田や関空など)か国内便しか飛ばない空港(伊丹や丘珠など)かのどちらかであるとします.
abstract sig Airport {
route: set Airport
}
sig InternationalAirport, DomesticAirport extends Airport {}
このとき,DomesticAirport <: route :> InternationalAirport は,国内先しか飛ばない空港から国際空港への航路を表します.このように書くと,記法が理解しやすいのではないでしょうか.
関係式のオーバーライド(++)
r1, r2 はともに要素のタプルの長さ(アリティ)が同じであるような関係式とします.
このとき,r1 ++ r2 を,以下のように定義します.
- r2 の要素全てと,r1 の要素のうち r2 の要素の第一成分を第一成分にもつもの以外の和
文字にするとわかりにくいですが,図にすると以下のようになり,オーバーライド感が出ます.
最後に
次は,if や iff などの条件式,制約条件の書き方や,Pred, Func, Fact などについてまとめたいと思います.
参考
非公式ドキュメントですが,基本的にはここを参照しています.
公式の言語リファレンスも参考にしています.
過去の投稿
- Alloy で形式手法を始めてみた!~導入編~
- Alloy で形式手法を始めてみた!~シグネチャ編~
- Alloy で形式手法を始めてみた!~関係式の多重度編~
- Alloy で形式手法を始めてみた!~特殊なシグネチャ編~
- Alloy で形式手法を始めてみた!~集合の演算と数値編~
では!
コメント