采用自然语言描述的非形式的规格说明通常具有模糊性和歧义性,这往往不利于软件质量和生产率的提高。为了克服自然语言描述规格说明的缺陷,人们提出了形式化方法。Z是目前最为流行的一种形式规格说明语言,但就总体而言,Z规格说明的理论和技术尚未达到可以在工业界广泛应用的程度。人们提出了Z规格说明到高级语言自动求精的思想,但其实现却进展缓慢。基于以上原因,以自动求精的实现为目的,为研制一套完整的编译环境,使其可以将Z规格说明自动转化为可编译的高级程序设计语言,本课题研究了集合论算子的自动求精。 研究工作主要包含以下几方面内容:研究了Z规格说明的数据类型以及各类型之间的关系;以Z的自动求精为目的,提出了用STL中的不同容器表示Z规格说明各数据类型的思想;利用C++及STL技术设计了Z中集合、关系、包、序列等数据类型的求精规则;结合C++语言的模板、重载技术和STL模板库对数据结构和通用算法的强大支持功能,为集合论中各操作算子到C++代码自动求精提供了相应的函数模板,制定了集合论各算子的求精规则。 以上述研究工作为基础,设计了ZTOC自动求精器,主要工作内容有:设计自动求精处理过程的符号表;对于Z规格说明进行了词法分析;对于修改后的Smart Z设计语法规则并采用自顶向下方法进行了语法分析,并给出相应出错处理;语义分析阶段主要处理静态语义检查及更新符号表的信息;目标代码生成阶段根据语义分析的信息、符号表的信息以及集合论算子的求精规则产生目标程序,即C++程序代码。 Z到高级语言自动求精的研究与设计对于形式化方法及形式规格说明应用于软件开发的各个阶段具有非常重要的意义:确保了从需求分析阶段开始的软件开发周期的完全形式化;避免了人工的误操作或演算错误导致的求精前后不一致,保证了系统的一致性和完整性;由于求精过程避免了手工操作,因而Z规格说明自动精化为程序代码的编译环境可以建立,这将会加速Z规格说明在工业界的推广应用。