A system for the automatic conversion between semi-formal structured specification techniques and a formal representation

Abstract

This report describes the rationale for integrating semi-formal structured specification techniques and formal representations. In particular, a way of translating Logical Data Structures and Data Flow Diagrams into an outline Z specification is explained. Information from a data dictionary is used to improve the Z specification generated. A draft technique is also illustrated for the generation of a Logical Data Structure and a Data Flow Diagram from a Z specification. The translation algorithms are featured as a CASE Tool development of the above mentioned techniques. This CASE Tool is based on the method of integration devised. The implementation and use of the tool are illustrated with examples of different complexities. The benefits gained by the use of formal and structured specifications integrated into one method are presented and expounded.