Z规格说明自动生成器

摘要

The formalized Z language can improve the reliability and robustness of the software via using complex mathematical theories. However, only a few people can understand these theories and compile with Z specification. At present, the main research of Z language focuses on the theoretical research. There is no corresponding tools support the automatic generation of Z specification. The research of Z specification automatic generator introduced in this article can help with the compilation of the Z specification and cut the cost of formal development. This automatic generator has great significance for the large-scale promotion of the Z language.%形式化Z语言采用严格的数学理论可以有效提高软件的可靠性和鲁棒性,但是由于其包含的数学理论使得只有少数人能够熟练应用Z语言进行形式化规格说明书的编写.目前,多数对于Z语言的研究集中在理论阶段,还没有相应的工具支持Z规格说明的自动生成.本文中对于Z规格说明自动生成器的研究有助于降低Z规格说明书的编写难度,降低了形式化开发的难度及成本,对于形式化Z语言的推广具有重要的意义.