Back - Formal Specification | Previous - Weather Map

Tutorial Solutions - Warehouse Stock Control

 

Provide a summary for each schema below, see newly named Schema.

ÚÄWarehouseÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
carried : ITEM
level : ITEM
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
dom level = carried
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄInitWarehouseÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
Warehouse
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
carried = í
level = í
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

Schema One - allows for the withdrawal of a number of a specific item of stock.

ÚÄWithdrawalÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
Warehouse
i? : ITEM
qty? :
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
i? î carried
level i? ò qty?
level' = level Å {i? level i? - qty?}
carried' = carried
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

Schema Two - discontinues holding a specific item of stock.

ÚÄDiscontinueÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
Warehouse
i? : ITEM
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
i? î carried
level i? = 0
level' = i? level
carried' = carried \ i?
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