diff --git a/courseA/IM_DTRAM.html b/courseA/IM_DTRAM.html index 5003ba2..064ac9e 100644 --- a/courseA/IM_DTRAM.html +++ b/courseA/IM_DTRAM.html @@ -38,7 +38,7 @@

ItemRegistration チャンネルでは inventory リソースが，メッセージ registerItem(itemId, itemName, quantity) を受け取ると， リソースの状態が itemDB から insert(itemDB, itemId, {"count": quantity, "name": itemName}) に変わることを示しています．
- ここで，insert() 関数は，第1引数に渡された写像に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．
+ ここで，関数 insert(x, y, z) は，写像 x に対し，キー y と値 z の対応を追加した結果得られる写像を返す関数です．
また {"count": quantity, "name": itemName} は，"count" と "name" をキーに持つ JSON オブジェクトを表しています．

diff --git a/courseA/ST_Alloy.html b/courseA/ST_Alloy.html index ba53683..038e4ae 100644 --- a/courseA/ST_Alloy.html +++ b/courseA/ST_Alloy.html @@ -20,7 +20,7 @@

ここでは，SimpleTwitter の Alloy による仕様記述に関する課題に取り組んでいただきます．
以下に Alloy で記述された SimpleTwitter のモデルを示します．こちらを適宜参照しながら課題を進めてください．
- Alloy の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます) + Alloy の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます)．

@@ -58,6 +58,7 @@ 操作後のインスタンス acs' の関係を述語として定義しています．ここで contents はツイートの内容を表しています．
述語定義中の some ac': Account は，acs のデータベースに登録されていない Account のインスタンス (ac') が存在していることを示しており， 直観的には Account のインスタンスが，ツイートを行うことによって複製されたことを示しています．
+ なお，関数 plus[x, y] は加算 x + y を，関数 minus[x, y] は減算 x - y を表します． また implies は，その前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．

diff --git a/courseA/ST_DTRAM.html b/courseA/ST_DTRAM.html index da23c2a..191b043 100644 --- a/courseA/ST_DTRAM.html +++ b/courseA/ST_DTRAM.html @@ -20,7 +20,7 @@

ここでは，SimpleTwitter の DTRAM による仕様記述に関する課題に取り組んでいただきます．
以下に DTRAM で記述された SimpleTwitter のモデルを示します．こちらを適宜参照しながら課題を進めてください．
- DTRAM の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます) + DTRAM の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます)．

@@ -39,13 +39,13 @@ アカウント登録用のイベントチャンネルを Signup，accountId で登録されているアカウントに対してツイートを行うためのイベントチャンネルを Tweet(accountId:Str) として宣言しています．

-Signup チャンネルでは accounts リソースが，メッセージ signUp(accountId, name) を受け取ると， リソースの状態が accountDB から insert(accountDB, accountId, {"name": name, "tweets": nil}) に変わることを示しています．nil は空のマップやリストを表しています．
-ここで，insert() 関数は，第1引数に渡された写像に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．また {"name": name, "tweets": nil} は，"name" と "tweets" をキーに持つ JSON オブジェクトを表しています．
+ Signup チャンネルでは accounts リソースが，メッセージ signUp(accountId, name) を受け取ると， リソースの状態が accountDB から insert(accountDB, accountId, {"name": name, "tweets": nil}) に変わることを示しています．nil は空のマップやリストを表しています．
+ ここで，関数 insert(x, y, z) は，写像 x に対し，キー y と値 z の対応を追加した結果得られる写像を返す関数です．また {"name": name, "tweets": nil} は，"name" と "tweets" をキーに持つ JSON オブジェクトを表しています．

-Tweet(accountId:Str) チャンネルでは accounts.{accountId}.tweets リソースがメッセージ tweet(contents) を受け取ると， -遷移前の状態 tweetList が append(tweetList, contents) に変わることを示しています．
-ここで，append() 関数は，第1引数に渡されたリストに対し，第2引数のオブジェクトを末尾に追加した結果得られるリストを返す関数です．
+ Tweet(accountId:Str) チャンネルでは accounts.{accountId}.tweets リソースがメッセージ tweet(contents) を受け取ると， + 遷移前の状態 tweetList が append(tweetList, contents) に変わることを示しています．
+ ここで，関数 append(x, y) は，リスト x に対し，オブジェクト y を末尾に追加した結果得られるリストを返す関数です．

diff --git a/courseB/IM_Alloy_B.html b/courseB/IM_Alloy_B.html index d656fc8..e83e5aa 100644 --- a/courseB/IM_Alloy_B.html +++ b/courseB/IM_Alloy_B.html @@ -20,7 +20,7 @@

