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