2/CS/3T Formal Methods unit
Autumn Term assessment

Case Study
Invoicing


- The subject is to invoice orders;

- To invoice is to change the state of an order (to change it from the
state "pending" to "invoiced");

- On an order, we have one and one only reference to an ordered product
of a certain quantity.  The quantity can be different to other orders;

- The same reference can be ordered on several different orders;

- The state of the order will be changed into "invoiced" if the ordered
quantity is either less or equal to the quantity which is in stock
according to the reference of the ordered product.

You have to take into account the entries of:
        - new orders
        - cancellations of orders
        - entries of quantities in the stock

You may consider that this text is incomplete. One goal of this
exercise is think about questions raised by using the Z notation
on the problem.

If you have such questions, you may propose different possible
"solutions" but select one, giving your reasons.

- Your text should be self-sufficient.

Careful!  Do not extend the domain. For example, do not specify stock
management (when, following what minimum quantity to restock, etc.), do
not add new information as "category of customer", "category of
product", "payment type", "bank account", etc.