ここでは，InventoryManagement の Alloy による仕様記述に関する課題に取り組んでいただきます．
以下に Alloy で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながら課題を進めてください．
- Alloy の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます) + Alloy の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます)．

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

最後の execute では，init，itemRegistration，receivingOrShipping を @@ -165,6 +165,7 @@ ここからが課題です．
本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ なお，以下のモデル中にある関数 minus[x, y] は，減算 x - y を表します．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．

diff --git a/courseB/IM_DTRAM_B.html b/courseB/IM_DTRAM_B.html index 86e8b93..6a7b418 100644 --- a/courseB/IM_DTRAM_B.html +++ b/courseB/IM_DTRAM_B.html @@ -20,7 +20,7 @@

ここでは，InventoryManagement の DTRAM による仕様記述に関する課題に取り組んでいただきます．
以下に DTRAM で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながら課題を進めてください．
- DTRAM の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます) + DTRAM の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます)．

@@ -39,7 +39,7 @@

ItemRegistration チャンネルでは inventory リソースが，メッセージ registerItem(itemId, itemName, quantity) を受け取ると， リソースの状態が itemDB から insert(itemDB, itemId, {"count": quantity, "name": itemName}) に変わることを示しています．
- ここで，insert() 関数は，第1引数に渡された写像に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．
+ ここで，関数 insert(x, y, z) は，写像 x に対し，キー y と値 z の対応を追加した結果得られる写像を返す関数です．
また {"count": quantity, "name": itemName} は，"count" と "name" をキーに持つ JSON オブジェクトを表しています．

@@ -161,6 +161,7 @@ ここからが課題です．
本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ なお，以下のモデル中にある関数 if(x, y, z) は，x が true のときは y を返し，false のときは z を返します． 設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．

diff --git a/courseB/ST_Alloy_B.html b/courseB/ST_Alloy_B.html index f303387..5dd24af 100644 --- a/courseB/ST_Alloy_B.html +++ b/courseB/ST_Alloy_B.html @@ -57,6 +57,7 @@ 操作後のインスタンス acs' の関係を述語として定義しています．ここで contents はツイートの内容を表しています．
述語定義中の some ac': Account は，acs のデータベースに登録されていない Account のインスタンス (ac') が存在していることを示しており， 直観的には Account のインスタンスが，ツイートを行うことによって複製されたことを示しています．
+ なお，関数 plus[x, y] は加算 x + y を，関数 minus[x, y] は減算 x - y を表します． また implies は，その前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．

diff --git a/courseB/ST_DTRAM_B.html b/courseB/ST_DTRAM_B.html index 1be2570..e2d8a3f 100644 --- a/courseB/ST_DTRAM_B.html +++ b/courseB/ST_DTRAM_B.html @@ -39,12 +39,12 @@

Signup チャンネルでは accounts リソースが，メッセージ signUp(accountId, name) を受け取ると， リソースの状態が accountDB から insert(accountDB, accountId, {"name": name, "tweets": nil}) に変わることを示しています．nil は空のマップやリストを表しています．
- ここで，insert() 関数は，第1引数に渡された写像に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．また {"name": name, "tweets": nil} は，"name" と "tweets" をキーに持つ JSON オブジェクトを表しています．
+ ここで，関数 insert(x, y, z) は，写像 x に対し，キー y と値 z の対応を追加した結果得られる写像を返す関数です．また {"name": name, "tweets": nil} は，"name" と "tweets" をキーに持つ JSON オブジェクトを表しています．

Tweet(accountId:Str) チャンネルでは accounts.{accountId}.tweets リソースがメッセージ tweet(contents) を受け取ると， 遷移前の状態 tweetList が append(tweetList, contents) に変わることを示しています．
- ここで，append() 関数は，第1引数に渡されたリストに対し，第2引数のオブジェクトを末尾に追加した結果得られるリストを返す関数です．
+ ここで，関数 append(x, y) は，リスト x に対し，オブジェクト y を末尾に追加した結果得られるリストを返す関数です．

@@ -160,7 +160,7 @@ ここからが課題です．
本課題ではまず，上記にて説明を行った SimpleTwitter の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
- なお，以下のモデル中にある関数 if(x, y, x) は，x が true のときは y を返し，false のときは z を返します． + なお，以下のモデル中にある関数 if(x, y, z) は，x が true のときは y を返し，false のときは z を返します． また関数 contains(x, y) は，写像 x のキーとして y が含まれているときは true を，そうでないときは false を返します．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．

