REFINEMENT VendingMachine_r2 REFINES VendingMachine_r1 SEES Product ABSTRACT_CONSTANTS initial_stock PROPERTIES initial_stock : PRODUCT --> NATURAL1 VARIABLES stock0 INVARIANT stock0 : PRODUCT --> NATURAL & stock = stock0 |>> {0} & /* * Additional invariant needed for correctness of restock refinement. */ !pp . (pp : PRODUCT => stock0(pp) <= initial_stock(pp)) INITIALISATION stock0 := initial_stock || credit := 0 || state := off OPERATIONS status <-- dispense (item) = PRE state = on & item : PRODUCT THEN IF stock0(item) > 0 & credit >= price(item) THEN status := TRUE || credit := credit - price(item) || stock0(item) := stock0(item) - 1 ELSE status := FALSE END END ; restock = PRE state = off THEN stock0 := initial_stock END END