Alloy で形式手法を始めてみた！～集合の演算と数値編～

Alloy で形式手法を始めてみた！～集合の演算と数値編～

ここでは，集合に対する演算と数値の扱いについて説明します．

集合の演算

集合の演算には， +, -, &, -> の四つがあります．

+

+ は和集合を表します．

A = {a1, a2}, B= {a1, b1} とすると， A + B = {a1, a2, b1} となります．

-

- は差集合を表します．

A = {a1, a2}, B= {a1, b1} とすると， A - B = {a2} となります．

&

& は共通部分を表します．

A = {a1, a2}, B= {a1, b1} とすると， A - B = {a1} となります．

->

-> は直積を表します．

A = {a1, a2}, B= {a1, b1} とすると， A -> B = {a1 -> a1, a1 -> b1, a2 -> a1, a2 -> b1} となります．

（イメージとしては，(a1, a1), (a1, b1), (a2, a1), (a2, b1) と同じです．このあたりは，Alloy が全てのものを関係式 (n 項関係)として認識するという思想に基づいているということを理解しないと難しいです．改めてどこかで説明します．が，このあとの数値計算でもう一度出てきます．）

数値

定数としての数値は，デフォルトでは -8 から 7 まで（4 ビット）が利用可能です．スコープを変更することで，それ以上の数値を表現することも可能です ( run {} for 6 Int とすれば，6 ビット分の数値を扱うことが可能です)．

数値の例

シグネチャ S に対し，#S でその要素数を表します．

sig A {}

one sig B{
    num: one Int
}

fact BNum {
    B.num = #A
}

card

A が三つあるので，B.num は 3 になります．

数値の演算

plus[a, b]

足し算です．plus[1, 2] は 3 を表しますし，plus[1, 1] は 2 を表します．

以下を実行すると，A.num は 1 になります．

sig A {
  num: one Int
}
fact numOp {
  plus[1, 1] = 2 implies A.num = 1 else A.num = 2 // A implies B else C は if 文です
}

plus

1.plus[2] のような表記も可能です．

minus[a, b]

引き算です．minus[1, 2] は -1 を表しますし，minus[2, 1] は 1 を表します．

以下を実行すると，A.num は 1 になります．

sig A {
  num: one Int
}

fact numOp {
  minus[1, 1] = 0 implies A.num = 1 else A.num = 2
}

1.minus[2] のような表記も可能です．

画像は省略します．

mul[a, b]

掛け算です．mul[1, 2] は 2 を表しますし，mul[2, 3] は 6 を表します．

以下を実行すると，A.num は 6 になります．

sig A {
  num: one Int
}

fact numOp {
  A.num = mul[2, 3]
}

mul

2.mul[3] のような表記も可能です．

div[a, b]

割り算の商です．div[3, 2] は 1 を表しますし，div[2, 4] は 0 を表します．

以下を実行すると，A.num は 1 になります．

sig A {
    num: one Int
}

fact numOp {
    A.num = div[3, 2]
}

div

3.div[2] のような表記も可能です．

rem[a, b]

割り算の余りです．rem[3, 2] は 1 を表しますし，div[2, 4] は 2 を表します．

以下を実行すると，A.num は 2 になります．

sig A {
    num: one Int
}

fact numOp {
    A.num = rem[2, 4]
}

rem

2.rem[4] のような表記も可能です．

sum[set Int]

数値の集合に対する総和です．

以下を実行すると，A.num が B.nums の総和になっています．

one sig A {
    num: one Int
}

one sig B {
    nums: some Int
}

fact numOp {
    A.num = sum[B.nums]
}

sum

数値の比較演算

数値の大小関係やイコール関係を比較することが可能です．

=, >, <, =<, >= の記号を利用します．通常，プログラム言語では小なりイコールを <=と書くことが多いですが，含意の矢印と混同される可能性があるため Alloy では =< と記述します．

演算の注意点

数値の計算をする際に，plus, minus, mul, div, rem を使わない場合，意図しない挙動をすることがあります．

one sig A, B {
    num: one Int
}

fact numOp {
    A.num = (1 + 3).plus[0] // {1} + {3} = {1, 3}
    B.num = (1 + 1).plus[0] // {1} + {1} = {1}
}

plus2

plus などの四則演算，及び大小関係 (>= と =<)を使う場合，Int 型の値の集合に暗に sum 演算が行われます．
そのため，1 + 3 は 1 と 3 の和として計算されますが，1 + 1 は {1} なので sum を取ると 1 になります．
これを避けるため，以下のように計算すべきです．

one sig A, B, C, D {
    num: one Int
}

one sig E {
    nums: some Int
}

fact numOp {
    A.num = plus[1, 3]  // 1 + 3 = 4
    B.num = plus[1, 1]  // 1 + 1 = 2
    C.num = sum[E.nums] // E.nums の和
    (1 + 1) = 2 implies D.num = 1 else D.num = 2    // {1} + {1} = {1} != {2}
}

plus3

一方で，上で述べたように，大小関係については，暗に sum 演算が行われます．

one sig A, B, C {
    num: one Int
}

fact numCondition {
    // イコールでは暗黙の sum 演算は行われない
    (1 + 1) = 2 implies A.num = 1 else A.num = 2    // {1} != {2} なので false

    // 大小関係では，暗黙の sum 演算が行われる
    (1 + 1) >= 2 implies B.num = 1 else B.num = 2   // sum[{1}] = 1 < 2 なので false
    (1 + 2) >= 3 implies C.num = 1 else C.num = 2   // sum[{1, 2}] = 3 >= 3 なのでtrue
}

plus_geqleq

最後に

次回は，集合の演算についてもっと深く考えようと思います．ドットジョインや推移閉包などを紹介する予定です．

参考

非公式ドキュメントですが，基本的にはここを参照しています．

過去の投稿

では！

コメント