Question: 3. Z Schema (15 marks) We are asked to develop a Z specification for a company that lets its apartments to known customers for fixed

3. Z Schema (15 marks) We are asked to develop a Z specification for a company that lets its apartments to known customers for fixed time-slots. For that purpose we have developed the following state space schema wherein (APARTMENT, TIMESLOT, PERSON] are Z types representing the set of apartments, timeslots, and persons respectively. TimeShare Co. owned : P APARTMENT customers : P PERSON booked : APARTMENT + (TIMESLOT + PERSON) dom booked = owned Vap: APARTMENT | ap e owned . ran( booked ap) customers a) Devise a schema that initializes the system. [2 marks] b) Devise a schema for the operation to add a new customer. [4 marks] c) Devise a schema for the operation to acquire a new apartment. [4 marks] d) Devise a schema for the operation to make a booking of a given apartment to a given customer at a given time. [5 marks] 3. Z Schema (15 marks) We are asked to develop a Z specification for a company that lets its apartments to known customers for fixed time-slots. For that purpose we have developed the following state space schema wherein (APARTMENT, TIMESLOT, PERSON] are Z types representing the set of apartments, timeslots, and persons respectively. TimeShare Co. owned : P APARTMENT customers : P PERSON booked : APARTMENT + (TIMESLOT + PERSON) dom booked = owned Vap: APARTMENT | ap e owned . ran( booked ap) customers a) Devise a schema that initializes the system. [2 marks] b) Devise a schema for the operation to add a new customer. [4 marks] c) Devise a schema for the operation to acquire a new apartment. [4 marks] d) Devise a schema for the operation to make a booking of a given apartment to a given customer at a given time. [5 marks]
Step by Step Solution
There are 3 Steps involved in it
Get step-by-step solutions from verified subject matter experts
