z specification

student TT' =student TT (8? --- studentTTx? U new Pairs) The operation schema is as follows: Reg For Module A Timetable s?: STUDENT m?: MODULE s? e dom student TT me dom moduleTT module TT m? dom(student TT 3?) ndom(moduleTT m?) 3 new Pairs: TIMESLOT - ROOM ((dom new Pairs=dom moduleTT m'?) A(new Pairs moduleTT m?) (studentTT' = student TT (8?- student TT s? Unew Pairs))) moduleTT' - module TT Exercises 11.3 1. Write a schema to 'deregister' a student from a module. 2. How could we modify the state schema to specify that each module can use a maximum of one room in any given time slot? 3. How could we modify the state schema to specify that each module is only allowed one time slot in the schedule? Write a Z expression for the set of all students registered for a module m. 5. Write a Z expression for the set of all modules being taken by a students. 6. Write a Z expression for the set of all students in a room r at a time i. 7. Write a Z expression for the set of all modules which student p and student q have in common 8. Write a Z expression for the set of all times when student p and student are in the same room. 4. A GENEALOGICAL DATABASE 133 9. Write a Z expression for the set of all modules which clash with a module m on the timetable, that is which take place at the same time as module m. 10. Write a Z expression for the set of all time/room maplets for which one or more modules are scheduled, but no students are scheduled. 11. What would it mean if all Pairs module77 was one to one? (See Section 7.4 for a definition the term one-to-one for functions.) 12. What would it mean if all Pairs student was one-to-one? 13. How could you extend the specification to include concepts such as room capacities and maximum numbers of students allowed in a module, 14. Why would it be difficult to extend the module registration example in Chapter 6 to include timetabling information? student TT' =student TT (8? --- studentTTx? U new Pairs) The operation schema is as follows: Reg For Module A Timetable s?: STUDENT m?: MODULE s? e dom student TT me dom moduleTT module TT m? dom(student TT 3?) ndom(moduleTT m?) 3 new Pairs: TIMESLOT - ROOM ((dom new Pairs=dom moduleTT m'?) A(new Pairs moduleTT m?) (studentTT' = student TT (8?- student TT s? Unew Pairs))) moduleTT' - module TT Exercises 11.3 1. Write a schema to 'deregister' a student from a module. 2. How could we modify the state schema to specify that each module can use a maximum of one room in any given time slot? 3. How could we modify the state schema to specify that each module is only allowed one time slot in the schedule? Write a Z expression for the set of all students registered for a module m. 5. Write a Z expression for the set of all modules being taken by a students. 6. Write a Z expression for the set of all students in a room r at a time i. 7. Write a Z expression for the set of all modules which student p and student q have in common 8. Write a Z expression for the set of all times when student p and student are in the same room. 4. A GENEALOGICAL DATABASE 133 9. Write a Z expression for the set of all modules which clash with a module m on the timetable, that is which take place at the same time as module m. 10. Write a Z expression for the set of all time/room maplets for which one or more modules are scheduled, but no students are scheduled. 11. What would it mean if all Pairs module77 was one to one? (See Section 7.4 for a definition the term one-to-one for functions.) 12. What would it mean if all Pairs student was one-to-one? 13. How could you extend the specification to include concepts such as room capacities and maximum numbers of students allowed in a module, 14. Why would it be difficult to extend the module registration example in Chapter 6 to include timetabling information