Alloy Analyzer を使ってみようと思ってはや数ヶ月，いくつか文献を見たけど無定義で記号が使われたりしていたりでぶん投げ続けていますが，もう日本語で文献を調べるのはやめました．
初歩の初歩は [hoge lecture] でググるのが一番ですね．
ということで，ちまちまと Alloy Analyzer の記法を加筆修正していきます．
Alloy Analyzer の文法まとめ
オブジェクト
Alloy ではすべてのオブジェクト（スカラーや集合，二項関係など）を"関係"で表す．
集合
AddressBook = { (Book0), (Book1) }
Name = { (Taro), (Hanako) }
Address = { (Tokyo), (Osaka), (Fukuoka) }
スカラー：単行関係
myAddr = { (Osaka) }
myName = { (Taro) }
myBook = { (Book0) }
二項関係
names = { (Book0, Taro), (Book0, Hanako) }
※当然だが関数ではない．
三項関係
addrs = { (Book0, Taro, Tokyo), (Book0, Hanako, Fukuoka), (Book1, Taro, Osaka), (Book1, Hanako, Fukuoka) }
特に，集合の元の個数は size，各元の列の個数を arity という．上記の三項関係の例の場合，size = 4, arity = 3 である．
また，n 項関係は列が n の，列名のない表と思える．ただし，列が入れ替われば当然 n 項関係としての意味合いは変わる．
定数扱いの集合
| 集合 | 意味 |
|---|---|
| none | 空集合 |
| univ | 全体集合 |
| iden | 恒等関係 |
定数扱いの集合の例
Name = { (N0), (N1), (N2) },
Addr = { (A0), (A1) }
のとき，
none = { },
univ = { (N0), (N1), (N2), (A0), (A1) },
iden = { (N0, N0), (N1, N1), (N2, N2), (A0, A0), (A1, A1) }
となる．
集合の演算子
| 演算子 | 意味 |
|---|---|
| + | 和集合 |
| & | 共通部分 |
| - | 差集合 |
| in | 部分集合 |
| = | イコール |
| -> | 直積 |
集合の演算の具体例
Name = { (N0), (N1), (N2) },
Alias = { (N1), (N2) },
Group = { (N0) },
RecentlyUsed = { (N0), (N2) }
Addr = { (A0), (A1) }
のとき，
| 演算 | 演算結果 |
|---|---|
| Alias + Group | { (N0), (N1), (N2) } |
| Alias & RecentlyUsed | { (N0) } |
| Name - RecentlyUsed | { (N1) } |
| Alias -> Addr | { (N1, A0), (N1, A1), (N2, A0), (N2, A1) } |
| RecentlyUsed in Alias | false |
| RecentlyUsed in Name | true |
| Name = Group + Alias | true |
となる．
関係の Join
関係 p, q に対して，
- p.q で「p の末尾と q の先頭での Join」を表し (dot join)，
- p[q] で q.p を表す (box join)．
ただし，Join したあとは結びになった項は落とされる．
関係の Join の例
p = { (a, b), (a, c), (b, d) }, q = { (a, b, c), (b, c, d), (b, a, d), (c, c, b) }, r = { (c) }のとき，
| Join | Join 結果 |
|---|---|
| p.q | { (a, c, d), (a, a, d) } |
| r.q | { (c, b) } |
| p[q] | { (c, c, d) } |
単項演算子
ここでは
Node = { (N0), (N1), (N2), (N3) },
next = { (N0, N1), (N1, N2), (N2, N3) }
とする．
| 演算 | 意味 | 例 |
|---|---|---|
| ~ | 転置 | ~next = { (N1, N0), (N2, N1), (N3, N2) } |
| ^ | 推移閉包. ^r = r + r.r + r.r.r + … | ^next = { (N0, N1), (N0, N2), (N0, N3), (N1, N2), (N1, N3), (N2, N3) } |
| * | 反射推移閉包. *r = iden + ^r | *next = { (N0, N0), (N1, N1), (N2, N2), (N3, N3) } + ^next |
制限とオーバーライド
特定の関係を取り出す手段に"制限"と"オーバーライド"がある．
Addr = { (A0) },
Name = { (N0), (N1), (N2) },
Alias = { (N0), (N1) },
address = { (N0, N1), (N1, N2), (N2, A0) },
workAddress = { (N0, N1), (N1, A１) }
とする．
| 演算 | 意味 | 例 |
|---|---|---|
| p <: q | q の 1 要素目の p への制限 | Alias <: address = { ((N0, N1), (N1, N2) }（address のうち，左側が Alias に入っているやつ） |
| p :> q | p 最終要素の q への制限 | address :> Name = { ((N0, N1), (N1, N2) }（address のうち，右側が Name に入っているやつ） |
| p ++ q | p の中で，q と同じ 1 要素目を持つものを q の関係で置き換える | address ++ workAddress = { (N0, N1), (N1, A1), (N2, A0)} |
意味合い的に，以下のようにも書ける：
p ++ q = p - (domain[q] <: p) + q （ p から，q と 1 列目がかぶっているものを引いておいて，その代わり q で置き換える）．
bool 値の演算子
p, q を bool 値とする．
| 演算 | 意味 |
|---|---|
| !p, not p | p でない |
| p && q, p and q | p かつ q |
| p || q p or q | P または q |
F, G, H を論理式とする．
| 演算 | 意味 |
|---|---|
| F => G | F && G ？!F || G ではなく？？ |
| F => G else H, F implies G else H | (F && G) || ((!F) && H) |
| F <=> G, F iff G | F => G and G => F |
含意ではなく，if - else - っぽい．
限量子
- all x: e | F
F holds for all x in e. - all x: e1, y: e2 | F
F holds for all x in e1 and all y in e2. - all x, y: e | F
F holds for all x and y in e. - all disj x, y: e | F
F holds for all dictinct element x and y in e.（多分）
なお，all の他には以下もある．
| 限量子 | 意味 |
|---|---|
| all | for all |
| some | for at least one |
| no | no |
| lone | at most one |
| one | exactly one |
限量子は | までかかるように思われる．
例
some n: Name, a: Address | a in n.address
ある n: Name とある a: Address があって，a は n の住所である．
言い換えると，AddressBook は空でない．
集合の宣言
x: hoge e の形．hoge のところに色々入る．
| 宣言 | 意味 |
|---|---|
| x: set e | x は e の部分集合 |
| x: one e | x は e の部分集合であって唯一の元をもつ |
| x: lone e | x は e の部分集合であって元を高々一つもつ |
| x: some e | x は e の空でない部分集合 |
| x: e | x: one e と同じ意味．x は e の元，に近いといえば近い． |
関係の宣言
r: A hoge -> fuga B の形．
これが意味するところは，「A is mapped to fuga elements of B, and hoge elements of A is mapped to B」である．
例えば，members: Name lone -> some Addr は，どの Name にも必ず Addr が対応していて，かつどの Addr も高々一つの Name に対応している（どの Addr も，それを参照する Name を持たないか，持つとしてもちょうど 1 つだけである）とうことである．
hoge, fuga が省略されたときは，hoge も fuga も set として扱われる．
表現の限量子
some, no, lone, one を用いる．
例
no (address.Addr - Name) は，Addr へ飛ぶのは Name の元以外にない，といっている．
前に出した例では以下のようになる：
Addr = { (A0) },
Name = { (N0), (N1), (N2) },
address = { (N0, N1), (N1, N2), (N2, A0) }
とすると，address.Addr = { (N2) } なので，no (address.Addr - Name) が成り立っている．
集合，関係の生成
{ n: Name | no n.^address & Addr } の意味は，Addr へ推移されないような Name 全体の集合．
{ n: Name, a: Address | n -> a in ^address} の意味は，n -> a が address の推移閉包に含まれるということ．言い換えると， 到達可能な( 名前, アドレス )全体．
if と let
if は Alloy では f implies e1 else e2 と書く．
let は一時変数．
基数
| 式 | 意味 |
|---|---|
| #r | 関係 r に含まれるタプルの個数 |
| 0, 1, ... | 整数 |
| + | プラス |
| - | マイナス |
| = | イコール |
| < | 小なり |
| > | 大なり |
| =< | less than or equal to |
| >= | greater than or equal to |
例
all b: Bag | #b.marbles =< 3 は，どのバッグにも大理石が 3 個以下入っている，ということ．
ちまちま更新します．
コメント