@@ -67,27 +67,27 @@
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
+
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]
+
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]
+ init[its]
+ itemRegistration[its, its', itemId,
100, n]
+ receivingOrShipping[its', its'', itemId, -
50]
}
}
@@ -123,7 +123,7 @@
仮想実行の可視化:
このテストケースはモデル中の execute 述語で実装されています．
- execute の仮想実行を可視化したものを以下に示します．
+ execute の実行を可視化したものを以下に示します．
@@ -131,10 +131,10 @@
左下にある Inventory2($execute_its) は execute 述語中の変数 its で参照される Inventory のインスタンスであり，init 述語を満たしているため，
まだ何の商品(Item)も登録されていない状態になっています．
- 次に，1番上の段の左にある Inventory1($execute_its') は変数 its' で参照されるインスタンスで，
- its で参照されるインスタンスに対して，itemId で参照される Item のインスタンスを初期数量100個で登録したインスタンスになっています．
+ 次に，1番上の段の左にある Inventory1($execute_its') は変数 its' で参照される Inventory のインスタンスで，
+ its で参照される Inventory のインスタンスに対して，Item のインスタンス Item1(itemRegistration_it) を初期数量100個で登録したインスタンスになっています．
Inventory1 の右にあるInventory0($execute_its'')は少し複雑です．
- まず，Inventory1 において，ItemId で参照される Item のインスタンスは Item1 です．このインスタンスに対して50個出荷した後の Item のインスタンスは Item0 になります．
+ まず，Inventory1 において，ItemId で参照される Item のインスタンスは Item1 です．このインスタンスに対して50個出荷した後の Item のインスタンスが Item0 になります．
ここで Item0 の在庫数が50個に減少していることに注意して下さい．
ItemId で参照される Item のインスタンスが Item1 から Item0 に変わるので，Inventory のインスタンスも Inventory1 から Inventory0 に変わります．
@@ -144,8 +144,10 @@
課題概要
+ ここからが課題です．
本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
- その仕様のモデルと，仮想実行を可視化した以下の図を見ていただいた上で，２つの設問にお答えいただきます．
+ その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ なお，以下のモデル中にある implies はその前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．
@@ -165,9 +167,9 @@
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
+ no itemId2: ItemId | its.itemDB[itemId2] = it
+ its'.itemDB = its.itemDB + itemId -> it
+ it.name = n
it.count = quantity
}
}
@@ -178,20 +180,20 @@
}
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]
+ 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]
+ init[its]
+ itemRegistration[its, its', itemId, 100, n]
+ shippingOrReceiving[its', its'', itemId, -50]
+ shippingOrReceiving[its'', its''', itemId, -75]
}
}