diff --git a/courseA/IM_Alloy.html b/courseA/IM_Alloy.html index f01d24b..de4a6b2 100644 --- a/courseA/IM_Alloy.html +++ b/courseA/IM_Alloy.html @@ -18,37 +18,35 @@ 【InventoryManagement(Alloy)の課題】

- ここでは，Alloyを用いて記述したInventoryManagementの課題について説明します．
- 以下にInventoryManagementのモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください． + ここでは，InventoryManagementのAlloyによる仕様記述の課題に取り組んでいただきます．
+ 以下にAlloyで記述されたInventoryManagementのモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．

InventoryManagementのAlloyによる記述についての説明

sig:

- 以下のモデルでは始めに，商品を識別するためのIDを表す ItemId と商品名を表す Name を集合として宣言しています．
- 次に，商品全体を管理する倉庫を表している Inventory は，itemDB フィールドを持っています． - このフィールドを定義している行では，itemDB フィールドが ItemId から， - 商品の情報を表す Item との対応関係を参照していることを表しています．
- 最後の Item では始めに，商品名を表す name を Item の要素と，Name の要素の間の関係として定義しています． - 次にある，在庫数を表す count では在庫数を Int 型で表すように定義を行っています．
+ 以下のモデルでは始めに，商品IDの集合を表す ItemId と商品名の集合を表す Name を宣言しています．
+ 次に，商品全体を保管する倉庫の集合を表す Inventory を宣言しています．Inventory には，ItemId から + 商品情報を表す Item への対応関係がitemDB フィールドとして定義されています．
+ 最後の Item では，商品名を表す name が Name のインスタンスとして， + 在庫数を表す count が Int のインスタンスとして定義されています．

pred:

- 以下のモデルで最初に記述されている init は，Inventory の - 構造を持った its 初期化するという操作になっています．
- 次の，itemRegistraction では初めて取り扱う商品を入荷する際に， - 商品名と入荷数量を Inventory に登録するという操作になっています．
- その次にある， receivingOrShipping では登録されている商品に対して - 入荷か出荷を行った際に起こる数量の変化の操作を表しています．
- 最後の execute では上記にて説明を行った， - init ，itemRegistraction ，receivingOrShipping を - 上から順番に実行を進めるという操作になっています．
- そして，最後にある run では，execute を呼び出して実行を行っています． - この実行の際に 100 や -50 の数字を扱うため， - 末尾に 8 Int という - Alloyで8bitの数字を扱うことができるようにするための記述を行っています． + 最初の述語として記述されている init は，Inventory の + インスタンスである its が初期化されているという条件を満たしていることを示しています．
+ 次の，itemRegistration は itemId で示された商品を登録する前の Inventory のインスタンス its と + 登録した後のインスタンス its' の関係を述語として定義しています．
+ ここで quantity は初期数量，n は商品名を示しています．
+ receivingOrShipping ではitemId で登録されている商品に対して + 入荷か出荷を行った際の操作前の Inventory のインスタンス its と操作後のインスタンス its' の関係を述語として定義しています．
+ ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
+ 最後の execute では，init ，itemRegistraction ，receivingOrShipping を + この順で呼び出す操作を定義しています．
+ run では，execute を呼び出して実行を行います． + この実行の際に，Int で8bitの数字を扱うことができるよう末尾に 8 Int という記述を行っています．

@@ -99,40 +97,44 @@

モデルの可視化

- 先ほどのInventoryManagementを，Alloyの可視化ツールを使用して，モデルを可視化した図が以下の通りになります．
+ 先ほどのInventoryManagementのモデルの構造を，Alloyの可視化ツールを使用して，可視化したものを以下の図に示します．


- Inventory が，商品名を表す name と在庫数を表す count の２つのフィールドを持っている， - Item を管理するというモデルになっています． + この図がモデルの実行に依らない，モデルそのものが持つ構造を表していることに注意して下さい．
+ Inventory が，ItemId のインスタンスを Item のインスタンスに対応させる itemDB という + フィールドを持っており，Item が Name のインスタンスを参照する name フィールドと， + Int のインスタンスを参照する count フィールドを持っていることがわかります．

-

InventoryManagementの仮想実行について

+

InventoryManagementモデルの仮想実行について

- ここでは，InventoryManagementの仮想実行について説明します．InventoryManagementの仮想実行で用いるテストケースは次の通りです．
+ ここでは，InventoryManagementモデルの仮想実行について説明します．InventoryManagementの仮想実行で用いるテストケースは次の通りです．

    -
  1. Inventoryに新しく取り扱う商品を100個入荷します．
    2. -
  2. お客様が商品を50個購入してくれたので，在庫数が50個に減少しました．
    3. +
  3. Inventoryに新しく取り扱う商品を初期数量100で登録します．
    4. +
  4. 登録した商品を50個出荷します．

仮想実行の可視化:

- 先ほどの仮想実行を可視化したものを以下に示します．
+ このテストケースはモデル中の execute 述語で実装されています．
+ execute の仮想実行を可視化したものを以下に示します．


- 左下にあるInventory2($execute_its)は，始めに init が実行された時の状態になっているため， - まだ何の商品(Item)も登録されていない状態になっています．
- 次に，1番上の段の左にあるInventory1($execute_its')はテストケースの１が行われた時の状態になっているため， - 100個のItem1を入荷している状態になっています．
- そして，Inventory1の右にあるInventory0($execute_its'')ではテストケース２が行われた時の状態になっているため， - 在庫数が50個に減少しています． + 左下にあるInventory2($execute_its)は execute 述語中の変数 its で参照される Inventory のインスタンスであり， + init 述語を満たしているため，まだ何の商品(Item)も登録されていない状態になっています．
+ 次に，1番上の段の左にあるInventory1($execute_its')は変数 its' で参照されるインスタンスで， + its で参照されるインスタンスに対して itemId で参照される Item のインスタンスを初期数量100個で登録したインスタンスになっています．
+ そして，Inventory1の右にあるInventory0($execute_its'')はitemId で参照される Item のインスタンスを50個出荷したインスタンスになっているため， + 在庫数が50個に減少しています．
+ ここで出荷前の Item のインスタンス(Item1)と出荷後のインスタンス(Item0)が別々のインスタンスになっていることに注意して下さい．

@@ -140,10 +142,10 @@ 課題概要

- 本課題ではまず，上記にて説明を行ったInventoryManagementに，とある機能を追加した時のモデルと可視化の図を - 実験参加者の皆様に見て頂きます．
- 次に，その２つを見てどの様な機能が追加されたのか，またどの様なテストケースになっているのかを - 考えて頂き，以下のアンケートにお答えください． + 本課題ではまず，上記にて説明を行ったInventoryManagementに，ある機能を追加したモデルとその仮想実行を可視化した以下の図を見ていただき， + ２つの設問に答えていただきます．
+ 必ず設問１，設問２の順番でご解答下さい．
+ 以下の図は設問のページにも記載されているページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．