+
- 本課題では，SimpleTwitterプログラムにアカウント名を変更可能にする機能追加を行っていただきます．
+ ここでは，Alloyを用いて記述したInventoryManagementについて説明します．
+ 以下にInventoryManagementのソースコードを示します．こちらを適宜参照しながらソースコードの理解を行ってください．
sig
- このSSDStoreプログラムが，サイトA以外のサイトからも商品情報を収集して扱えるようにすることを考えます．
+ 以下のソースコードでは始めに，内部構造を持たない集合として商品を識別するためのIDを表すItemIdと 商品名を表すNameを宣言しています．
+ 次に，商品全体を管理する倉庫を表しているInventoryは，itemDBフィールドを持っています．
+ そして，このフィールドを定義している行では，itemDBフィールドがItemIdから，
+ 具体的な商品の情報を表すItemという集合への対応関係を参照していることを表しています．
+ 最後のItemでは始めに，商品名を表すnameをItemの要素と，Nameの要素の間の関係として定義しています．
+ 次の，在庫数を表すcountでは在庫数をInt
pred
+ 以下のソースコードで最初に記述されているinitは，Inventoryの
+ 内部構造を持ったits初期化するという操作になっています．
+ 次の，itemRegistractionでは初めて取り扱う商品を入荷する際に，
+ 商品名と入荷数量をInventoryに登録するという操作になっています．
+ その次にある，receivingOrShippingでは登録されている商品に対して
+ 入荷か出荷を行った際に起こる数量の変化の操作を表しています．
+ 最後のexecuteでは上記にて説明を行った，
+ init，itemRegistraction，receivingOrShippingを
+ 上から順番に実行が進むという操作になっています．
+ そして，最後にあるrunexecuteを呼び出して実行を行っています．
+ この実行の際に
++sig ItemId, Name{} +sig Inventory { + itemDB: ItemIdlone ->lone Item +} +sig Item { + name : Name, + count:Int +} + +pred init[its: Inventory] { +no its.itemDB +} + +pred itemRegistration[its, its': Inventory, itemId: ItemId, quantity:Int , n: Name] { +some it: Item | { +no itemId2: ItemId | its.itemDB[itemId2] = it + its'.itemDB = its.itemDB + itemId -> it + it.name = n + it.count = quantity + } +} + +pred receivingOrShipping[its, its': Inventory, itemId: ItemId, quantity:Int ] { +some it': Item | { +no itemId2: ItemId | its.itemDB[itemId2] = it' + its'.itemDB = its.itemDB ++ itemId -> it' + it'.name = its.itemDB[itemId].name + it'.count = plus[its.itemDB[itemId].count, quantity] + } +} + +pred execute[] { +some disj its, its', its'': Inventory, itemId: ItemId, n: Name | { + init[its] + itemRegistration[its, its', itemId,100 , n] + receivingOrShipping[its', its'', itemId, -50 ] + } +} + +run executefor 2 but3 Inventory,8 Int +
- 以下では，リファクタリングに要した時間を測っていただきますので，お手元に時計をご用意ください．
- 時間計測にあたって，急いで作業していただく必要はまったくありません．
- 最初の課題から最後の課題まで一定のペースを保てるよう, 正しくリファクタリングを行うことを意識してください．
- 開発環境を立ち上げてソースコードの確認をしていただいて構いませんが，ソースコードの変更は時間計測の準備ができるまで行わないで下さい．
- まずは、以下の作業手順を一通り読んでから作業を開始してください．
-
- 現在の設計では，以下のクラス図ように ItemsByPrice オブジェクトと ItemsByCapacity オブジェクトが，それぞれ SiteA オブジェクトから直接SSDの商品情報をPULL型のデータ転送で取得し，
- さらに Price オブジェクトから価格を，Capacity オブジェクトから容量をPULL型のデータ転送で取得して，それらの値を使って別々に検索を行い検索結果を出力しています．
+ 先ほどのInventoryManagementを，Alloyの可視化ツールを使用して，モデルを可視化した図が以下の通りになります．
- 具体的には以下のコードように，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が，商品名を表すnameと在庫数を表すcountの情報を持った，
+ Itemを管理するというモデルになっています．
- そこで，以下のクラス図のように複数のサイトを同時に参照することができる SiteWrapper オブジェクトを新たに導入し，
- ItemsByPrice オブジェクトと ItemsByCapacity オブジェクトが，SiteWrapper オブジェクトを通じて，間接的に SiteA オブジェクトや SiteB オブジェクトにアクセスするように設計変更を行います．
- そうすることによって，SiteWrapper にいくつサイトを追加しても，ItemsByPrice オブジェクトや ItemsByCapacity オブジェクトの実装に影響が及ばないようにすることができます．
+ ここでは，InventoryManagementの，例題仕様について説明します．InventoryManagementの例題仕様は次の通りです．
+
+ 先ほどの例題仕様で，実行時の状態を可視化したものを以下に示します．
- 具体的に変更後の設計の中では，以下のように SiteWrapper クラスが SiteA を参照し，
- ItemsByPrice オブジェクトと ItemsByCapacity オブジェクトは，この SiteWrapper の getSiteValue() メソッドを呼び出して，最新のSSDの一覧を得るようにします．
- そして，新しいサイトを追加する際は，この SiteWrapper クラスを変更するようにします．
+ 左下にあるInventory2($execute_its)は，始めにinitが実行された時の状態になっているため，
+ まだ何の商品(Item)も登録されていない状態になっています．
+ 次に，1番上の段の左にあるInventory1($execute_its')はテストケースの１が行われた時の状態になっているため，
+ 100個のItem1を入荷している状態になっています．
+ そして，Inventory1の右にあるInventory0($execute_its'')ではテストケース２が行われた時の状態になっているため，
+ 在庫数が50個に減少しています．
-public class SiteWrapper {
- private SiteA siteA;
- public SiteWrapper(SiteA siteA) {
- this.siteA = siteA;
- }
- public List<Map<String, Object>> getSiteValue() {
- return this.siteA.getValue();
- }
-}
-
-
- 本課題では，リファクタリングに要した時間を測っていただきますので，お手元に時計をご用意ください．
- 時間計測にあたって，急いで作業していただく必要はまったくありません．
- 最初の課題から最後の課題まで一定のペースを保てるよう, 正しくリファクタリングを行うことを意識してください．
- 課題に着手する前に開発環境を立ち上げて現状のソースコードの確認をしていただいて構いませんが，実際のソースコードの変更は時間計測の準備ができるまで行わないで下さい．
+ 本課題ではまず，上記にて説明を行ったInventoryManagementに，とある機能を追加した時のソースコードと可視化の図を
+ 実験参加者の皆様に見て頂きます．
+ 次に，その２つを見てどの様な機能が追加されたのか，またどの様なシナリオになっているのかを
+ 考えて頂き，以下のアンケートにお答えください．
++sig ItemId, Name{} +sig Inventory { + itemDB: ItemIdlone ->lone Item +} +sig Item { + name : Name, + count:Int +} + +pred init[its: Inventory] { +no its.itemDB +} + +pred itemRegistration[its, its': Inventory, itemId: ItemId, quantity:Int , n: Name] { +some it: Item | { +no itemId2: ItemId | its.itemDB[itemId2] = it + its'.itemDB = its.itemDB + itemId -> it + it.name = n + it.count = quantity + } +} + +pred shippingOrReceiving[its, its': Inventory, itemId: ItemId, quantity:Int ] { + plus[its.itemDB[itemId].count, quantity] <0 implies { +all itemId': ItemId | its'.itemDB[itemId'] = its.itemDB[itemId'] + } +else { +some it': Item | { +no itemId2: ItemId | its.itemDB[itemId2] = it' + its'.itemDB = its.itemDB ++ itemId -> it' + it'.name = its.itemDB[itemId].name + it'.count = plus[its.itemDB[itemId].count, quantity] + } + } +} + +pred execute[] { +some disj its, its', its'', its''': Inventory, itemId: ItemId, n: Name | { + init[its] + itemRegistration[its, its', itemId,100 , n] + shippingOrReceiving[its', its'', itemId, -50 ] + shippingOrReceiving[its'', its''', itemId, -75 ] + } +} + +run executefor 2 but 4 Inventory,8 Int +
- 作業に着手する前に，main ブランチから，メッセージでお伝えした自分専用のブランチ（user??Refactor）を新規作成して，一度 push を行ってください．
- push を行った後，開発環境の準備ができれば，時間計測を開始してください. 時間計測はできる限り，30秒以内の単位での計測をお願いします.
- ソースコードの変更作業は上記「SSDStore のリファクタリングの概要」にしたがって進めてください．
- テストプログラムTestSSDStoreUpdate.javaが正しく動作するまでは作業完了とは見なされないので注意してください．
-
- リファクタリングの作業が完了したら作業時間を記録し，その後，作業結果を自分専用のブランチに commit ＆ push してください．
- ただし，main ブランチには決して merge をしないように，また自分専用のブランチを決して削除しないように注意してください．
- push 後に，以下のアンケートにお答えください．
-
- アンケートフォーム (別タブが開きます)
+
+ 課題アンケート (別タブが開きます)
+
+
+
+
+
+ 課題終了後の評価アンケート (別タブが開きます)