A video rental company keeps a data base of its customers & classifier then as good, bad or Ugly. Every customer is classified as exactly one of these. For each customer there is a record of which videos he or has out & a record of which of these are over rude. Each customer has unique ID call the customer set C,G, B & U respectively.
(a) Write a Z-schema for a Person & for database including invariants to specify this.
(b) Write pre & post condition for a routine that transfers a given customer & from G to B, assuming that the customer is originally in G.
(c) Write conditions for the above routine without assumption of pre-condition: true?
Q2: Z specifications/schema for a car rental system. In which cars are classified as small, medium and large. When a person rented a car, that person will automatically become members of company. Cars can only be rented in first in first out order and returned cars can only be added from the back of queue.
ReplyDelete1: Specify the system and initial conditions.
persons == [ Member: Rcar; Company: Rcar | Member ⊆ Company]
Database == [C: car ; S: small; M: medium; L:large | C= S∪M∪L]
2: When a customer returns a car. Write pre-condition and operations for making system robust.
Pre-condition
Queue = Empty
Queue: rentCars = rentCars \ {c} // In the front
returnCar: rentCars' = rentCars + {c} //Added at the back
newCar: rentCars' = rentCars + {c} //Added at the back
Pre-condition - Optional
date of return == today
Condition == ok
payment == submitted
if c=> status == rented
rentCars' = rentCars + {c} //Added at the back