Generative Formal Templates And Relational Databases

It has often been noted that good database design is a difficult process, and many designers fail to adequately capture the behaviour of the systems they are modelling.  Using formal methods to guide the design of relational databases has the potential to encourage software engineers to think about the constraints that should be imposed on their models. By bringing structure to the design process, and producing models are more rigid by construction, the resulting databases should be improved.  The Z notation shares common features with the relational model and has been used in this context with some success, providing an accessible means to impose constraints and to verify the correctness of a design. However, the standard generics in Z are not sufficient to describe this class of problems generally, and no satisfactory abstract description of the relational model has been suggested using this notation that is entirely formal. Formalising abstract descriptions is desirable, since it brings many benefits, such as the automatic verification of the validity of these descriptions.  In this project we consider the development of a generative template language that allows a generic, template based description of Z schemas. This framework allows not only the description of general models, but also provides a means to discharge repetitive proof obligations more easily. By using this framework, we aim to capture the general form of relational database descriptions in Z.