AlloyのSignature

集合を定義する

code:Alloy

sig A {}

sig B, C {}

code:alloy

sig A, B {}

以下も、AとBは共通部分を持たない

code:Alloy

sig C {}

sig A, B extends C {}

code:Alloy

abstract sig C {}

sig A, B extends C {}

subsetを作って初めて差が出る

code:alloy

sig C {}

sig A, B in C {}

複数の集合の和集合の部分集合としても定義できる

code:alloy

sig C in A + B {}

集合演算子

和集合

共通部分

-

差集合

in

部分集合

=

イコール

fieldは関係の導入

code:alloy

sig A {f: e}

とかけば、

code:alloy

f in A -> e

というfactが存在するのと同じ意味

以下2つは等価

code:alloy

sig A {f: e}

sig A {f: one e}

fieldのoverloadについて

読み飛ばした

seq

singleton

code:alloy

one sig A {}

一つの要素のみを持つ集合A