前回 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: