03 May, 2010

[Alloy][FM] Sample code: Addressbook

 [Coq][FM] Fomal Methods Forum #4でのAlloyチュートリアルの話。

 まず Alloy4 を各自インストールしておくのは前提。但し、JARファイル1つなので、JRE (Java5以上) が入っているコンピュータならば起動は難しくありません。

 表示されるWindowの左側入力欄に下記を打ち込みます。

sig Name, Addr {}
sig Book {
addr: Name -> lone Addr
}

 sigというのは普通のOO言語のクラス定義の様なもの --- なんですが、Alloy はOOなプログラミング言語ではないのでOOとのアナロジーは時に誤解を与えるかも。どちらかというと、RDBMSに Name, Addr という表を作ったと考えるといいかも。実際、Alloy は関係代数に基づいていますし。
 OO でいうところのインスタンスはAlloyではatomと言います。Alloyでインスタンスというのは、全てのatomから構成されるモデル(モデルの中には求める反例とかも含まれます)のことを指します。用語は間違わない様に。
 また、. (ドット演算子) もOO言語の属性やメソッドを指す様に勘違いしますが、join演算子で、RDBのjoinみたいな振る舞いをします。
 Bookのatomを仮に B0, B1 と書くと、Book は {(B0), (B1)} という集合です。( () はタプル、{}は集合を表す。)

 lone は 0 or 1 個を表す数量限定子です。他にも all (全ての)、some (1個以上)、one (1個)、no (0個) があります。lone Addr は、関数型言語的には Option Addrのようなものです。
 addr は Book の属性みたいに見えますが、これも関数型言語的には addr : Book -> Name -> Option Addr -> Prop みたいに考えると良いです。addr は (Book, Name, Addr) のタプル型の元の集合、例えば{(B0,N0,D0), (B1,N1,D1)}として表現されます。 (関係 R : R x y は (X,Y) の部分集合として表現出来る)
 Book = {(B0),(B1)} であると、ドットはjoin演算子なので(テンソルとかの添字の縮約の如く)ジョイン演算をします。Bookとaddrの共通のB0を見て(B0).(B0,N0,D1)=(N0,D0)の様に計算して、b=B0ならば、b.addr={(N0,D0)}, Book.addr={(N0,D0),(N1,D1)} となります。

 この時点で sig Book {...} の下に

pred show[] {}
run show for 3
と書いて Execute のボタンを押します。
 右側に Instance found と出るので Instance のリンクを押すと、atom 間の関係を示すダイヤグラムが表示されます。nextを押すと別のインスタンスが表示されます。
 for 3 と書いたので各 sig 毎に 3 atom づつです。

 次にモデルの性質をテストする事を考えます。addr を追加して削除すると元に戻る、という性質が成り立つ事をモデル検査で確認(=反例が見つからない事を確認)します。
 まず追加と削除を表す述語を定義します。述語なので戻り値は真偽値を返します。

pred add[disj b,b':Book, n:Name, a:Addr] {
b'.addr = b.addr + (n -> a)
}
pred del[disj b,b':Book, n:Name] {
b'.addr = b.addr - (n -> Addr)
}
 Alloyは手続き型言語ではないので、b'addrに何か破壊的代入が行われる事は無く、単にbとb'の間の関係を示しているだけです。disjはbとb'とが別atomであるという意味です。

 次いでテストしたい性質を書きます。

assert delUndoesAdd {
all b,b',b'':Book, n:Name, a:Addr |
add[b,b',n,a] and del[b',b'',n] implies b.addr = b''.addr
}
check delUndoesAdd for 5
 |はsuch thatみたいな意味、and, implisは論理演算の記号です。

 これを追加してexecuteすると「何故か」counterexampleが見つかったと表示されます。counterexampleをじっと眺めると、bとb'が同じBookであることが判ります。
 これは元々 b に (n -> a) が含まれていた場合、b, b' が同じになるからです。(集合に既にある要素を加えても同じ)
 assertの中身を

no n.(b.addr) and add[b,b',n,a] and del[b',b'',n] implies b.addr = b''.addr
に修正するとconterexampleが無くなります。

No comments: