Alloy は代表的な形式的仕様記述言語の一つです．
- 形式的仕様記述言語とは，仕様を自然言語ではなく，論理式のような数学的に厳密に意味が定義された形式で記述する方法で，
+ 形式的仕様記述言語とは，仕様を自然言語ではなく，論理式や等式のような数学的に厳密に意味が定義された形式で記述する方法で，
- 以下の仕様記述では名前の集合を Name，アドレスの集合を Addr，アドレス帳の集合を Book で表しています．
+ 以下の仕様記述では名前の集合を Name，アドレスの集合を Addr，アドレス帳の集合を Book で表します．
Book は，2つのフィールド owner と addr を持っています．Alloy におけるフィールドは，インスタンスの内部構造を表すものではなく，基本的に2つの集合の要素間の関係を表しています．たとえば Book の owner フィールドは，Book の各要素に Name の要素を対応づける関係を表しています．フィールドの詳細な意味については後ほど説明します．
Alloy では，操作も関係で表されます．たとえば add 操作は，連絡先を登録する前の Book の状態と，登録した後の Book の状態の間の関係を表していると考えます．
より具体的には Book の状態 b，登録後の Book の状態 b'，登録する連絡先の名前 n，登録するアドレス a の間に成り立つ述語として定義されています．
- 述語の本体は 1つ以上の式によって構成されます．これらの式は変数間に成り立つ制約関係を表しているため記述順は関係ありません．たとえば，b'.owner = b.owner は，add 操作前の Book の owner と，add 操作後の Book の owner が同じであることを示しています．
- b'.addr = b.addr + n -> a は，add 操作前の Book の addr （Book の各インスタンスが持つ，名前とアドレスの対応表）に対して，名前 n とアドレス a の対応を付け足したものが，add 操作後の Book の addr になることを示しています．これらの式は順番を入れ替えても意味は変わりません．
+ 述語の本体は 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 の対応を追加した関係を表しています．）
実行は，execute という引数を持たない述語が呼び出されます．