Alloy で形式手法を始めてみた！～シグネチャ編～

Signature とは？
参考
過去の投稿

Signature とは？

Signature（シグネチャ）はオブジェクト指向プログラミングでいうオブジェクトに相当します．人や状態，DB のレコード，ファイルなど，モノを表すための基本要素です．

例えば，以下のコードを表示してみましょう．

sig A {}

sigA

パラパラとめくると，A というインスタンスがいくつか生成されていることが確認できます．

sig でシグネチャの宣言を，A がシグネチャの名前を表しています．{} の中に色々な関係式（フィールド）を付け加えることで，A を特徴づけていきます．

sig Father {}
sig Mother {}
sig Child {
    father: Father
    , mother: Mother
}

Child の中に，father: Father と mother: Mother が追加されました．
これは，「Child のインスタンスは father (resp., mother) という Father (resp., Mother) 型のインスタンスをもつ」ということを表しています．

このコードを Execute し，パラパラと Next で例を見ていくと，次のような例が出てきます．

parents

Child に対して，Father1 と Mother がぶら下がっています．他にもいろいろな例が挙がっているでしょう．

例えば，以下の図は兄弟を表しているはずです．

brothers

下の図は奥さんが再婚したんでしょうね．

harachigai

このように，モノを定義するのがシグネチャです．

フィールド

プログラミングでいうフィールドとほぼ同じような意味合いのようです．
カンマ区切りで記述します．

フィールドに対する記述方法を見ていきましょう．

フィールドの重複度

例えば，最近導入が進みつつあるマイナンバーについて考えてみましょう．

sig MyNumber {}
sig Person {
    number: one MyNumber // number: MyNumber としても同じ
}

いくつか例を見ていくと，下の図のように，「2 人に同じマイナンバーが割り当てられている」状態が出てきます．

マイナンバー重複

マイナンバーに重複はあり得ませんから，このような例が生じてはいけないはずです．
そこで，重複度を指定するような構文が必要になります．

いろいろな例で，重複度について調べてみます．

one

one は「ちょうど一つ」を表します． one はデフォルトなので，省略しても OK です．

sig MyNumber {}
sig Person {
    number: one MyNumber // number: MyNumber としても同じ
}

lone

lone は「高々一つ」を表します．つまり，one の場合に加えて 0 個の場合も含まれます．

sig Directory {
    parent: lone Directory
}

lone

some

some は「少なくとも一つ」を表します．つまり one の場合に加えて， 2 個以上の場合も含まれます．

sig Window {}
sig House {
    window: some Window
}

some

家に窓は少なくとも一個はありますよね？

disj

以下のように，disj を型の部分につけることで，「互いに異なる，重複がない」という重複度を指定することができます．

sig MyNumber {}
sig Person {
    number: disj MyNumber
}

disj

これで，異なる人には異なるマイナンバーが（つまり重複なく）振られました．

数学でも，交差のない集合は disjoint だとか表現しますよね．

set

set は名前の通り集合を表します．つまり，0 個以上の複数のインスタンスがぶら下がります．

sig Directory {
    children: set Directory
}

set

seq

配列（* ここは公式ページを理解できず，誤った情報が含まれる場合があります）です．
seq は 0 個以上の要素を持つ配列を表します．

sig Book {}
sig Person {
    books: seq Book
}

seq

なお，seq には色々なヘルパ関数が用意されています．以下は，公式サイトの和訳です．
s は seq だとします．

