(******************************************************************************
* BOOKSTORE.lib: data type of bookstores for the book auction example
*
* Bookstores are sets of triples , represented as lists, where
* - book is a book (cf BOOK.lib),
* - q is the number of available copies of the book, and
* - inv is the invariant associated to the book (cf INVARIANT.lib)
*****************************************************************************)
type BOOKSTORE is
NATURAL, BOOLEAN, BOOK, INVARIANT
sorts BookStore
opns
(* constructors *)
emptyBS (*! constructor *) : -> BookStore
addBS (*! constructor *) : Book, Nat, Inv, BookStore -> BookStore
(* operations *)
retrieveInv : Nat, BookStore -> Inv
retrievePrice : Nat, BookStore -> Nat
isAvailable : Nat, BookStore -> Bool
isIn : Nat, BookStore -> Bool
decrease : Nat, Nat, BookStore -> BookStore
eqns
(* Each operation is defined by three equations, describing a recursive
* traversal of the list. The first equation describes the terminal case,
* the second corresponds to the handling of the case where the book
* has been found, and the third equation describes the recursive call
*)
forall r, q, q1, q2 : Nat,
b, b1 : Book,
iv, iv1 : Inv,
bs : BookStore
ofsort Inv
(* retrieve(r, emptyBS) = error *)
ref (b) == r =>
retrieveInv (r, addBS (b, q, iv, bs)) = iv;
not (ref (b) == r) =>
retrieveInv (r, addBS (b, q, iv, bs)) = retrieveInv (r, bs);
ofsort Nat
(* retrieve(r, emptyBS) = error *)
ref (b) == r =>
retrievePrice (r, addBS (b, q, iv, bs)) = price (b);
not (ref (b) == r) =>
retrievePrice (r, addBS (b, q, iv, bs)) = retrievePrice (r, bs);
ofsort Bool
isAvailable (r, emptyBS) = false;
ref (b) == r =>
isAvailable (r, addBS (b, q, iv, bs)) = (q > 0);
not (ref (b) == r) =>
isAvailable (r, addBS (b, q, iv, bs)) = isAvailable (r, bs);
ofsort Bool
isIn (r, emptyBS) = false;
ref (b) == r =>
isIn (r, addBS (b, q, iv, bs)) = true;
not (ref (b) == r) =>
isIn (r, addBS (b, q, iv, bs)) = isIn (r, bs);
ofsort BookStore
(* decrease(r, q, emptyBS) = error *)
ref (b) == r =>
decrease (r, q1, addBS (b, q2, iv, bs)) = addBS (b, q2 - q1, iv, bs);
not (ref (b) == r) =>
decrease (r, q1, addBS (b, q2, iv, bs)) = decrease (r, q1, bs);
endtype