diff --git a/courseA/Alloy.html b/courseA/Alloy.html index a03a226..c83ae4e 100644 --- a/courseA/Alloy.html +++ b/courseA/Alloy.html @@ -145,7 +145,7 @@

addr フィールドは少し複雑です．この仕様では addr フィールドは，addr: Name -> lone Addr のように定義されています． これは，addr フィールドが Name から Addr への対応関係を参照していることを表しています． - ここで，lone の記述は Name の各要素に対して，対応する Addr がたかだか1つ（0個か1個）であることを示しています．
+ ここで，lone の記述は Name の各要素に対して，対応する Addr の要素がたかだか1つ（0個か1個）であることを示しています．
たとえば，Book2 を見ると，addr は Name1 に Addr1 を対応させていることがわかります． 一方，Name0 に対応する Addr の要素は存在していません．Book1 では add 操作によって，新たに Name0 から Addr0 への対応が追加されています． さらに Book0 ではadd 操作によって，Name1 から Addr1 への対応が削除されています．
diff --git a/courseA/IM_Alloy.html b/courseA/IM_Alloy.html index 6957c4a..ac4b391 100644 --- a/courseA/IM_Alloy.html +++ b/courseA/IM_Alloy.html @@ -57,7 +57,7 @@ 直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．

- 最後の execute では，init，itemRegistraction，receivingOrShipping を + 最後の execute では，init，itemRegistration，receivingOrShipping を この順で呼び出す操作を定義しています．
run では，execute を呼び出して仮想実行を行います． この実行の際に，Int で8bitの整数を扱うことができるよう末尾に 8 Int という記述を付け加えています． diff --git a/courseA/ST_Alloy.html b/courseA/ST_Alloy.html index 5b6f8b5..ba53683 100644 --- a/courseA/ST_Alloy.html +++ b/courseA/ST_Alloy.html @@ -19,7 +19,8 @@

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

diff --git a/courseA/ST_DTRAM.html b/courseA/ST_DTRAM.html index 6378c73..da23c2a 100644 --- a/courseA/ST_DTRAM.html +++ b/courseA/ST_DTRAM.html @@ -19,7 +19,8 @@

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

diff --git a/courseB/Alloy.html b/courseB/Alloy.html index 48eb946..c628c13 100644 --- a/courseB/Alloy.html +++ b/courseB/Alloy.html @@ -145,7 +145,7 @@

addr フィールドは少し複雑です．この仕様では addr フィールドは，addr: Name -> lone Addr のように定義されています． これは，addr フィールドが Name から Addr への対応関係を参照していることを表しています． - ここで，lone の記述は Name の各要素に対して，対応する Addr がたかだか1つ（0個か1個）であることを示しています．
+ ここで，lone の記述は Name の各要素に対して，対応する Addr の要素がたかだか1つ（0個か1個）であることを示しています．
たとえば，Book2 を見ると，addr は Name1 に Addr1 を対応させていることがわかります． 一方，Name0 に対応する Addr の要素は存在していません．Book1 では add 操作によって，新たに Name0 から Addr0 への対応が追加されています． さらに Book0 ではadd 操作によって，Name1 から Addr1 への対応が削除されています．
diff --git a/courseB/IM_Alloy_B.html b/courseB/IM_Alloy_B.html index f122e6b..d656fc8 100644 --- a/courseB/IM_Alloy_B.html +++ b/courseB/IM_Alloy_B.html @@ -19,7 +19,8 @@

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

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

- 最後の execute では，init，itemRegistraction，receivingOrShipping を + 最後の execute では，init，itemRegistration，receivingOrShipping を この順で呼び出す操作を定義しています．
run では，execute を呼び出して仮想実行を行います． この実行の際に，Int で8bitの整数を扱うことができるよう末尾に 8 Int という記述を付け加えています． diff --git a/courseB/IM_DTRAM_B.html b/courseB/IM_DTRAM_B.html index 1943f21..86e8b93 100644 --- a/courseB/IM_DTRAM_B.html +++ b/courseB/IM_DTRAM_B.html @@ -19,7 +19,8 @@

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

