A system for prototyping Z specifications in Prolog
S. Ekambareshwar · The University of Queensland · 1991
This thesis is concerned with the development of software tools to assist with the processes of software testing and debugging. These tools are developed for the testing and debugging of software that has been formally specified using the Z specification technique and are centered around the logic programming language Prolog. The thesis describes a technique for implementing a rapid prototype (in Prolog) of a system specified in Z. Such a prototype has two particular applications. Firstly, it can be used as a basis for examining the suitability of the Z specification In terms of user's requirements. And secondly, once the final specification has been agreed upon, a Prolog implementation (produced by this technique) can be used as an oracle in the testing of an implementation based upon a more conventional language. The prototyping system has been developed in terms of three components. One is the top level command system which provides the user Interface; a second component is a predicate library which contains the Prolog implementations of all necessary Z constructs (some of them non-standard), and the third component is an automatic type checker. Use of the prototyping system is illustrated by means of a case study which is based upon the Z specification of the Unix Filing System.