【Alloyの説明】

本実験で用いる Alloy の概要について説明します．
現時点では本ページの内容を完全に理解する必要はありません．課題に取り組む際に必要に応じて本ページを参照しながら進めるようにください．

Alloy とは？

Alloy は代表的な形式的仕様記述言語の一つです．
Alloy は形式的仕様記述言語としては比較的表現能力が高いため，完全に網羅的な解析はできませんが，実用性を大きく損なわない範囲で網羅性を制限した解析を行うことができるといった特長があります．
本実験では，Alloy による仕様記述と仕様の仮想実行に着目していきます．そのため，Alloy による仕様の解析は行いません．また，Alloy のツールをPCにダウンロードして操作していただく必要もありません．

Alloyによる仕様記述:

Alloy では，集合と関係を使って仕様を記述していきます．また，その記述は宣言的な形式で行われます．
宣言的記述の対義語は手続き的記述です．我々が通常用いるプログラミング言語では手続き的な記述が用いられています．手続き的な記述ではプログラムは基本的に一番上の行から順番に一行ずつ, 記述された順に実行されていきます．
一方宣言的な記述では，記述の順序は関係ありません．すべての行が同時に成り立っていると考えます．連立方程式を考えてみると解りやすいと思います．連立方程式では，すべての式が同時に成り立っているため，式の記述順に関係なく同じ解が得られます．そのため，宣言的記述には基本的に時間の経過が存在しません．実行の初期状態から最終状態までのすべての状態が同時に存在していることになります．これは DTRAM の記述にはなかった性質です．
Alloy の概念的な説明はこれくらいにして，具体的に Alloy の記述を見ていきましょう．

Alloy による仕様記述の例

例題仕様:

DTRAM のときに記述したアドレス帳と同じ仕様を，今度は Alloy を用いて記述することを考えます．アドレス帳の仕様を再掲します．

Alloy による記述例:

以下の仕様記述では名前の集合を Name，アドレスの集合を Addr，アドレス帳の集合を Book で表します．
sig でこれらの集合を宣言しています．ここで集合はクラス，集合に属している各要素はインスタンスに相当すると考えてください．ただし，Alloy は宣言型の言語なので，DTRAM とは異なりインスタンスの状態を変えることができません．状態の変更前と変更後でインスタンスが別々になると考えてください．
Book は，2つのフィールド owner と addr を持っています．Alloy におけるフィールドは，インスタンスの内部構造を表すものではなく，基本的に2つの集合の要素間の関係を表しています．たとえば Book の owner フィールドは，Book の各要素に Name の要素を対応づける関係を表しています．フィールドの詳細な意味については後ほど説明します．

Alloy では，操作も関係で表されます．たとえば add 操作は，連絡先を登録する前の Book の状態と，登録した後の Book の状態の間の関係を表していると考えます．
より具体的には pred を用いて，登録前の Book の状態 b，登録後の Book の状態 b'，登録する連絡先の名前 n，登録するアドレス a の間に成り立つ述語として定義されています．
述語の本体は 1つ以上の式によって構成されます．これらの式は変数間に成り立つ制約関係を表しているため記述順は関係ありません．
たとえば，b'.owner = b.owner は，add 操作前の Book の owner（b.owner）と，add 操作後の Book の owner（b'.owner）が同じであることを示しています．
b'.addr = b.addr + n -> a は，add 操作前の Book の addr （Book の各インスタンスが持つ，名前とアドレスの対応表）に対して，名前 n とアドレス a の対応を付け足したものが，add 操作後の Book の addr になることを示しています．これらの式は順番を入れ替えても意味は変わりません．（なお x + y -> z は，関係 x に y と z の対応を追加した関係を表しています．）

