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

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

ここでは，シグネチャ編で話さなかった，以下の内容を話します．

  • "継承" したときに，継承元のフィールドはどうなるか？
  • Enum とはなにか？
  • 特殊な集合
    • iden
    • univ
    • none

なので，シグネチャ編の補足という形の記事になります．

継承とフィールドの関係

結論から言うと，abstract sig や sig がフィールドを持つとき，それを extends や in で継承した
シグネチャにもそのフィールドが引き継がれます．

in の例

sig LeftButton {}
sig RightButton {}
sig Mouse {
    leftButton: one LeftButton,
    rightButton: one RightButton,
}

sig Wheel {}

sig UsefulMouse in Mouse {
    wheel: one Wheel,
}

/* UsefulMouse, Mouse が両方表示されるおまじない */
fact fct {
    #UsefulMouse = 1 and #Mouse >= 2
}

UsefulMouse が Mouse を継承しています．これを実行すると以下の例が表示されます．

in

二つのマウスがボタンを共有してるのはおかしいですが，確かに UsefulMouse にも LeftButton, RightButton が属していますね．

abstract - extends の例

sig LeftButton {}
sig RightButton {}
abstract sig Mouse {
    leftButton: one LeftButton,
    rightButton: one RightButton,
}

sig Wheel {}

sig UsefulMouse extends Mouse {
    wheel: one Wheel,
}

sig SideButtons {}

sig ExpensiveMouse extends Mouse {
    wheel: one Wheel,
    sideButtons: one SideButtons,
}

/* UsefulMouse, ExpensiveMouse が両方表示されるおまじない */
fact fct {
    #UsefulMouse = 1 and #ExpensiveMouse = 1
}

この場合も，以下の通り．

useful_and_expensive

Enum とはなにか？

Enum は予め定めておいた要素しか持たない集合を表します．

enum Buttons {
    LeftButton, RightButton, Wheel
}

順序関係も保持し，LeftButton, RightButton, Wheel の順に要素を持ちます．暗に ordering というモジュールをインポートしています．モジュールについてはいずれ説明します．

特殊な集合

予め Alloy で予約された集合があります．

A = {a1, a2, a3} ，B = {b1, b2} とします．

iden

iden は恒等関係を表します．
つまり，iden = {(a1, a1), (a2, a2), (a3, a3), (b1, b1), (b2, b2)} です．

univ

univ は全体集合を表します．
つまり，univ = {a1, a2, a3, b1, b2} です．

none

none は空集合を表します．

最後に

次回は，Integer やその演算について書こうかなと思います．数値の計算は，集合の演算をしているのか数値の演算をしているかわかりにくくなる箇所なので，具体例を交えながらじっくり説明しようかと思います．

参考

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

過去の投稿

では！

コメント