Formal Specification and Documentation Using Z: A Case Study Approach
Jonathan P. Bowen · 1996
Reserve ( interval? : Interval; until! : Time; report! : Report ) A reservation is made for a period of time (interval?), and returns the expiry time of the new reservation (until!). A client can cancel a reservation by making a new reservation in which interval? is zero; this will then be removed by the next scavenge. Definition ∗ Reservesuccess ∆RS interval? : Interval until! : Time until! = now + interval? shutdown′ = shutdown resns′ = resns⊕ {clientnum 7→ until!} Reports † Reserve = (Reservesuccess ∧ Success) ⊕ TooManyUsers ⊕ NotAvailable ⊕ NotKnownUser The client cannot be a guest user. The reservation must expire before the shutdown time or be for a zero interval. There may be no space for new reservations. ∗ In the Definition section,⊕ is used for relational overriding. Any existing entry under clientnum in resns is removed and a new entry with value until! is added. † In the Reports section, ⊕ is applied to schemas for schema overriding. Mathematically, this can be defined as A ⊕ B = (A ∧ ¬ pre B) ∨ B, where pre B is the precondition of the B schema in which all after state and output components have been existentially quantified. In practice this means that the error conditions are ‘checked’ in reverse order. 78 Formal Specification and Documentation using Z 4.5.5 Service charges The basic parameters are supplemented by two hidden parameters, an operation identifier op? and the cost of executing the operation cost!. The latter can conveniently be defined in terms of natural numbers.