diff --git a/courseA/DTRAM.html b/courseA/DTRAM.html index 945bf55..3b2afc0 100644 --- a/courseA/DTRAM.html +++ b/courseA/DTRAM.html @@ -96,7 +96,8 @@ この例では，メッセージ 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 はJSONオブジェクト型を表します．

Alloy と異なり，DTRAM では仮想実行に関する情報を仕様記述には記載しません． diff --git a/courseA/IM_Alloy.html b/courseA/IM_Alloy.html index 3faa717..4a79af1 100644 --- a/courseA/IM_Alloy.html +++ b/courseA/IM_Alloy.html @@ -41,8 +41,8 @@

pred:

- 最初の述語として記述されている init は，Inventory の - インスタンスである its が初期化されていることを示しています．
+ 最初の述語として記述されている init は，Inventory のインスタンスである its が初期化されていることを示しています． + 具体的には述語定義中の noで，its.itemDB が空であることを示しています．

次の itemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と， @@ -54,7 +54,8 @@ receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と， 操作後のインスタンス its' の関係を述語として定義しています．ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
また，述語定義中の some it': Item は，its のデータベースに登録されていない Item のインスタンス (it') が存在していることを示しており， - 直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．なお関数 plus[x, y] は，加算 x + y を表します．
+ 直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．
+ なお x ++ y -> z は，関係 x 中ですでに y に何らかの値が対応していた場合に，それを y から z への対応に置き換えたものを表しています．関数 plus[x, y] は，加算 x + y を表します．

最後の execute では，init，itemRegistration，receivingOrShipping を diff --git a/courseA/ST_Alloy.html b/courseA/ST_Alloy.html index 038e4ae..affc817 100644 --- a/courseA/ST_Alloy.html +++ b/courseA/ST_Alloy.html @@ -44,8 +44,8 @@

pred:

- 最初の述語として記述されている init は，Accounts の - インスタンスである acs が初期化されていることを示しています．
+ 最初の述語として記述されている init は，Accounts のインスタンスである acs が初期化されていることを示しています． + 具体的には述語定義中の noで，acs.accountDB が空であることを示しています．

次の signUp は，id に対応するアカウントを登録する前の Accounts のインスタンス acs と， @@ -54,11 +54,11 @@ 直観的には Account のインスタンスが生成されたことを示しています．

- tweet ではid で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と， + tweet では id で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と， 操作後のインスタンス acs' の関係を述語として定義しています．ここで contents はツイートの内容を表しています．
述語定義中の some ac': Account は，acs のデータベースに登録されていない Account のインスタンス (ac') が存在していることを示しており， 直観的には Account のインスタンスが，ツイートを行うことによって複製されたことを示しています．
- なお，関数 plus[x, y] は加算 x + y を，関数 minus[x, y] は減算 x - y を表します． + なお x ++ y -> z は，関係 x 中ですでに y に何らかの値が対応していた場合に，それを y から z への対応に置き換えたものを表しています．関数 plus[x, y] は加算 x + y を，関数 minus[x, y] は減算 x - y を表します．
また implies は，その前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．

diff --git a/courseB/DTRAM.html b/courseB/DTRAM.html index f77bf0f..a498dc3 100644 --- a/courseB/DTRAM.html +++ b/courseB/DTRAM.html @@ -96,7 +96,8 @@ この例では，メッセージ 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 はJSONオブジェクト型を表します．

Alloy と異なり，DTRAM では仮想実行に関する情報を仕様記述には記載しません． diff --git a/courseB/IM_Alloy_B.html b/courseB/IM_Alloy_B.html index e83e5aa..bb81a0f 100644 --- a/courseB/IM_Alloy_B.html +++ b/courseB/IM_Alloy_B.html @@ -42,8 +42,8 @@

pred:

- 最初の述語として記述されている init は，Inventory の - インスタンスである its が初期化されていることを示しています．
+ 最初の述語として記述されている init は，Inventory のインスタンスである its が初期化されていることを示しています． + 具体的には述語定義中の noで，its.itemDB が空であることを示しています．

