Formal Relational Database Design: An Exercise in Extending the Formal Template Language

The use of formal description techniques aims to prevent the defects found in software that arise due to poor planning at the design stage. However, the ensuing specifications are often designed with only a single application in mind and are not easily generalised. One area in which these deficiencies arise is that of the formal modelling of relational databases: many authors have drawn parallels between the formal description language, Z, and the relational model of data, but none of these contributions have managed to be both close to the relational model in terms of providing a practical means of database design and fully formal in terms of providing an appropriate metamodel. In this paper, we describe a generative template language, based on the formal template language (FTL). In particular, we extend the FTL, which was developed originally as means of expressing templates, to underpin an approach that facilitates the reuse of specifications in Z, paying particular attention to the formal design of relational databases. These templates encapsulate the common structure found in specifications and can be instantiated to produce specifications tailored to suit particular needs. To achieve this, we extend the FTL and present a mechanism for naming and referencing templates. We also introduce the semantics of template annotations to enforce the syntactic correctness of instantiations.