Formal Methods - Z notation
Practical Case Study
Part II 2/CS/3T Unit (Autumn Term)

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.