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 という引数を持たない述語が呼び出されます．
diff --git a/courseA/DTRAM.html b/courseA/DTRAM.html
index 3b2afc0..055630a 100644
--- a/courseA/DTRAM.html
+++ b/courseA/DTRAM.html
@@ -93,6 +93,7 @@
によって定義されています．
少しわかりにくいですが，この式では左端の book.addr が関数名に相当します．状態遷移関数の関数名にはリソース名をそのまま用います．
また関数 book.addr は，2つの引数を受け取っています．DTRAMでは，状態遷移関数の第1引数は遷移前の状態，第2引数は受け取るメッセージ，式の右辺は遷移後の状態を表しています．
+ すなわち，r(x, y) = z と定義されていた場合，リソース r はメッセージ y を受け取ると，状態を x から z に変化させることを意味しています．
この例では，メッセージ add(name, addr) を受け取った book.addr リソースが，状態を pre_addr から insert(pre_addr, name, addr) に変化させることが示されています．
この insert() 関数は，第1引数に渡された写像(対応表)に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．
したがって，上の式の右辺は，遷移前の状態 prev_addr に対して，メッセージ add() の引数で渡された name と addr の対応を追加した写像が遷移後の状態になることを示しています．
diff --git a/courseB/Alloy.html b/courseB/Alloy.html
index c628c13..9198e04 100644
--- a/courseB/Alloy.html
+++ b/courseB/Alloy.html
@@ -22,7 +22,7 @@
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 という引数を持たない述語が呼び出されます．
diff --git a/courseB/DTRAM.html b/courseB/DTRAM.html
index a498dc3..13255fe 100644
--- a/courseB/DTRAM.html
+++ b/courseB/DTRAM.html
@@ -93,6 +93,7 @@
によって定義されています．
少しわかりにくいですが，この式では左端の book.addr が関数名に相当します．状態遷移関数の関数名にはリソース名をそのまま用います．
また関数 book.addr は，2つの引数を受け取っています．DTRAMでは，状態遷移関数の第1引数は遷移前の状態，第2引数は受け取るメッセージ，式の右辺は遷移後の状態を表しています．
+ すなわち，r(x, y) = z と定義されていた場合，リソース r はメッセージ y を受け取ると，状態を x から z に変化させることを意味しています．
この例では，メッセージ add(name, addr) を受け取った book.addr リソースが，状態を pre_addr から insert(pre_addr, name, addr) に変化させることが示されています．
この insert() 関数は，第1引数に渡された写像(対応表)に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．
したがって，上の式の右辺は，遷移前の状態 prev_addr に対して，メッセージ add() の引数で渡された name と addr の対応を追加した写像が遷移後の状態になることを示しています．
diff --git a/courseC/Alloy.html b/courseC/Alloy.html
index e084cd6..f1aca7e 100644
--- a/courseC/Alloy.html
+++ b/courseC/Alloy.html
@@ -52,15 +52,17 @@
- 以下の仕様記述では名前の集合を 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 の対応を追加した関係を表しています．）
Alloy では実行は，execute という引数を持たない述語が呼び出されます．
diff --git a/courseC/DTRAM.html b/courseC/DTRAM.html
index 87b9fcc..7c3f448 100644
--- a/courseC/DTRAM.html
+++ b/courseC/DTRAM.html
@@ -22,7 +22,7 @@
DTRAM は仕様とアーキテクチャの両方を同時に記述することが可能な言語で，形式的仕様記述言語であると同時に形式的アーキテクチャ記述言語でもあります．
- 形式的仕様記述言語とは，仕様を自然言語ではなく，論理式のような数学的に厳密に意味が定義された形式で記述する方法で，
+ 形式的仕様記述言語とは，仕様を自然言語ではなく，論理式や等式のような数学的に厳密に意味が定義された形式で記述する方法で，
book.addr が関数名に相当します．状態遷移関数の関数名にはリソース名をそのまま用います．book.addr は，2つの引数を受け取っています．DTRAMでは，状態遷移関数の第1引数は遷移前の状態，第2引数は受け取るメッセージ，式の右辺は遷移後の状態を表しています．r(x, y) = z と定義されていた場合，リソース r はメッセージ y を受け取ると，状態を x から z に変化させることを意味しています．add(name, addr) を受け取った book.addr リソースが，状態を pre_addr から insert(pre_addr, name, addr) に変化させることが示されています．insert() 関数は，第1引数に渡された写像(対応表)に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．
したがって，上の式の右辺は，遷移前の状態 prev_addr に対して，メッセージ add() の引数で渡された name と addr の対応を追加した写像が遷移後の状態になることを示しています．: の直後に変数の型を記述することができます．型推論によって型がわかる場合には，型を省略することもできます．状態の型が，List Map Json : の直後に変数の型を記述することができます．型推論によって型がわかる場合には，型を省略することもできます．List Map Json List Map Json diff --git a/courseD/Alloy.html b/courseD/Alloy.html index f66c1fd..c432ff4 100644 --- a/courseD/Alloy.html +++ b/courseD/Alloy.html @@ -52,15 +52,17 @@Alloy による記述例:
- 以下の仕様記述では名前の集合を
Name，アドレスの集合をAddr，アドレス帳の集合をBookで表しています．
+ 以下の仕様記述では名前の集合を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と，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の対応を追加した関係を表しています．）Alloy では実行は，
run で指定された述語を呼び出すことによってなされます．ここでは，executeという引数を持たない述語が呼び出されます．
diff --git a/courseD/DTRAM.html b/courseD/DTRAM.html index ef019ff..357cea8 100644 --- a/courseD/DTRAM.html +++ b/courseD/DTRAM.html @@ -22,7 +22,7 @@形式的仕様記述言語とは？
DTRAM は仕様とアーキテクチャの両方を同時に記述することが可能な言語で，形式的仕様記述言語であると同時に形式的アーキテクチャ記述言語でもあります．
- 形式的仕様記述言語とは，仕様を自然言語ではなく，論理式のような数学的に厳密に意味が定義された形式で記述する方法で，
+ 形式的仕様記述言語とは，仕様を自然言語ではなく，論理式や等式のような数学的に厳密に意味が定義された形式で記述する方法で，
book.addr が関数名に相当します．状態遷移関数の関数名にはリソース名をそのまま用います．book.addr は，2つの引数を受け取っています．DTRAMでは，状態遷移関数の第1引数は遷移前の状態，第2引数は受け取るメッセージ，式の右辺は遷移後の状態を表しています．r(x, y) = z と定義されていた場合，リソース r はメッセージ y を受け取ると，状態を x から z に変化させることを意味しています．add(name, addr) を受け取った book.addr リソースが，状態を pre_addr から insert(pre_addr, name, addr) に変化させることが示されています．insert() 関数は，第1引数に渡された写像(対応表)に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．
したがって，上の式の右辺は，遷移前の状態 prev_addr に対して，メッセージ add() の引数で渡された name と addr の対応を追加した写像が遷移後の状態になることを示しています．