前回 http://d.hatena.ne.jp/propella/20090527/p1 Alloy をちょっとだけ触ってみました。大体使い方が分かった所で、もう一度最初からチュートリアルをやってみます。実は最初読んでいたファイルシステムのチュートリアルはあまり出来が良くなくて http://alloy.mit.edu/alloy4/tutorial/ にあるスライドの方が良いそうです。
サンプルとして、次のようなプログラムを Arroy に入力します。多分「人の上には人がいる、人の下にも人がいる」の証明だと思います。
// 床がある sig Platform {} // 人の上に床があって、人の下にも床がある sig Man {ceiling, floor: Platform} // Above[m,n] とは、m の下の床と n の上の床が同じ事。 pred Above [m, n: Man] {m.floor = n.ceiling} // 全ての人の上には誰かいる fact {all m: Man | some n: Man | Above[n,m] } // 問題: 全ての人の下にも誰かいる assert BelowToo { all m: Man | some n: Man | Above [m,n] } // 二つ以下の床や人がいたとき、この BelowToo が正しいか調べる。 check BelowToo for 2
それから Execute ボタンを押すと、グラフィカルに反例が表示されて正しくないと分かります。そこで Evaluator ボタンを押すと、この反例について色々 REPL できます。ここで使う事の出来る変数名を知るには univ という定数を使います。定数には次のような物があります。
- none : 空集合
- univ : 全体集合
- iden : 一意関係
univ の中から Man を一つ表示してみます。
univ - Man
{-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7,
Man$0, Man$1, Platform$0, Platform$1}
Man$0
{Man$0}
Man$0 は自動生成された Man の要素です。奇妙な事に、Man$0 とやると Man$0 が一つ入った集合 {Man$0} が表示されます。もしかして要素と集合を区別しないのかもしれません。集合演算の例はこんな感じです。Man の補集合を求めています。
univ - Man
{-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7,
Platform$0, Platform$1}
なぜ -1 や -2 といった数字が出てくるのかわかりませんでした。もうちょっと複雑な例も書きます。some というのは存在を表す量指定子で、| の右に式を書きます。p in Platform という時、Platform が p を含んでいれば true です。
some m:Man | m.floor in Platfom
true
ここまで道具がそろった所で、この例の文法を詳しく見てみます。
sig Platform {}
sig は新しい集合を定義します。どんな要素があるかは気にしないで、集合の名前だけを書きます。
sig Man {ceiling, floor: Platform, between: Man -> Platform}
中括弧の中には関係を書きます。関係にアクセスするには Man.floor のようにドット表記を使います(この場合、全ての Man の floor の集合が返ります)。Haskell 風に書くと次のようになります。
ceiling, floor :: Man -> Platform
「関係」の文法は構造体のようになっていて、まるで要素へのアクセスのように振る舞います。しかし意味としては関係とは二つの要素の組み合わせの事で、クロス積とも呼びます。たとえば、「Man$1 の floor は Platform$0 である」という関係は、「floor という関係は Man$1 -> Platform$0 を含んでいる」と言い換える事も出来ます。プログラム中での書き方も二通りあります。
Man$1.floor = Platform$0 // Man$0 の floor は Platform$0 である true Man$1 -> Platform$0 in floor // floor は Man$1 -> Platform$0 という関係を含む true
値域にクロス積 -> を書くと引き数がある関数っぽくなります。
sig Man {between: Man -> Platform}
Man.between[Man] のようにしてアクセスします。このへんオブジェクト指向言語にあわせようとして嫌な文法になってると思います。
pred Above [m, n: Man] { m.floor = n.ceiling }
pred は新しい述語を定義します。式の中に Above[m,n] と書くと、それは m.floor = n.ceiling と書いたのと同じ事になります。ちなみに、大文字小文字の区別は単に慣用的に決まっているようです。
fact { all m: Man | some n: Man | Above[n,m] }
fact は要素間の制約を表します。
assert BelowToo { all m: Man | some n: Man | Above [m,n] }
assert は fact と似ていますが、モデルが従うべき制約です。
check BelowToo for 2
最後にテストする制約を書きます。for の後ろに書いた数字の分だけ要素が生されて反例を探します。
今日はここまで。正直文法はかなりしんどいです。prolog や Coq に比べて難しい感じがするのは、なんか無理矢理 Java っぽい文法にしてるからじゃ無いだろうか。。。
