形式仕様記述Alloyを試してみる

試してみるよ。
とりあえず商品をまとめたセット商品についての仕様を書いてみる。
まず商品の定義

module exec/shohin

sig Shohin{}
pred show{
}
run show

sigはJavaとかのclassだと思えばだいたいOK。
なんか商品がみっつ出た。

じゃあ、セット商品を定義してみる。

sig SetShohin{
  bundle: set Shohin
}

おー、同じ商品が３つのセットに含まれてしまった。Alloyさんイヤらしいとこついてくる。

ということで、ひとつの商品は多くてもひとつのセットにしか含まれない、っていう制約を加えます。

fact {
  all s: Shohin | lone bundle.s
}

書き下ろすと「すべての商品について、商品をbundleとして持つのはたかだか１つ」になるんですけど、この、フィールドを左に書く書き方は通常のプログラムから考えると違和感あります。

で、まあ同じ商品が複数のセットに含まれることはなくなったんだけど、商品含んでないセットもあります。

セット商品のbundleにsetを指定しているので、bundleが0でもいいってことになってしまってました。setじゃなくてsomeにすれば、必ずなにか商品が含まれるはず。
あと、ついでに、システム的にはSetShohinもShohinの一種として扱いたいので、extendsの指定もします。これはclassのextendsと同じ。

sig SetShohin extends Shohin{
  bundle: some Shohin
}

そうすると、自分自身をもつセットができちゃいました。

ということで、自分自身をbundleにもつセットはないよ、っていう制約を加えます。

fact {
  all s: Shohin | lone bundle.s
  no ss: SetShohin |  ss in ss.bundle
}

そしたら今度は循環参照された ＞＜

さっきの制約に「^」を加えて、bundleをたどっていっても自分自身にはたどりつかないよっていう制約にします。

  no ss: SetShohin |  ss in ss.^bundle

これで循環参照もなくなりました。でも、そもそもセットにセット含んじゃだめじゃない？

ということで、セットにセットは含まないという制約にします。

fact {
  all s: Shohin | lone bundle.s
  all sp: SetShohin  | no ss: SetShohin | ss in sp.bundle
}

でも、これだと、セットとセットに含まれる商品はわけて定義したほうがよさそう。
ということで、SimpleShohinというのを定義して、セットに含むのはSimpleShohinだけにしました。

sig Shohin{}
sig SimpleShohin extends Shohin{}
sig SetShohin extends Shohin{
  bundle: some SimpleShohin
}
fact {
  all s: Shohin | lone bundle.s
}

これでセットに含まれるのはSimpleShohinだけになったけど、Shohinも単独で存在してる。

もうここではSetShohinかSimpleShohinしか存在しないようにしたい。
ということでShohinにはabstractになってもらいます。

abstract sig Shohin{}

これで問題ありそうなインスタンスは生成されなくなりました。
最終的な仕様はこんな感じ。

module exec/shohin

abstract sig Shohin{}
sig SimpleShohin extends Shohin{}
sig SetShohin extends Shohin{
  bundle: some SimpleShohin
}
fact {
  all s: Shohin | lone bundle.s
}
pred show{
}
run show

参考にしたのはこの本。

抽象によるソフトウェア設計−Alloyではじめる形式手法−

うむ、なんか面白いんだけど、実際にどんな感じで役にたてれるかわかんない。
ただ、形式仕様記述のZ言語の本を見たときに持った絶望感みたいなのはなくて、ちょっとずつ試していけるので、形式手法を試すのにはとてもいいのかなーと思います。

あ、あけましておめでとうございました。今年もよろしゅう。