Alloy では実行は，run で指定された述語を呼び出すことによってなされます．ここでは，execute という引数を持たない述語が呼び出されます．
execute の本体については，いくつか説明が必要です．
まず，この execute 本体は，1つの論理式で構成されています．一見，4つの論理式が列挙されているように思いますが，全体として論立式は1つです．
ポイントは存在限量子 some です．some は，後ろに並んだ変数の値のある組み合わせにおいて，| の後ろに記載された論理式が成り立つということを示しています．似たようなものに all と no があります． all は，後ろに並んだ変数の値の任意の組み合わせにおいて，| の後ろの論理式が成り立つということを，no は，後ろに並んだ変数の値のどんな組み合わせにおいても，| の後ろの論理式が成り立たないことを示します．
ここでは，b0, b1, b2, b3 という Book のインスタンスのある組み合わせにおいて（disj がついているのでこれら4つのインスタンスは互いに異なります），また，n0, n1, n2 という Name の互いに異なる3つのインスタンスのある組み合わせについて，さらに，a0, a1 という Addr の互いに異ならなくてもよいインスタンスのある組み合わせについて，| 以下の論理式が成り立っていることを示しています．| 以下の論理式は { と } で囲まれている4つの論理式をまとめたもの，すなわち4つの論理式が同時に成り立っていることを示す1つの論理式になります．
この4つの論理式も同時に成り立っているので，記述の順序を変えても意味は変わらないのですが，しかし，実行において最初に init 操作が呼ばれて，次に add 操作が2回呼ばれ，最後に del 操作が呼ばれることを表しています．詳細は後ほど説明しますが，これには，Book の4つのインスタンス（b0, b1, b2, b3）が関係しています．まず初期化の操作 init に関わるのは b0 です．次に，最初の add 操作は，b0 を b1 に変更します．さらに，次の add 操作は，b1 を b2 に，最後の del 操作は b2 を b3 に変更します．このようにインスタンス（の状態）を受け渡すことによって，実行が進んでいくことを表すことができます．

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

pred init[b: Book, n: Name] {
	b.owner = n
	no b.addr
}

pred add[b, b': Book, n: Name, a: Addr] {
	b'.owner = b.owner
	b'.addr = b.addr + n -> a
}

pred del[b, b': Book, n: Name] {
	b'.owner = b.owner
	b'.addr = b.addr - n -> b.addr[n]
}

pred execute[] {
	some disj b0, b1, b2, b3: Book, disj n0, n1, n2: Name, a0, a1: Addr | {
		init[b0, n0]
		add[b0, b1, n1, a0]
		add[b1, b2, n2, a1]
		del[b2, b3, n1]
	}
}

run execute for 2 but 4 Book, 3 Name

実行の可視化:

Alloy でも実行を可視化することができます．DTRAM とは異なり，Alloy では上の仕様記述内の run による実行を一枚の図で可視化します（以下の図参照）．

可視化では実行時に生成される1つのインスタンスが，1つの矩形で表されます．たとえば，図の上部に並んでいる4つの矩形は，execute 述語内で宣言されている4つの変数，b0, b1, b2, b3が参照する Book の4つのインスタンスに対応しています．矩形内部には，そのインスタンスが所属しているクラス名とインスタンスのIDが記されています．また，括弧の中にはそのインスタンスを参照している変数名が記されています．
Book のインスタンスは4つありますが，これは手続き型プログラムで考えると Book の1つのインスタンスの状態が3回変わったことに相当しています． Book の初期化後の状態が Book3，最初の add 操作後の状態が Book2，次の add 操作後の状態が Book1，最後の del 操作後の状態が Book0 に当たります． Alloy は宣言型言語なので，これらは順番に生成されるというわけではなく，最初から同時に存在しています．

Book の owner フィールドは，Book の要素と，Name の要素の間の関係として定義されます． Book のインスタンスを1つ指定すれば，ownerフィールドを使って b.owner のように Name のインスタンスを1つ取ってくることができるためです．この図では，Book のどのインスタンスも同じ Name のインスタンスを参照しています．これは，この実行における Book の状態の変化では，owner が変わらないためです．