diff --git a/courseC/IM_Alloy_C.html b/courseC/IM_Alloy_C.html index c4251ca..b0dbb92 100644 --- a/courseC/IM_Alloy_C.html +++ b/courseC/IM_Alloy_C.html @@ -54,7 +54,7 @@ receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と， 操作後のインスタンス its' の関係を述語として定義しています．ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
また，述語定義中の some it': Item は，its のデータベースに登録されていない Item のインスタンス (it') が存在していることを示しており， - 直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．
+ 直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．なお関数 plus[x, y] は，加算 x + y を表します．

最後の execute では，init，itemRegistration，receivingOrShipping を @@ -164,6 +164,7 @@ ここからが課題です．
本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ なお，以下のモデル中にある関数 minus[x, y] は，減算 x - y を表します．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．

diff --git a/courseC/IM_DTRAM_C.html b/courseC/IM_DTRAM_C.html index 12cbfa4..d7abcbf 100644 --- a/courseC/IM_DTRAM_C.html +++ b/courseC/IM_DTRAM_C.html @@ -38,7 +38,7 @@

ItemRegistration チャンネルでは inventory リソースが，メッセージ registerItem(itemId, itemName, quantity) を受け取ると， リソースの状態が itemDB から insert(itemDB, itemId, {"count": quantity, "name": itemName}) に変わることを示しています．
- ここで，insert() 関数は，第1引数に渡された写像に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．
+ ここで，関数 insert(x, y, z) は，写像 x に対し，キー y と値 z の対応を追加した結果得られる写像を返す関数です．
また {"count": quantity, "name": itemName} は，"count" と "name" をキーに持つ JSON オブジェクトを表しています．

@@ -160,7 +160,7 @@ ここからが課題です．
本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
- なお，以下のモデル中にある関数 if(x, y, x) は，x が true のときは y を返し，false のときは z を返します．
+ なお，以下のモデル中にある関数 if(x, y, z) は，x が true のときは y を返し，false のときは z を返します．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．

diff --git a/courseC/ST_Alloy_C.html b/courseC/ST_Alloy_C.html index 492c031..f4fc62a 100644 --- a/courseC/ST_Alloy_C.html +++ b/courseC/ST_Alloy_C.html @@ -20,7 +20,7 @@

ここでは，SimpleTwitter の Alloy による仕様記述に関する課題に取り組んでいただきます．
以下に Alloy で記述された SimpleTwitter のモデルを示します．こちらを適宜参照しながら課題を進めてください．
- Alloy の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます) + Alloy の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます)．

@@ -58,6 +58,7 @@ 操作後のインスタンス acs' の関係を述語として定義しています．ここで contents はツイートの内容を表しています．
述語定義中の some ac': Account は，acs のデータベースに登録されていない Account のインスタンス (ac') が存在していることを示しており， 直観的には Account のインスタンスが，ツイートを行うことによって複製されたことを示しています．
+ なお，関数 plus[x, y] は加算 x + y を，関数 minus[x, y] は減算 x - y を表します． また implies は，その前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．

diff --git a/courseC/ST_DTRAM_C.html b/courseC/ST_DTRAM_C.html index ab09216..6d257c7 100644 --- a/courseC/ST_DTRAM_C.html +++ b/courseC/ST_DTRAM_C.html @@ -20,7 +20,7 @@

ここでは，SimpleTwitter の DTRAM による仕様記述に関する課題に取り組んでいただきます．
以下に DTRAM で記述された SimpleTwitter のモデルを示します．こちらを適宜参照しながら課題を進めてください．
- DTRAM の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます) + DTRAM の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます)．

@@ -40,12 +40,12 @@

Signup チャンネルでは accounts リソースが，メッセージ signUp(accountId, name) を受け取ると， リソースの状態が accountDB から insert(accountDB, accountId, {"name": name, "tweets": nil}) に変わることを示しています．nil は空のマップやリストを表しています．
- ここで，insert() 関数は，第1引数に渡された写像に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．また {"name": name, "tweets": nil} は，"name" と "tweets" をキーに持つ JSON オブジェクトを表しています．
+ ここで，関数 insert(x, y, z) は，写像 x に対し，キー y と値 z の対応を追加した結果得られる写像を返す関数です．また {"name": name, "tweets": nil} は，"name" と "tweets" をキーに持つ JSON オブジェクトを表しています．