次の itemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と， @@ -55,7 +55,8 @@ receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と， 操作後のインスタンス its' の関係を述語として定義しています．ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
また，述語定義中の some it': Item は，its のデータベースに登録されていない Item のインスタンス (it') が存在していることを示しており， - 直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．なお関数 plus[x, y] は，加算 x + y を表します．
+ 直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．
+ なお x ++ y -> z は，関係 x 中ですでに y に何らかの値が対応していた場合に，それを y から z への対応に置き換えたものを表しています．関数 plus[x, y] は，加算 x + y を表します．

最後の execute では，init，itemRegistration，receivingOrShipping を diff --git a/courseB/ST_Alloy_B.html b/courseB/ST_Alloy_B.html index 5dd24af..7be0561 100644 --- a/courseB/ST_Alloy_B.html +++ b/courseB/ST_Alloy_B.html @@ -43,8 +43,8 @@

pred:

- 最初の述語として記述されている init は，Accounts の - インスタンスである acs が初期化されていることを示しています．
+ 最初の述語として記述されている init は，Accounts のインスタンスである acs が初期化されていることを示しています． + 具体的には述語定義中の noで，acs.accountDB が空であることを示しています．

次の signUp は，id に対応するアカウントを登録する前の Accounts のインスタンス acs と， @@ -53,11 +53,11 @@ 直観的には Account のインスタンスが生成されたことを示しています．

- tweet ではid で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と， + tweet では id で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と， 操作後のインスタンス acs' の関係を述語として定義しています．ここで contents はツイートの内容を表しています．
述語定義中の some ac': Account は，acs のデータベースに登録されていない Account のインスタンス (ac') が存在していることを示しており， 直観的には Account のインスタンスが，ツイートを行うことによって複製されたことを示しています．
- なお，関数 plus[x, y] は加算 x + y を，関数 minus[x, y] は減算 x - y を表します． + なお x ++ y -> z は，関係 x 中ですでに y に何らかの値が対応していた場合に，それを y から z への対応に置き換えたものを表しています．関数 plus[x, y] は加算 x + y を，関数 minus[x, y] は減算 x - y を表します．
また implies は，その前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．

diff --git a/courseC/DTRAM.html b/courseC/DTRAM.html index 08a8ccd..87b9fcc 100644 --- a/courseC/DTRAM.html +++ b/courseC/DTRAM.html @@ -23,15 +23,15 @@

DTRAM は仕様とアーキテクチャの両方を同時に記述することが可能な言語で，形式的仕様記述言語であると同時に形式的アーキテクチャ記述言語でもあります．
形式的仕様記述言語とは，仕様を自然言語ではなく，論理式のような数学的に厳密に意味が定義された形式で記述する方法で，
-

-といった特長を持っています．
-コンピュータによる仕様の解析としては，仕様レベルで不具合が存在しないか（機能的要件が満たされているか）を網羅的に調べたり，セキュリティホールが存在しないことを確認することなどが挙げられます．
-形式的仕様記述言語による記述は，通常のプログラミング言語におけるソースコードの記述とはかなり異なっております．そのため，最初に形式的な仕様記述を見ると少々戸惑うかもしれません．
-一般的に形式的仕様記述言語の表現能力はプログラミング言語よりも低く，表現能力が低くなればなるほど複雑な振る舞いが記述できなくなる一方で，強力な解析ができるといった関係が成り立っています．
+ + といった特長を持っています．
+ コンピュータによる仕様の解析としては，仕様レベルで不具合が存在しないか（機能的要件が満たされているか）を網羅的に調べたり，セキュリティホールが存在しないことを確認することなどが挙げられます．
+ 形式的仕様記述言語による記述は，通常のプログラミング言語におけるソースコードの記述とはかなり異なっております．そのため，最初に形式的な仕様記述を見ると少々戸惑うかもしれません．
+ 一般的に形式的仕様記述言語の表現能力はプログラミング言語よりも低く，表現能力が低くなればなるほど複雑な振る舞いが記述できなくなる一方で，強力な解析ができるといった関係が成り立っています．

