In a educational institution there are students and courses which are all uniquely identified. Students can register to attend a course. For each course name there is a collection of students following that class.
NewStudent: School * Student -> School NewCourse: School * Student * Course -> School DropStudent: School * Student -> School DropCourse: School * Student * Course -> School
The requirements specification is taken from “A Study of 12 Specifications of the Library Problem” by Jeannette M. Wing, IEEE Software, July 1988. Consider a small library database with the following transactions:
There are two kinds of users: staff users and ordinary borrowers. Transactions 1,2,4 and 5 are restricted to staff users, except that ordinary borrowers can perform transaction 4 to find out the list of books currently borrowed by themselves.
The database must also satisfy the following constraints:
Make an abstract VDM model of these requirements using the systematic approach described in the chapter with the chemical plant alarm example.
Let us now revisit the solution made to Exercise 5 in the collection of [[MSExSets][exercises for sets] and see how an alternative model using mappings would look.
This exercise provides more practice at the construction of a formal model, and also explores some of the ideas of validation and proof obligations. In the UK the train reservation system works in a way where a small reservation tag is placed at reserved seats. This tag is simply a piece of paper so when you get to the seat to find someone in it and no reservation tag. You end up stading all the way to Edinburgh or wherever. Danish railways get over the problem by having a software reservations system that sends reservation data to the train where it gets displayed in a little LCD panel over the seat. This way, you aren’t subject to the railways staff making a mistake with reservation tags or with dodgy individuals removing the seat reservation when they get ito it. Suppose you work for a software firm commissioned to develop a booking system on the Danish model. Your formal model refers to stations, trains and journeys. The purpose of your model is to define the functionality of the system. You might not be too concerned bout how precisely stations are represented: Station = token; A journey could be modelled as a sequence of stations that you go through:
Journey = seq of Station;
Reservations are for segments of a journey (e.g. between the second and fifth stations):
Segment :: origin : nat1 destignation : nat1 inv s == s.origin < s.destignation;
Trains will be identified by identifiers, the respresentation of which is immaterial:
TrainId = token;
For each train, we record its route (the journey it is following) and the collection of seat numbers available on the train:
TrainInfo :: route : Journey seats : set of SeatNo;
We will not be concerned with the details of seat numbers:
SeatNo = token;
Now to reservations. These are identified by reservation identifiers (ResId):
ResId = token;
Information about each reservation includes the seat number reserved, the train it’s on and the segment of the journey for which the reservation has been made - it’s possible to have a seat reserved fro someone from station 3 to station 5 and then reserved for someone else from station 5 to station 7, for example. The overall reservations system is a record of two mappings containing train details and reservation details:
System :: trains : map TrainId to TrainInfo res : map ResId to ResInfo
Define the following clauses in the invariant:
A function is satisfiable if, for any inputs satisfying the precondition (if there is one), the output is guaranteed to satisfy the invariant on the output type. Define the following functions and explain how you have ensured that your function is satisfiable in each case:
Are all the functions you have defined executable? Design an interface through which you could execute the specification. Just write a short note about it, and draw an illustration of how your interface would look.