Prototyping from Z specifications

Summary form only given. A simple method, requiring no investment in software tools, of producing prototypes from Z specifications is presented. The properties of constructive specification are discussed, and it is shown that, in spite of the theoretical disadvantages of writing specifications constructively, most Z specifications satisfy these properties. Pragmatic reasons for this are described. Rather than refine Z towards the target implementation language, a virtual extension of the language toward Z can be made. To illustrate this, an implementation of a subset of Z in Ada is described, and rules are developed for how this can be used to translate, as yet manually, this part of Z into Ada. A simple case study is used to illustrate the whole process from specification through to prototype. Finally, experiences of the costs of this method, such as initial and training costs, and benefits, such as an increase in programmer efficiency and a reduction in the time from specification to prototype, are described