C++STL-based Technology To Achieve Refinement And Transformation Of Z Formal Specification

Formal software development method is praised as the revolutionary way of software engineering to overcome the "software crisis", and to improve the reliability and the productivity of software. In order to overcome the ambiguities of natural languages and programming languages, people proposed formal models, which describe "what to do" to replace "how to do" by using mathematical theories of formalization and standardization.Z language is a representative specification language with the qualities of exactness and unambiguity. It can be used for reasoning and refinement of requirment specification. Refinement is an important process of implementing specification to execution. To implement refinement can make the application of Z language wider. This article focuses on the refinement methods of Z formal specification. Based on the refinement of data types, we refine Z formal specification by top-down and stepwise methods. Combined with C++ language, data structure, as well as C++ Standard Template Library technology, the refinement methods of Z specification are explored.Z is a typed language and has a wealth of data types. Its data types include simple types and composite types. Because of the complexity of data types in Z language, there is no direct way to transform the data types of Z specification to the existing high-level languages. However, the standard template library container types defined in C++ language provides a good support for the transformation of Z language data types. This article first analyzed the data types of Z language, and then researched the methods to transform them to C++ codes or C++ container types, and their operators into C++ functions. The foundation for further transformation and refinement of the Z specification is set up.The researched content of this paper provides some new ideas for the design phase of software engineering and helps to promote the application of formal methods in software engineering practice of software development. It makes software development process more rational, software design more careful, and the allocation of funds for software development more definite, thus the costs of software development can be depressed and the latter maintenance can be reduced.