Tweet(accountId:Str) チャンネルでは accounts.{accountId}.tweets リソースがメッセージ tweet(contents) を受け取ると， 遷移前の状態 tweetList が append(tweetList, contents) に変わることを示しています．
- ここで，append() 関数は，第1引数に渡されたリストに対し，第2引数のオブジェクトを末尾に追加した結果得られるリストを返す関数です．
+ ここで，関数 append(x, y) は，リスト x に対し，オブジェクト y を末尾に追加した結果得られるリストを返す関数です．

@@ -161,6 +161,8 @@ ここからが課題です．
本課題ではまず，上記にて説明を行った SimpleTwitter の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ なお，以下のモデル中にある関数 if(x, y, z) は，x が true のときは y を返し，false のときは z を返します． + また関数 contains(x, y) は，写像 x のキーとして y が含まれているときは true を，そうでないときは false を返します．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．

diff --git a/courseD/IM_Alloy_D.html b/courseD/IM_Alloy_D.html index 93e9f60..01ff0e4 100644 --- a/courseD/IM_Alloy_D.html +++ b/courseD/IM_Alloy_D.html @@ -20,7 +20,7 @@

ここでは，InventoryManagement の Alloy による仕様記述に関する課題に取り組んでいただきます．
以下に Alloy で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながら課題を進めてください．
- Alloy の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます) + Alloy の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます)．

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

最後の execute では，init，itemRegistration，receivingOrShipping を diff --git a/courseD/IM_DTRAM_D.html b/courseD/IM_DTRAM_D.html index bcdc9cf..0955c62 100644 --- a/courseD/IM_DTRAM_D.html +++ b/courseD/IM_DTRAM_D.html @@ -20,7 +20,7 @@

ここでは，InventoryManagement の DTRAM による仕様記述に関する課題に取り組んでいただきます．
以下に DTRAM で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながら課題を進めてください．
- DTRAM の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます) + DTRAM の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます)．

@@ -39,7 +39,7 @@

ItemRegistration チャンネルでは inventory リソースが，メッセージ registerItem(itemId, itemName, quantity) を受け取ると， リソースの状態が itemDB から insert(itemDB, itemId, {"count": quantity, "name": itemName}) に変わることを示しています．
- ここで，insert() 関数は，第1引数に渡された写像に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．
+ ここで，関数 insert(x, y, z) は，写像 x に対し，キー y と値 z の対応を追加した結果得られる写像を返す関数です．
また {"count": quantity, "name": itemName} は，"count" と "name" をキーに持つ JSON オブジェクトを表しています．

diff --git a/courseD/ST_Alloy_D.html b/courseD/ST_Alloy_D.html index b01a57f..79ffa8b 100644 --- a/courseD/ST_Alloy_D.html +++ b/courseD/ST_Alloy_D.html @@ -57,6 +57,7 @@ 操作後のインスタンス acs' の関係を述語として定義しています．ここで contents はツイートの内容を表しています．
述語定義中の some ac': Account は，acs のデータベースに登録されていない Account のインスタンス (ac') が存在していることを示しており， 直観的には Account のインスタンスが，ツイートを行うことによって複製されたことを示しています．
+ なお，関数 plus[x, y] は加算 x + y を，関数 minus[x, y] は減算 x - y を表します． また implies は，その前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．

diff --git a/courseD/ST_DTRAM_D.html b/courseD/ST_DTRAM_D.html index b09d358..3b33bf5 100644 --- a/courseD/ST_DTRAM_D.html +++ b/courseD/ST_DTRAM_D.html @@ -39,12 +39,12 @@

Signup チャンネルでは accounts リソースが，メッセージ signUp(accountId, name) を受け取ると， リソースの状態が accountDB から insert(accountDB, accountId, {"name": name, "tweets": nil}) に変わることを示しています．nil は空のマップやリストを表しています．
- ここで，insert() 関数は，第1引数に渡された写像に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．また {"name": name, "tweets": nil} は，"name" と "tweets" をキーに持つ JSON オブジェクトを表しています．
+ ここで，関数 insert(x, y, z) は，写像 x に対し，キー y と値 z の対応を追加した結果得られる写像を返す関数です．また {"name": name, "tweets": nil} は，"name" と "tweets" をキーに持つ JSON オブジェクトを表しています．

Tweet(accountId:Str) チャンネルでは accounts.{accountId}.tweets リソースがメッセージ tweet(contents) を受け取ると， 遷移前の状態 tweetList が append(tweetList, contents) に変わることを示しています．
- ここで，append() 関数は，第1引数に渡されたリストに対し，第2引数のオブジェクトを末尾に追加した結果得られるリストを返す関数です．
+ ここで，関数 append(x, y) は，リスト x に対し，オブジェクト y を末尾に追加した結果得られるリストを返す関数です．