形式仕様記述Alloyで時系列の仕様を試してみる

先日は、静的な構造をAlloyで試してみました。
http://d.hatena.ne.jp/nowokay/20120101#1325434520

こんどは時系列での動きを試してみます。時系列の仕様を書くには、util/orderingを使って、変化があるものに結び付けます。
今回は、カートに商品を入れるっていう仕様を書いてみます。カートの時系列を追うってことで、カートをutil/orderingの派生にしてます。

module exec/cart
open util/ordering[カート]

sig 商品{}
sig カート{
  含む: set 商品
}

pred show{
}
run show

ここでは、カートに複数の商品が含める、という仕様を定義してます。各商品は１つしかないものとしますね。
Alloy4.1.10だと日本語モデル名使えなかったのだけど、Alloy4.2RC使ったら日本語問題なかったんで、いろいろ日本語使ってます。

さっそく性格わるいAlloyさんが同じ商品を複数のカートに含ませてます。でも、今回は、別のタイミングのカートをあらわしたりするので、とりあえずこれはそのまま置いておきます。

こんな感じで、二つのカートをc,c'として受け取って商品を「含む」に追加する記述を加えます。cが最初のカート状態でc'があとのカート状態ということにしてます。

pred 商品追加(c, c':カート, s:商品){
  c'.含む = c.含む + s
}

実行用の記述に加えます。

pred show{
  some c, c':カート, s:商品 {
    商品追加[c, c', s]
  }
}

こんな感じに。

show_cがshowでのc、show_c'がshowでのc'ということで、cからc'になって商品show_sが追加されてるのがわかります。

んでは、商品削除を追加してみます。showに加えたc''が、削除後の状態のつもり。

pred 商品削除(c, c':カート, s:商品){
  c'.含む = c.含む - s
}
pred show{
  some c, c',c'':カート, s:商品 {
    商品追加[c, c', s]
    商品削除[c', c'', s]
  }
}

んで実行したらこんな感じに。

カート２がshow_cとshow_c''に割り当てられてます。つまり、cとc''が同じ状態を指していて、これはカートに商品を追加して削除したんじゃなくて、商品を追加して追加前に戻ってる。まあ、実際削除することと追加前に戻ることは同じではあるんですけども。
Alloyさんは、最小のインスタンスで要求を実現しようとしてくれます。なので「いやそうじゃなくて〜」と追加の仕様を記述していく必要があるわけです。

ここで、cとc'とc''は全部違う状態ですよってことを表したいので、それぞれを!=で結べばいいんですけど、こういう場合はdisjをつけると別々のインスタンスであることがあらわせます。

pred show{
  some disj c, c',c'':カート, s:商品 {
    商品追加[c, c', s]
    商品削除[c', c'', s]
  }
}

でも、orderingも使ってることだし、商品追加と商品削除が別の操作だということを表したいので、こんな感じの制約にしてみます。それぞれで、c'はcの次の状態、ってことです。

pred 商品追加(c, c':カート, s:商品){
  c' = c.next
  c'.含む = c.含む + s
}
pred 商品削除(c, c':カート, s:商品){
  c' = c.next
  c'.含む = c.含む - s
}

そしたら、こんな感じに。んーなんかおかしい？

ちょっと、assertを追加して、追加して削除したら元に戻ることをcheckしてみます。

assert 追加して削除したら元に戻る{
  all c, c',c'':カート, s:商品 | {
    商品追加[c, c', s]
    商品削除[c', c'', s]
   } implies c.含む = c''.含む  
}
check 追加して削除したら元に戻る

ここで、反例をみつけるときに、いままでsomeだった限量子をallにしてます。

そしたら、Counterexampleが見つかったって言われた。

で、やっぱりさっきのと同じです。

最初に含まれてた商品を改めて追加したら、削除したときに最初の状態と違うってことです。

これはこれで正しい挙動だとすることもできます。つまり、この商品を追加して削除したら元の状態に戻ると想定したassertが悪かったとすることもできるわけです。
今回はassertどおりになってほしいとして、商品を追加するときには、追加する商品はあらかじめ含まれていないということにします。

pred 商品追加(c, c':カート, s:商品){
  c' = c.next
  not s in c.含む
  c'.含む = c.含む + s
}

そうすると、checkでは「No counterexample found.」となって、run showを実行するとこういうインスタンスが得られます。

カート0→カート1→カート2と時系列が進む中で、カート0→カート1で商品追加して商品が追加され、カート1→カート2で商品削除されて元の状態に戻っています。

ふむ、なんか仕様の確認に使える気がほんのりしてきました。
といいつつ、基本的にAlloy本の「ざっと一巡り」のところに書いてあるサンプルよりも簡単なことしかしてないんで、読んだときにわかればよかったのだけど。

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