[Alloy][FM] Sample code: Addressbook

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

　まず Alloy4 を各自インストールしておくのは前提。但し、JARファイル１つなので、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 (１個以上)、one (１個)、no (０個) があります。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が無くなります。