diff --git a/courseC/IM_Alloy_C.html b/courseC/IM_Alloy_C.html new file mode 100644 index 0000000..3b7950f --- /dev/null +++ b/courseC/IM_Alloy_C.html @@ -0,0 +1,256 @@ + + + + + + 【InventoryManagement(Alloy)】 + + +

+ 【InventoryManagement(Alloy) の課題】 +

+

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

+
+ +

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

+

sig:

+

+ Alloy では，商品id の集合を ItemId，商品名の集合を Name， + 商品全体を保管する倉庫の集合を Inventory，商品の集合を Item で表します．
+ 以下のモデルでは sig を用いて，ItemId，Name，Inventory，Item の順番にこれらの集合を宣言しています．
+ Inventory には，ItemId から Item への対応関係が itemDB フィールドとして定義されています．
+ ここで，ItemId の右側の lone は１つの Item に対応する ItemId がたかだか１つしかないことを示しています．
+ Item の宣言では，商品名を表す name が Name のインスタンスとして， + 在庫数を表す count が Int のインスタンスとして定義されています．
+

+ +

pred:

+

+ 最初の述語として記述されている init は，Inventory の + インスタンスである its が初期化されていることを示しています．
+ 次の itemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と， + 登録した後のインスタンス its' の関係を述語として定義しています．ここで quantity は初期数量，n は商品名を示しています．
+ また，述語定義中の some it: Item は，its のデータベースに登録されていない Item のインスタンス it が存在していることを示しており， + 直観的には Item のインスタンスの生成を示しています．
+ receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と， + 操作後のインスタンス its' の関係を述語として定義しています．ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
+ また，述語定義中の some it': Item は，its のデータベースに登録されていない Item のインスタンス it' が存在していることを示しており， + 直観的には，Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．
+ 最後の execute では，init ，itemRegistraction ，receivingOrShipping を + この順で呼び出す操作を定義しています．
+ run では，execute を呼び出して仮想実行を行います． + この実行の際に，Int で8bitの整数を扱うことができるよう末尾に 8 Int という記述を付け加えています． +

+ +
+ 
+sig ItemId, Name{}
+sig Inventory {
+	itemDB: ItemId lone -> 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 execute for 2 but 3 Inventory, 8 Int
+
+
+
+ +

モデルの可視化

+

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

+
+
+
+

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

+
+ +

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

+

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

    +
  1. Inventoryに新しく取り扱う商品を初期数量100で登録します．
    2. +
  2. 登録した商品を50個出荷します．
    3. +
+

+ +

仮想実行の可視化:

+

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

+
+
+
+

+ 左下にある Inventory2($execute_its) は execute 述語中の変数 its で参照される Inventory のインスタンスであり，init 述語を満たしているため， + まだ何の商品(Item)も登録されていない状態になっています．
+ 次に，1番上の段の左にある Inventory1($execute_its') は変数 its' で参照される Inventory のインスタンスで， + its で参照される Inventory のインスタンスに対して，Item のインスタンス Item1(itemRegistration_it) を初期数量100個で登録したインスタンスになっています．
+ Inventory1 の右にあるInventory0($execute_its'') は少し複雑です．
+ まず，Inventory1 において，ItemId で参照される Item のインスタンスは Item1 です．このインスタンスに対して50個出荷した後の Item のインスタンスが Item0 になります．
+ ここで Item0 の在庫数が50個に減少していることに注意して下さい．
+ ItemId で参照される Item のインスタンスが Item1 から Item0 に変わるので，Inventory のインスタンスも Inventory1 から Inventory0 に変わります． +

+
+ +

+ 課題概要 +

+

+ ここからが課題です．
+ 本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
+ その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ 設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません． +

+
+
+sig ItemId, Name{}
+sig Inventory {
+	itemDB: ItemId lone -> 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 shipping[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 = minus[its.itemDB[itemId].count, quantity]
+	}
+}
+
+pred receiving[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'', its''': Inventory, itemId: ItemId, n: Name | {
+		init[its]
+		itemRegistration[its, its', itemId, 100, n]
+		shipping[its', its'', itemId, 50]
+		receiving[its'', its''', itemId, 25]
+	}
+}
+
+run execute for 2 but 4 Inventory, 3 Item, 8 Int
+
+
+ +
+
+
+ +

+ + + 課題アンケート (別タブが開きます) + + +
+ + + 課題終了後の評価アンケート (別タブが開きます) + + +

+ +
+
+【STの説明】へ + + + + +