CT216  TUTORIAL 1  INTRODUCTION TO Z

 http://www.it.nuigalway.ie/~gettrick/courses/CT216/t1.html

1. Develop a Z specification for bank accounts. Include operations to make deposits and withdrawals, open and close an account, and query the balance of an account.

2. Model the booking system for a particular flight. The aeroplane has a limited capacity and the flight should not be overbooked. The operations should include: a passenger booking onto the flight; a passenger cancelling his booking; a query of how many seats are still available; the production of a passenger list. Use the given set [PERSON].

3. A certain brokerage firm specialises in buying and selling companies. At a given time, its portfolio of investments is the set of companies it owns. Based on the State Schema

Portfolio

portfolio : ℙ COMPANY

portfolioSize : ℤ

portfolioSize = #portfolio

write down schemas for (i) buying a company, (ii) selling a company, (iii) a combined operation where we buy one company and sell a different one.

4. An antique shop buys and sells items. Model the collection of antiques in the shop at a given time, and describe operations to buy and sell antiques, using the basic type [ANTIQUE].

5. In the parking example discussed in class, with basic types [PERSON , PARKING SLOT ] our State Schema had the form

Parking

staff : ℙ PERSON

assigned to : PARKING SLOT ↔ PERSON available, occupied : ℙ PARKING SLOT

ran assigned to ⊆ staff

available ∩ occupied = ∅

Write schema (with appropriate error handling) to (i) find all parking slots assigned to a particular person, (ii) find all staff that share a particular parking slot.

6. In a certain US city, parking permission requires that the car is registered and has a parking permit. A parking permit is only issued to registered cars. Starting with the specification [CAR] STATUS ::= noRegistration | registeredCar | permitHolder REPORT ::= success | alreadyRegistered | permitCancelledAlso | notRegistered

| noPermitsLeft | permitAlready | notPermitHolder

permitLimit : ℕ and the State Schema

Reg registered, permits : 𝔽 CAR permits ⊆ registered #permits ≤ permitLimit

develop schema for each of the following (𝔽 above stands for a finite subset):

(a) Registration of a car. Write here 3 schema RegOK , Success, AlreadyRegistered

with the overall structure

Registration ˆ= RegOK ∧ Success ∨ AlreadyRegistered

(b) Deregistration of a car (4 schema: DeregOK , Success, DeregPlusPermit, NotRegistered) DeRegistration ˆ= DeregOK ∧ Success ∨ DeregPlusPermit ∨ NotRegistered

(c) Issuing of a permit:

Permit ˆ= PermitOK ∧ Success ∨ NotRegistered ∨ PermitAlready ∨ NoPermitsLeft

(d) Cancelling a permit:

CancelPermit ˆ= CancelPermitOK ∧ Success ∨ NotPermitHolder ∨ NotRegistered

(e) Enquiring about the status of a car: Enquire ˆ= (RegisteredOnly ∨ PermitHolder ∨ Unregistered) ∧ Success