diff --git a/courseC/Alloy.html b/courseC/Alloy.html index 9b4b498..e084cd6 100644 --- a/courseC/Alloy.html +++ b/courseC/Alloy.html @@ -131,7 +131,7 @@

addr フィールドは少し複雑です．この仕様では addr フィールドは，addr: Name -> lone Addr のように定義されています． これは，addr フィールドが Name から Addr への対応関係を参照していることを表しています． - ここで，lone の記述は Name の各要素に対して，対応する Addr がたかだか1つ（0個か1個）であることを示しています．
+ ここで，lone の記述は Name の各要素に対して，対応する Addr の要素がたかだか1つ（0個か1個）であることを示しています．
たとえば，Book2 を見ると，addr は Name1 に Addr1 を対応させていることがわかります． 一方，Name0 に対応する Addr の要素は存在していません．Book1 では add 操作によって，新たに Name0 から Addr0 への対応が追加されています． さらに Book0 ではadd 操作によって，Name1 から Addr1 への対応が削除されています．
diff --git a/courseC/IM_Alloy_C.html b/courseC/IM_Alloy_C.html index 4e990c8..c4251ca 100644 --- a/courseC/IM_Alloy_C.html +++ b/courseC/IM_Alloy_C.html @@ -57,7 +57,7 @@ 直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．

- 最後の execute では，init，itemRegistraction，receivingOrShipping を + 最後の execute では，init，itemRegistration，receivingOrShipping を この順で呼び出す操作を定義しています．
run では，execute を呼び出して仮想実行を行います． この実行の際に，Int で8bitの整数を扱うことができるよう末尾に 8 Int という記述を付け加えています． diff --git a/courseC/ST_Alloy_C.html b/courseC/ST_Alloy_C.html index b2a441e..492c031 100644 --- a/courseC/ST_Alloy_C.html +++ b/courseC/ST_Alloy_C.html @@ -19,7 +19,8 @@

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

diff --git a/courseC/ST_DTRAM_C.html b/courseC/ST_DTRAM_C.html index 7485b82..ab09216 100644 --- a/courseC/ST_DTRAM_C.html +++ b/courseC/ST_DTRAM_C.html @@ -19,7 +19,8 @@

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

diff --git a/courseD/Alloy.html b/courseD/Alloy.html index c944d27..f66c1fd 100644 --- a/courseD/Alloy.html +++ b/courseD/Alloy.html @@ -131,7 +131,7 @@

addr フィールドは少し複雑です．この仕様では addr フィールドは，addr: Name -> lone Addr のように定義されています． これは，addr フィールドが Name から Addr への対応関係を参照していることを表しています． - ここで，lone の記述は Name の各要素に対して，対応する Addr がたかだか1つ（0個か1個）であることを示しています．
+ ここで，lone の記述は Name の各要素に対して，対応する Addr の要素がたかだか1つ（0個か1個）であることを示しています．
たとえば，Book2 を見ると，addr は Name1 に Addr1 を対応させていることがわかります． 一方，Name0 に対応する Addr の要素は存在していません．Book1 では add 操作によって，新たに Name0 から Addr0 への対応が追加されています． さらに Book0 ではadd 操作によって，Name1 から Addr1 への対応が削除されています．
diff --git a/courseD/IM_Alloy_D.html b/courseD/IM_Alloy_D.html index 096f5c5..93e9f60 100644 --- a/courseD/IM_Alloy_D.html +++ b/courseD/IM_Alloy_D.html @@ -19,7 +19,8 @@

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

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

- 最後の execute では，init，itemRegistraction，receivingOrShipping を + 最後の execute では，init，itemRegistration，receivingOrShipping を この順で呼び出す操作を定義しています．
run では，execute を呼び出して仮想実行を行います． この実行の際に，Int で8bitの整数を扱うことができるよう末尾に 8 Int という記述を付け加えています． diff --git a/courseD/IM_DTRAM_D.html b/courseD/IM_DTRAM_D.html index e8f1ab0..bcdc9cf 100644 --- a/courseD/IM_DTRAM_D.html +++ b/courseD/IM_DTRAM_D.html @@ -19,7 +19,8 @@

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