sig
以下のモデルでは始めに，商品を識別するためのIDを表す ItemId と商品名を表す Name を集合として宣言しています．
- 次に，商品全体を管理する倉庫を表している Inventory は， itemDB フィールドを持っています．
- このフィールドを定義している行では， itemDB フィールドが ItemId から，
+ 次に，商品全体を管理する倉庫を表している Inventory は，itemDB フィールドを持っています．
+ このフィールドを定義している行では，itemDB フィールドが ItemId から，
商品の情報を表す Item との対応関係を参照していることを表しています．
- 最後の Item では始めに，商品名を表す name を Item の要素と， Name の要素の間の関係として定義しています．
+ 最後の Item では始めに，商品名を表す name を Item の要素と，Name の要素の間の関係として定義しています．
次にある，在庫数を表す count では在庫数を Int
pred
- 以下のモデルで最初に記述されている init は， Inventory の
+ 以下のモデルで最初に記述されている init は，Inventory の
構造を持った its 初期化するという操作になっています．
- 次の， itemRegistraction では初めて取り扱う商品を入荷する際に，
+ 次の，itemRegistraction では初めて取り扱う商品を入荷する際に，
商品名と入荷数量を Inventory に登録するという操作になっています．
その次にある， receivingOrShipping では登録されている商品に対して
入荷か出荷を行った際に起こる数量の変化の操作を表しています．
最後の execute では上記にて説明を行った，
- init ， itemRegistraction ， receivingOrShipping を
+ init ，itemRegistraction ，receivingOrShipping を
上から順番に実行を進めるという操作になっています．
- そして，最後にある runexecute を呼び出して実行を行っています．
+ そして，最後にある runexecute を呼び出して実行を行っています．
この実行の際に - の数字を扱うため，
末尾に