| Z is the present most widespread a kind of form specification language. It takes the first order logic and the set theory as its form semantics foundation, having precise and concise characteristic. It mainly uses in the software demand stage, abandoning using the natural language description demand the fuzziness and the ambiguity. But because Z specification itself lacks one entire set of complete translation environment, the development is slower, in view of the fact that Z to the high-level program language automatic transformation thought is proposed. This paper mainly is automatic refinement of cartesian operator in set theory.The paper has included following several aspects: First study Z each kind of data type and their some relations. Next summary the Z specification grammars, form a Z subset, we called them as Smart Z. After transforms them the EBNF grammars and unambiguous SINS charts, we may write the corresponding procedure according to every chart. This article mainly studied cartesian operator the data refinement and the process refinement, cartesian essentially is a set of the ordered pair which every element of n sets is composed , so data refinement is transformed in C++ the record type, the process data refinement has used the C++ template and the STL technology, First the template which two and even many sets formed cartesion has compiled, next formulated two cartesion intersection, union and difference the refinement rules. Finally design Z to C compiler , output each kind of word and its code value in Z lexical analysis, leave corresponding wrong processing after the Z grammar analysis, finally through refinement rule to transform the C++ procedure code.Z specification to higher program language automatic transformation though is proposed, realize from the complete formal specification to the code automaticlly transformation .It will speed up Z widespread promotion in the industrial area., also will speed up the speed which the software development. |
PDF Full Text Request