Research And Implementation Of The Power Set Operator Automatic Refinement In Z Specification

It is exigent for efficiency and security of software development in modern times. The formal method is more and more recognized by people with its own characteristic. Z language is a formal specification which is representative in formal method. Z language is accurate and without different meanings. It could be used to discursion and refinement. The refinement is important course of actualizing executable specification. Actualizing automatic refinement of Z specification insteading of manpower is base of making Z use in more extensive fields. The paper is aim at automatic refinement of Z specification, and is base on the Smart Z which is subset of Z, and integrating the knowledge of C++, data structure and STL, and managing compile technology to actualize automatic refinement of power set in Smart Z.By analysing type and structure of power set, it is discovered that the STL container and data structure are similar, and discussing the mode during automatic refinement, and showing the algorithm and rule. The paper established the surroundings of automatic refinement of Smart Z. And actualize automatic refinement by lexical analysis, parsing, semantic analysis and code-switching. By analyzing the words of Smart Z, classify them and write information on table. By judging left-recursion and different meanings of Smart Z, make it determinate grammar. Then analyzing the transition from grammar chart to code by SI-NS chart and completing parsing. Building the tree of semanteme and assuring the events of the tree. Final, integrating the theory analysis, produce the codes during the last step of refinement.The conclusion that the automatic refinement of the power set in Smart Z specification is acquirable, and it not only validates the feasibility of Z specification automatic refinement but also contributes to the further research.