diff --git a/courseA/Alloy.html b/courseA/Alloy.html index b886006..283e0fa 100644 --- a/courseA/Alloy.html +++ b/courseA/Alloy.html @@ -29,7 +29,7 @@
以下の仕様記述では名前の集合を 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
になることを示しています.これらの式は順番を入れ替えても意味は変わりません.
+ b'.addr = b.addr + n -> a
は,add 操作前の Book
の addr
(Book
の各インスタンスが持つ,名前とアドレスの対応表)に対して,名前 n
とアドレス a
の対応を付け足したものが,add 操作後の Book
の addr
になることを示しています.これらの式は順番を入れ替えても意味は変わりません.
実行は,execute
という引数を持たない述語が呼び出されます.
@@ -85,7 +85,7 @@
ここでは,b0, b1, b2, b3
という Book
のインスタンスのある組み合わせにおいて(n0, n1, n2
という Name
の互いに異なる3つのインスタンスのある組み合わせについて,
さらに,a0, a1
という Addr
の互いに異ならなくてもよいインスタンスのある組み合わせについて,|
以下の論理式が成り立っていることを示しています.|
以下の論理式は {
と }
で囲まれている4つの論理式をまとめたもの,すなわち4つの論理式が同時に成り立っていることを示す1つの論理式になります.
この4つの論理式も同時に成り立っているので,記述の順序を変えても意味は変わらないのですが,しかし,実行において最初に init 操作が呼ばれて,次に add 操作が2回呼ばれ,最後に del 操作が呼ばれることを表しています.
- 詳細は後ほど説明しますが,これには,Book
の4つのインスタンスが関係しています.まず初期化の操作 init に関わるのは b0
です.次に,最初の add 操作は,b0
を b1
に変更します.
+ 詳細は後ほど説明しますが,これには,Book
の4つのインスタンス(b0, b1, b2, b3
)が関係しています.まず初期化の操作 init に関わるのは b0
です.次に,最初の add 操作は,b0
を b1
に変更します.
さらに,次の add 操作は,b1
を b2
に,最後の del 操作は b2
を b3
に変更します.このようにインスタンス(の状態)を受け渡すことによって,実行が進んでいくことを表すことができます.
- 可視化では実行時に生成される1つのインスタンスが,1つの矩形で表されます.たとえば,図の上部に並んでいる4つの矩形は,execute
述語内で宣言されている4つの変数,b0, b1, b2, b3
に対応しています.
+ 可視化では実行時に生成される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
に当たります.