CS 245 Winter 2009
Due: Thu 19 Mar 2009 10am in the CS245 Drop Boxes
There may be multiple correct answers to this question.
1. (50 marks) The National Basketball Association (NBA) is creating an on-line system to sell
memorabilia associated with basketball teams (e.g., sweaters, mugs, ﬂags, etc.).
Each product is represented by a unique product identiﬁer. It is not the case that all product
identiﬁers are always in use. Each product is associated with only one basketball team.
But each team may have multiple products associated with it. Each product has a single
description (e.g., mug). Multiple products can have the same description. For each product,
the system stores the quantity of the product in stock. This quantity must be greater than 0
for each product.
There is a limit on the maximum number of products that the system can handle. In its ﬁrst
deployment, the system will be used for Canadian teams only so all products stored in the
system must be associated with Canadian teams. (Do not use speciﬁc team names.) There
are no limits on the product identiﬁers or number of descriptions that can be used.
Initially, there are no products in the system.
Here are the operations that can be performed in this on-line system:
(a) Given a team name, description, and quantity of the product, add an entry to the on-line
system using a product number that is not already in use.
(b) Given a team name, if the team name is associated with some product, remove all
products associated with that team.
(c) Given a product identiﬁer, if it is in use, output its associated team and description.
(d) Given a team name, output all the descriptions of products for that team. This output
may be empty.
(e) Given a description, output all the teams that have products with that description. This
output may be empty.
(f) In a purchasing request, the customer provides a product identiﬁer, and if there is at
least 1 of that product in stock, the system outputs a message that the product has
shipped and reduces the quantity of stock of that product by 1. If this purchase reduces
the quantity of stock to 0, the product is removed from the system.
Write a Z speciﬁcation of this system. Write all necessary exception handlers.
1. (4 marks) Types
ErrMsgs ::= NoNewProductIds |SystemFull |TeamNotSupported
|StockisZero |TeamDoesntExist |ProductDoesntExist
Reports ::= ProductShipped
2. (2 marks) Constants
3. (5 marks) System Schema
Products :ProductIds 7→ (Teams ↔Descriptions)
ProductStock :ProductIds 7→ N
dom Products = dom ProductStock
dom (ran Products)⊆CdnTeams
06∈ ran ProductStock
4. (2 marks) Initial State