Z规格说明中集合论算子的自动求精研究及实现

论文摘要

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

论文目录

• 摘要
• Abstract
• 1 绪论
• 1.1 研究背景
• 1.1.1 形式化方法
• 1.1.2 形式规格说明
• 1.2 研究意义
• 1.2.1 自动求精思想的提出
• 1.2.2 课题的提出
• 2 C++STL
• 2.1 STL简介
• 2.2 STL基本结构
• 2.2.1 容器（Containers）
• 2.2.2 算法（Algorithms）
• 2.2.3 迭代器（Iterators）
• 3 Z规格说明
• 3.1 研究动态
• 3.2 Z规格说明的类型
• 3.2.1 基本类型
• 3.2.2 复合类型
• 3.3 Z规格说明的构造单元
• 3.3.1 Z的符号
• 3.3.2 模式
• 4 Z规格说明中集合论算子求精规则的设计
• 4.1 采用C++及STL设计Z数据类型的求精规则
• 4.1.1 基本类型的声明
• 4.1.2 变量的声明
• 4.2 采用模板及重载技术设计Z中集合论算子的求精规则
• 4.2.1 采用模板实现Z算子的自动求精
• 4.2.2 运算符重载在Z算子自动求精中的应用
• 4.2.3 Z中集合论算子自动求精的具体算法
• 5 从规格说明到程序代码的自动求精
• 5.1 实现自动求精需要的编译步骤
• 5.1.1 词法分析
• 5.1.2 语法分析
• 5.1.3 语义分析
• 5.1.4 目标代码生成
• 5.1.5 符号表的总体组织
• 5.2 ZTOC自动求精器的设计及实现
• 5.2.1 词法分析阶段
• 5.2.2 语法分析阶段
• 5.2.3 语义分析阶段
• 5.2.4 目标代码生成
• 5.3 符号表
• 5.3.1 符号的主要属性及作用
• 5.3.2 符号表的总体组织
• 5.4 ZTOC自动求精器的扫描及处理过程
• 5.4.1 自动求精器与用户的接口
• 5.4.2 扫描器第一趟扫描及处理
• 5.4.3 扫描器第二趟扫描及处理
• 6 Z规格说明向C++转换示例
• 6.1 图书馆数据库管理规格说明
• 6.2 用于转换的规格说明
• 6.3 转换为C++程序代码
• 7 结论
• 参考文献
• 附录A Smart Z语法
• 附录B 集合论部分常见算子的函数模板定义
• 在学研究成果
• 致谢