ヘルパ関数	内容
#s	s の要素数を返す
s.elems	s の要素からなる集合を返す
s.first	#s > 0 なら初めの要素を，そうでなければ空集合を返す
s.last	#s > 0 なら最後の要素を，そうでなければ空集合を返す
s.rest	#s > 1 なら，最初の要素を取り除いた配列を，そうでなければ空集合を返す
s.butlast	#s > 1 なら，最後の要素を取り除いた配列を，そうでなければ空集合を返す
s.isEmpty	#s == 0 なら true を返す
s.hasDups	配列要素に重複があれば true を返す (duplication)
s.inds	#s > 0 なら集合 {0, 1, ..., #s - 1} を，そうでなければ空集合を返す
s.lastIdx	#s > 0 なら #s - 1 を，そうでなければ空集合を返す
s.afterLastIdx	#s として利用可能な最大長を超えない場合は #s を，そうでない場合は空集合を返す
s.idxOf[x]	x が s に存在しなければ空集合を，存在すれば値が x である最も小さい番号を返す
s.lastIdxOf[x]	x が s に存在しなければ空集合を，存在すれば値が x である最も大きい番号を返す
s.indsOf[x]	x が s に存在しなければ空集合を，存在すれば値が x である番号全体の集合を返す
s.add[x]	#s として利用可能な最大長を超えない場合は x を s の末尾に追加し s を返す
s.setAt[i, x]	0 <= i <= #s - 1 であれば i 番目の要素を x に置き換え，そうでなければ何もしない？
s.insert[i, x]	0 <= i <= #s - 1 であれば i 番目に x を差し込み，そうでなければ何もしない？なお，#s がすでに最大長に達していたら，最後の要素は削除される．
s.delete[i]	0 <= i なら i 番目の要素を削除する．そうでなければ何もしない？
s.append[t]	s の末尾に t を連結する．もし長すぎれば不足分が落とされる．
s.subseq[from. to]	from から to までの部分列を返す．配列の範囲外が指定されたら，空集合を返す（from が -1 や，to が #s の場合など）

※配列については，うまく理解ができなかったところに"？"マークを付けています．

シグネチャの重複度

シグネチャにも重複度の設定が可能です．
デフォルトでは，set と同等になります．

set は，モデルを表示したときに 0 個以上表示されるということです．
one は，モデルを表示したときに 1 個だけ表示されるということです．
some は，モデルを表示したときに 1 個以上表示されるということです．
lone は，モデルを表示したときに 1 個以下表示されるということです．

one, some, lone の例を 2 個表示させてみましょう．

one sig OneSig {}
some sig SomeSig {}
lone sig LoneSig {}

onesome

↑ は，one と some のインスタンスが 1 個ずつ表示されていて，
lone のインスタンスは表示されていません．

onesomelone

↑ は，one と lone のインスタンスが 1 個ずつ，
some のインスタンスが複数個表示されています．

サブタイプ

ざっくりいうと，型の継承関係のようなものです．

in

サブタイプの基本形です．

sig Integer {}

sig Non-Negative in Integer {}
sig Non-Positive in Integer {}
// Non-Negative かつ Non-Positive であるような Integer のインスタンスの存在も許される．

+

和です．親は複数かもしれないし，単一かもしれないです．

sig Mathematics, Information {}

sig MachineLearning in Mathematics + Information {}

extends

in とほぼ同じ使い方をしますが，違いは，親のインスタンスが複数の型を許すかどうかです．
extends の場合，複数の型は許されません．

sig Person {}

sig Man extends Person {}
sig Woman extends Person {}
// Person は Man か Woman のどちらか一方であるか，またはそれ以外である．
// Man かつ Woman にはなりえない．

さて，以下の場合はどのようなパターンが許されるでしょうか？

sig Person {}
sig Sleeping in Person {}

sig Man extends Person {}
sig Woman extends Person{}

この場合，Person のインスタンスは (i) Sleeping 型かつ Man 型; (ii) Sleeping 型かつ Woman 型; (iii) Sleeping 型でない Man 型; (iv) Sleeping 型でない Woman 型; (v) Man 型でも Woman 型でもない Sleeping 型; (vi) どれでもない型，の 6 種類のうちのどれかになります．

abstract

継承される側を abstract にしておくと，そのシグネチャのインスタンスは extends したシグネチャのどれかの型を持ちます．

abstract sig Person {}

sig Man extends Person {}
sig Woman extends Person {}
sig Other extends Person {}
// Person のインスタンスは，Man か Woman か Other のどれかの型をもつ．
// しかも，このどれかに一致する．

誰からも extends されない abstract なシグネチャは無視されるようです．

かなり長くなったので，一旦ここまでで区切ろうと思います．
フィールドの説明では，多項関係の説明を一切行っていないので，次回はそこを書いていこうと思います．

参考

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

Alloy Documentation

過去の投稿

Alloy で形式手法を始めてみた！～導入編～

では！