アーキテクチャ記述言語とは？

diff --git a/courseC/IM_Alloy_C.html b/courseC/IM_Alloy_C.html index b0dbb92..2bd1a59 100644 --- a/courseC/IM_Alloy_C.html +++ b/courseC/IM_Alloy_C.html @@ -41,8 +41,8 @@

pred:

- 最初の述語として記述されている init は，Inventory の - インスタンスである its が初期化されていることを示しています．
+ 最初の述語として記述されている init は，Inventory のインスタンスである its が初期化されていることを示しています． + 具体的には述語定義中の noで，its.itemDB が空であることを示しています．

次の itemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と， @@ -54,7 +54,8 @@ receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と， 操作後のインスタンス its' の関係を述語として定義しています．ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
また，述語定義中の some it': Item は，its のデータベースに登録されていない Item のインスタンス (it') が存在していることを示しており， - 直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．なお関数 plus[x, y] は，加算 x + y を表します．
+ 直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．
+ なお x ++ y -> z は，関係 x 中ですでに y に何らかの値が対応していた場合に，それを y から z への対応に置き換えたものを表しています．関数 plus[x, y] は，加算 x + y を表します．

最後の execute では，init，itemRegistration，receivingOrShipping を diff --git a/courseC/ST_Alloy_C.html b/courseC/ST_Alloy_C.html index f4fc62a..874cc54 100644 --- a/courseC/ST_Alloy_C.html +++ b/courseC/ST_Alloy_C.html @@ -44,8 +44,8 @@

pred:

- 最初の述語として記述されている init は，Accounts の - インスタンスである acs が初期化されていることを示しています．
+ 最初の述語として記述されている init は，Accounts のインスタンスである acs が初期化されていることを示しています． + 具体的には述語定義中の noで，acs.accountDB が空であることを示しています．

次の signUp は，id に対応するアカウントを登録する前の Accounts のインスタンス acs と， @@ -54,11 +54,11 @@ 直観的には Account のインスタンスが生成されたことを示しています．

- tweet ではid で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と， + tweet では id で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と， 操作後のインスタンス acs' の関係を述語として定義しています．ここで contents はツイートの内容を表しています．
述語定義中の some ac': Account は，acs のデータベースに登録されていない Account のインスタンス (ac') が存在していることを示しており， 直観的には Account のインスタンスが，ツイートを行うことによって複製されたことを示しています．
- なお，関数 plus[x, y] は加算 x + y を，関数 minus[x, y] は減算 x - y を表します． + なお x ++ y -> z は，関係 x 中ですでに y に何らかの値が対応していた場合に，それを y から z への対応に置き換えたものを表しています．関数 plus[x, y] は加算 x + y を，関数 minus[x, y] は減算 x - y を表します．
また implies は，その前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．

diff --git a/courseD/DTRAM.html b/courseD/DTRAM.html index a89793a..ef019ff 100644 --- a/courseD/DTRAM.html +++ b/courseD/DTRAM.html @@ -23,15 +23,15 @@

DTRAM は仕様とアーキテクチャの両方を同時に記述することが可能な言語で，形式的仕様記述言語であると同時に形式的アーキテクチャ記述言語でもあります．
形式的仕様記述言語とは，仕様を自然言語ではなく，論理式のような数学的に厳密に意味が定義された形式で記述する方法で，
-

