Report critical system

You will be required to prepare a detailed report based on the problem domain given below. It must contain the key documents or artefacts specified. Qu. 1 A university operates a modular degree scheme, wherein students choose a selection of modules from a large menu. One function of the administration system for the scheme is to keep track of which students are doing which modules. We define the basic types [PERSON, MODULE] the set of all people and the set of all modules respectively Then the type PERSON x MODULE = { p : PERSON, m : MODULE ⦁p ↦ m } is the set of all ordered pairs (maplets) such that the first thing in each pair is a person and the second thing in each pair is a module. You should consider the maplet p ↦ m to represent the information that person p is taking module m. The information for the entire modular degree scheme would therefore be represented by a set of maplets, that is by a relation which is a subset of PERSON x MODULE. We will call this relation taking : PERSON ↔ MODULE Clearly, taking will be an important part of the representation of the state of our administration system. However, we are only interested in the set of people who are registered as students at the university, and the set of modules which are part of the modular degree scheme. students : ℙ PERSON degModules : ℙ MODULE This places a restriction on the maplets allowed in the relation taking. The people doing modules must be registered as students, and the modules they are doing must be bona fida degree modules at our university. dom taking ⊆ students ran taking ⊆ degModules The schema describing the state of the module registration part of the administration system is thus ModuleReg students : ℙ PERSON degModules : ℙ MODULE taking : PERSON↔ MODULE dom taking ⊆ students ran taking ⊆ degModules
You are required to write Z schemas for the following administrative operations: i) Adding a new student to the university. ii) Registering a student for a module. iii) Remove a student from the university. iv) Withdraw a student from a module. v) Add a new module to the degree scheme. vi) Remove a module from degree scheme. You need NOT consider the error conditions for your operations above or prove that they are total operations however they should be supported with an informal narrative.
Qu. 2 Let there be a limit of n students who may be registered for any single module. Modify the RegForModule schema that you have produced in Qu 1 (ii) above, to take account of this extra constraint, and use the schema calculus to define a total version of this operation, that is one which deals appropriately with all possible exceptions to the schemas preconditions.