Set Theory Operator Automatic Refinement Research And Implementation In Z Specification

It is frequently disadvantageous to the improvement of software quality and productivity that informal specification discribed by nature language frequently is obscure and divergent. Formal method was preferred in order to override deficiency of specification discribed by nature language. Z is presently the most fashionable formal specification. But as a whole, the theory and technology of Z specification isn't extensively applied in industry field. So, the theory of automatic refinement from Z specification to high language is preferred. However, its realization makes slow progress. Therefore, this subject studies automatic refinement of set theory operator in order to develop a entire compiler which can make a convert of Z specification to compiled high-level programme language.At first, the subject mainly discusses following aspects: first, study Z specification data types and relationship among data types; Second, prefer the thought that using containers in STL express Z specification data types in order to study automatic refinement; Third, design the refinement rule of set, reference, bag, sequence etc data types in Z using C++ and STL technology; Fourth, offer function template for automatic refinement from operators in set theory to C++ code and makes refinement rule of operator in set theory by template technology in C++ language and STL template library supporting data construction and general algorithm.Then, basing on above study, design ZTOC automatic refiner. Study includes: First, design the symbol table in automatic refinement handling process; Second, proceed lexical analysis of Z specification; Third, design grammar rule for Smart Z modified and proceed grammar analysis by top-down parsing, and give error dealing; Fourth, in stage of semantics analysis proceed static semantics checking and refresh the information in symbol table.; Fifth, generate target programme(C++ code) in according to the information in analysis of semantics and symbol table, as well as the refinement rule of set theory operator in generating target code stage.It is important for the application of formal approach and formal specification in all stages of software development to study and design automatic refinement from Z to high-levellanguage: Insure complete formalization in all stages of software development; Avoid antilogy in refinement due to mistaken operation or computative mistake and insure consistency and integrity of system; Due to avoiding manual operation in refinement process, it is feasible to bulid a compile environment that Z specification automatic refine and form high-level programme, this will accelerate the promotion and application of Z in industry.