| Formal methods of software developing are regarded as a revolutionary approach to solve "software crisis", improve dependability and boost efficiency of software products. Among formal methods, people are accustomed to use specification to describe the computer "how to do". At present, Z specification is the most popular specification language, which was finished standardization under the guide of ISO in 2002, and Z specification is more and more applied in every field of industry estate. However, because of the abstraction and great complexity, Z specification has not been widely accepted by programmers.Basic data type and compound data type of Z specification were presented first and some examples of establishing in operations based on compound data type were given. Second, the process of accidence analysis, the thought of syntax analysis and the error control were expatiated briefly on. After that, according to the constitution structure of Z specification, the handling modal of frame was brought up, in order to deal with declarations and predications more flexibly. At last, the frequent errors and their error controls were presented.The article mainly study on the analysis and refinement of relation and function mapping of Z specification. Its main steps as follows: handle the standard Z specification with the method of accidence analysis and phrasing; according to the difference of data types, with the help of STL supporting data construction and general algorithm and codes programmed by myself, proceed semantic operations and refinement respectively, and solve the problem of storage of relation and function mapping; on the condition of no changing of the original meaning of Z specification, realize the target of automatic conversion form Z specification to interim codes and from interim codes to C++ codes.The realization of this article will provide the new approach for software engineering in the period of summary design, help software engineering language more and more used in software exploitation and practice, make the process of software developing reasonable, make the design of software elaborate, and make the allocation of funds accurate, in order to reduce the cost of software exploitation and diminish the maintenance in later software periods. |