-といった特長を持っています．
-コンピュータによる仕様の解析としては，仕様レベルで不具合が存在しないか（機能的要件が満たされているか）を網羅的に調べたり，セキュリティホールが存在しないことを確認することなどが挙げられます．
-形式的仕様記述言語による記述は，通常のプログラミング言語におけるソースコードの記述とはかなり異なっております．そのため，最初に形式的な仕様記述を見ると少々戸惑うかもしれません．
-一般的に形式的仕様記述言語の表現能力はプログラミング言語よりも低く，表現能力が低くなればなるほど複雑な振る舞いが記述できなくなる一方で，強力な解析ができるといった関係が成り立っています．
+ + といった特長を持っています．
+ コンピュータによる仕様の解析としては，仕様レベルで不具合が存在しないか（機能的要件が満たされているか）を網羅的に調べたり，セキュリティホールが存在しないことを確認することなどが挙げられます．
+ 形式的仕様記述言語による記述は，通常のプログラミング言語におけるソースコードの記述とはかなり異なっております．そのため，最初に形式的な仕様記述を見ると少々戸惑うかもしれません．
+ 一般的に形式的仕様記述言語の表現能力はプログラミング言語よりも低く，表現能力が低くなればなるほど複雑な振る舞いが記述できなくなる一方で，強力な解析ができるといった関係が成り立っています．

アーキテクチャ記述言語とは？

@@ -109,7 +109,8 @@ この例では，メッセージ 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 はJSONオブジェクト型を表します． 

diff --git a/courseD/IM_Alloy_D.html b/courseD/IM_Alloy_D.html
index 01ff0e4..a0e1029 100644
--- a/courseD/IM_Alloy_D.html
+++ b/courseD/IM_Alloy_D.html
@@ -42,8 +42,8 @@
 
 
pred:

 

-	最初の述語として記述されている init は，Inventory の
-	インスタンスである its が初期化されていることを示しています．

+	最初の述語として記述されている init は，Inventory のインスタンスである its が初期化されていることを示しています．
+	具体的には述語定義中の noで，its.itemDB が空であることを示しています．

 

 

 	次の itemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と，
@@ -55,7 +55,8 @@
 	receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と，
 	操作後のインスタンス its' の関係を述語として定義しています．ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．

 	また，述語定義中の some it': Item は，its のデータベースに登録されていない Item のインスタンス (it') が存在していることを示しており，
-	直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．なお関数 plus[x, y] は，加算 x + y を表します．

+	直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．

+	なお x ++ y -> z は，関係 x 中ですでに y に何らかの値が対応していた場合に，それを y から z への対応に置き換えたものを表しています．関数 plus[x, y] は，加算 x + y を表します．

 

 

 	最後の execute では，init，itemRegistration，receivingOrShipping を
diff --git a/courseD/ST_Alloy_D.html b/courseD/ST_Alloy_D.html
index 79ffa8b..cfdc3c8 100644
--- a/courseD/ST_Alloy_D.html
+++ b/courseD/ST_Alloy_D.html
@@ -43,8 +43,8 @@
 
 
pred:

 

-	最初の述語として記述されている init は，Accounts の
-	インスタンスである acs が初期化されていることを示しています．

+	最初の述語として記述されている init は，Accounts のインスタンスである acs が初期化されていることを示しています．
+	具体的には述語定義中の noで，acs.accountDB が空であることを示しています．

 

 

 	次の signUp は，id に対応するアカウントを登録する前の Accounts のインスタンス acs と，
@@ -53,11 +53,11 @@
 	直観的には Account のインスタンスの生成を示しています．

 

 

-	tweet ではid で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と，
+	tweet では id で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と，
 	操作後のインスタンス acs' の関係を述語として定義しています．ここで contents はツイートの内容を表しています．

 	述語定義中の some ac': Account は，acs のデータベースに登録されていない Account のインスタンス (ac') が存在していることを示しており，
 	直観的には Account のインスタンスが，ツイートを行うことによって複製されたことを示しています．

-	なお，関数 plus[x, y] は加算 x + y を，関数 minus[x, y] は減算 x - y を表します．
+	なお x ++ y -> z は，関係 x 中ですでに y に何らかの値が対応していた場合に，それを y から z への対応に置き換えたものを表しています．関数 plus[x, y] は加算 x + y を，関数 minus[x, y] は減算 x - y を表します．

 	また implies は，その前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．