diff --git a/courseA/IM_Alloy.html b/courseA/IM_Alloy.html index 1072f45..f01d24b 100644 --- a/courseA/IM_Alloy.html +++ b/courseA/IM_Alloy.html @@ -27,25 +27,25 @@
sig :
以下のモデルでは始めに,商品を識別するためのIDを表す ItemId と商品名を表す Name を集合として宣言しています.
- 次に,商品全体を管理する倉庫を表している Inventory は, itemDB フィールドを持っています.
- このフィールドを定義している行では, itemDB フィールドが ItemId から,
+ 次に,商品全体を管理する倉庫を表している Inventory は,itemDB フィールドを持っています.
+ このフィールドを定義している行では,itemDB フィールドが ItemId から,
商品の情報を表す Item との対応関係を参照していることを表しています.
- 最後の Item では始めに,商品名を表す name を Item の要素と, Name の要素の間の関係として定義しています.
+ 最後の Item では始めに,商品名を表す name を Item の要素と,Name の要素の間の関係として定義しています.
次にある,在庫数を表す count では在庫数を Int
pred :
- 以下のモデルで最初に記述されている init は, Inventory の
+ 以下のモデルで最初に記述されている init は,Inventory の
構造を持った its 初期化するという操作になっています.
- 次の, itemRegistraction では初めて取り扱う商品を入荷する際に,
+ 次の,itemRegistraction では初めて取り扱う商品を入荷する際に,
商品名と入荷数量を Inventory に登録するという操作になっています.
その次にある, receivingOrShipping では登録されている商品に対して
入荷か出荷を行った際に起こる数量の変化の操作を表しています.
最後の execute では上記にて説明を行った,
- init , itemRegistraction , receivingOrShipping を
+ init ,itemRegistraction ,receivingOrShipping を
上から順番に実行を進めるという操作になっています.
- そして,最後にある runexecute を呼び出して実行を行っています.
+ そして,最後にある runexecute を呼び出して実行を行っています.
この実行の際に や - の数字を扱うため,
末尾に という
Alloyで8bitの数字を扱うことができるようにするための記述を行っています.
diff --git a/courseA/IM_DTRAM.html b/courseA/IM_DTRAM.html
index 3fb08f4..3f4700d 100644
--- a/courseA/IM_DTRAM.html
+++ b/courseA/IM_DTRAM.html
@@ -1,173 +1,211 @@
- 本課題では,SimpleTwitterプログラムにアカウント名を変更可能にする機能追加を行っていただきます.
+ ここでは,DTRAMを用いて記述したInventoryManagementの課題について説明します.
+ 以下にInventoryManagementのモデルを示します.こちらを適宜参照しながらモデルの理解を行ってください.
- このSSDStoreプログラムが,サイトA以外のサイトからも商品情報を収集して扱えるようにすることを考えます.
+ 以下のモデルでは始めに,新規に取り扱う商品を入荷する時に使用されるイベントチャンネル,ItemRegistraction を宣言しています.
+ 次にある,ReceivingOrShipping(itemId: は itemId を用いて
+ 登録されている商品に対して出荷か入荷を行う時に使用されるイベントチャンネルになります.
++channel ItemRegistration { +out inventory(itemDB:Map , registerItem(itemId:Str , itemName:Str , quantity:Int )) = insert(itemDB, itemId, {"count": quantity, "name": itemName}) +} + +channel ReceivingOrShipping(itemId:Str ) { +out inventory.{itemId}.count(prev_quantity:Int , receiveOrShip(quantity:Int )) = prev_quantity + quantity +} +
- 以下では,リファクタリングに要した時間を測っていただきますので,お手元に時計をご用意ください.
- 時間計測にあたって,急いで作業していただく必要はまったくありません.
- 最初の課題から最後の課題まで一定のペースを保てるよう, 正しくリファクタリングを行うことを意識してください.
- 開発環境を立ち上げてソースコードの確認をしていただいて構いませんが,ソースコードの変更は時間計測の準備ができるまで行わないで下さい.
- まずは、以下の作業手順を一通り読んでから作業を開始してください.
-
- 現在の設計では,以下のクラス図ように ItemsByPrice オブジェクトと ItemsByCapacity オブジェクトが,それぞれ SiteA オブジェクトから直接SSDの商品情報をPULL型のデータ転送で取得し,
- さらに Price オブジェクトから価格を,Capacity オブジェクトから容量をPULL型のデータ転送で取得して,それらの値を使って別々に検索を行い検索結果を出力しています.
+ 先ほどのInventoryManagementを,DTRAMの可視化ツールを使用して,モデルを可視化した図が以下の通りになります.


- 具体的には以下のコードように,ItemsByPrice オブジェクトの getValue() メソッド内部で,サイトAからSSDのリストを取得してその中から Price オブジェクトで指定された価格以下の商品を検索し,
- 同様に ItemsByCapacity オブジェクトの getValue() メソッド内部で,サイトAからSSDのリストを取得してその中から Capacity オブジェクトで指定された容量以上の商品を検索しています.
-
-public class ItemsByPrice {
- private Price price;
- private SiteA siteA;
- :
- public double getValue() {
- List<Map<String, Object>> temp_l1 = new ArrayList<>();
- {
- for (Map<String, Object> item: this.siteA.getValue()) {
- if ((Integer) item.get("price") <= this.price.getValue()) {
- temp_l1.add(item);
- }
- }
- }
- return temp_l1;
- }
-}
-
-
-public class ItemsByCapacity {
- private Capacity capacity;
- private SiteA siteA;
- :
- public double getValue() {
- List<Map<String, Object>> temp_l1 = new ArrayList<>();
- {
- for (Map<String, Object> item: this.siteA.getValue()) {
- if ((Integer) item.get("capacity") >= this.capacity.getValue()) {
- temp_l1.add(item);
- }
- }
- }
- return temp_l1;
- }
-}
-
-
- ここで,このSSDStoreプログラムがサイトBからも商品情報を収集して扱えるように拡張することを考えた場合,ItemsByPrice オブジェクトと ItemsByCapacity オブジェクトの両方の実装を,
- SiteA オブジェクトと SiteB オブジェクトを同時に扱えるように書き換えなければならなくなります.
- 今後,より多くのサイトを扱えるように拡張していくことを考えると,このように ItemsByPrice オブジェクトと ItemsByCapacity オブジェクトが直接,個々のサイトのオブジェクトを参照しているような現在の設計では,拡張作業が煩雑になってしまいます.
+ まず,始めに商品全体を管理する倉庫を表している inventory というリソースがあります.
+ 次に,その下の階層に inventory リソースを親にしている,inventory.{itemId} という子リソースがあります.
+ この子リソースは,商品を識別するためのIDを表す itemId という
+ パスパラメータがあるので,一意なリソース(商品)を特定することができます.
+ そして,最後に inventory.{itemId} リソースを親にしている,inventory.{itemId}.count という子リソースがあり,特定の商品の在庫数量を表しています.
- そこで,以下のクラス図のように複数のサイトを同時に参照することができる SiteWrapper オブジェクトを新たに導入し,
- ItemsByPrice オブジェクトと ItemsByCapacity オブジェクトが,SiteWrapper オブジェクトを通じて,間接的に SiteA オブジェクトや SiteB オブジェクトにアクセスするように設計変更を行います.
- そうすることによって,SiteWrapper にいくつサイトを追加しても,ItemsByPrice オブジェクトや ItemsByCapacity オブジェクトの実装に影響が及ばないようにすることができます.
+ ここでは,InventoryManagementの仮想実行について説明します.InventoryManagementの仮想実行で用いるテストケースは次の通りです.
+
+ 先ほどの仮想実行を可視化したものを以下に示していきます.
+ まず,システムの初期状態を可視化したものが以下の図です.
+


- 具体的に変更後の設計の中では,以下のように SiteWrapper クラスが SiteA を参照し,
- ItemsByPrice オブジェクトと ItemsByCapacity オブジェクトは,この SiteWrapper の getSiteValue() メソッドを呼び出して,最新のSSDの一覧を得るようにします.
- そして,新しいサイトを追加する際は,この SiteWrapper クラスを変更するようにします.
+ 初期状態のため,inventory リソースには何の商品も登録されていないという状態になっています.
+ 次に,テストケースの1を実行していくので,inventory リソースをダブルクリックします.
-public class SiteWrapper {
- private SiteA siteA;
- public SiteWrapper(SiteA siteA) {
- this.siteA = siteA;
- }
- public List<Map<String, Object>> getSiteValue() {
- return this.siteA.getValue();
- }
-}
-
+
+
+ ダブルクリックすると,registerItem というメッセージが選択できるので,こちらを選択します.
+

+ 次に,inventory リソースに対して,商品のIDを表す itemId と
+ 商品名を表す itemName,入荷数量を表す quantity を入力できる画面が表示されます.
+

+ ここでは,inventory リソースに対してregisterItem(@123, "Asahi", 100)というメッセージを入力し,実行します.
+

+ 実行した結果,次の状態に遷移することができたので,固有のID(@123)の状態を持ったinventory.@123 と
+ 在庫数量が100の状態を持ったinventory.@123.count,商品名がAsahiの状態を持った inventory.@123.name という
+ 3つのリソースが表示されました.
+ 次に,テストケースの2を実行していきますので,inventory.@123.countリソースをダブルクリックします.
+

+ ダブルクリックすると,メッセージを選択する画面が先ほどと同様に表示されますので,出荷と入荷の両方を行うことができる receiveOrShip を選択します.
+

+ 次に,出荷数量,または入荷数量を入力可能な画面が表示されますので,receiveOrShip(-50) と入力して実行します.
+

+ 次の状態に遷移したため,inventory.@123.name リソースの状態が50に遷移したことが確認できました.
+
- 本課題では,リファクタリングに要した時間を測っていただきますので,お手元に時計をご用意ください.
- 時間計測にあたって,急いで作業していただく必要はまったくありません.
- 最初の課題から最後の課題まで一定のペースを保てるよう, 正しくリファクタリングを行うことを意識してください.
- 課題に着手する前に開発環境を立ち上げて現状のソースコードの確認をしていただいて構いませんが,実際のソースコードの変更は時間計測の準備ができるまで行わないで下さい.
+ 本課題ではまず,上記にて説明を行ったInventoryManagementに,とある機能を追加した時のモデルと可視化の図を
+ 実験参加者の皆様に見て頂きます.
+ 次に,その2つを見てどの様な機能が追加されたのか,またどの様なシナリオになっているのかを
+ 考えて頂き,以下のアンケートにお答えください.
++channel ItemRegistration { + out inventory(itemDB:Map , registerItem(itemId:Str , itemName:Str , quantity:Int )) = insert(itemDB, itemId, {"count": quantity, "name": itemName}) +} + +channel Receiving(itemId:Str ) { + out inventory.{itemId}.count(prev_quantity:Int , receive(quantity:Int )) = prev_quantity + quantity +} + +channel Shipping(itemId:Str ) { + out inventory.{itemId}.count(prev_quantity:Int , ship(quantity:Int )) = prev_quantity - quantity +} + +

- 作業に着手する前に,main ブランチから,メッセージでお伝えした自分専用のブランチ(user??Refactor)を新規作成して,一度 push を行ってください.
- push を行った後,開発環境の準備ができれば,時間計測を開始してください. 時間計測はできる限り,30秒以内の単位での計測をお願いします.
- ソースコードの変更作業は上記「SSDStore のリファクタリングの概要」にしたがって進めてください.
- テストプログラムTestSSDStoreUpdate.javaが正しく動作するまでは作業完了とは見なされないので注意してください.
-
- リファクタリングの作業が完了したら作業時間を記録し,その後,作業結果を自分専用のブランチに commit & push してください.
- ただし,main ブランチには決して merge をしないように,また自分専用のブランチを決して削除しないように注意してください.
- push 後に,以下のアンケートにお答えください.
-
- アンケートフォーム (別タブが開きます)
+
+ 課題アンケート (別タブが開きます)
+
+
+
+
+
+ 課題終了後の評価アンケート (別タブが開きます)