(******************************************************************************
* STOCK.lib:
* stocks held by suppliers and stores in the stock management example
* Products are represented by natural numbers, and a store is a set of pairs
* (p, n) meaning that n items of product number p are available
*****************************************************************************)
type STOCK is
NATURAL, BOOLEAN
sorts Stock
opns
(* constructors: the set is implemented as a list *)
empty (*! constructor *) : -> Stock
cons (*! constructor *) : Nat, Nat, Stock -> Stock
(* operations *)
isAvailable : Nat, Nat, Stock -> Bool
decrease : Nat, Nat, Stock -> Stock
increase : Nat, Nat, Stock -> Stock
extract : Stock -> Nat
eqns
(* Each operation is defined by three equations, describing a recurisve
* traversal of the list. The first equation describes the terminal case,
* the second corresponds to the handling of the case where the product
* has been found, and the third equation describes the recursive call
*)
forall id, id1, id2 : Nat,
q, q1, q2 : Nat,
s : Stock
ofsort Bool
isAvailable (id, q, empty) = false;
isAvailable (id1, q1, cons (id1, q2, s)) = (q2 >= q1);
isAvailable (id1, q1, cons (id2, q2, s)) = isAvailable (id1, q1, s);
ofsort Stock
(* decrease(id, q, empty) is undefined and raises an error *)
decrease (id1, q1, cons (id1, q2, s)) = cons (id1, q2 - q1, s);
decrease (id1, q1, cons (id2, q2, s)) = decrease (id1, q1, s);
ofsort Stock
(* increase(id, q, empty) is undefined and raises an error *)
increase (id1, q1, cons (id1, q2, s)) = cons (id1, q1 + q2, s);
increase (id1, q1, cons (id2, q2, s)) = increase (id1, q1, s);
ofsort Nat
extract (empty) = 0;
(* default product zero *)
extract (cons (id, 0, s)) = id;
extract (cons (id, q, s)) = extract (s);
endtype