Abstract: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.