Z规格说明中一阶逻辑算子自动求精的研究与实现

论文摘要

随着计算机产业的快速发展,软件的开发规模不断扩大,对软件开发效率和安全性的要求也越来越高,各种开发方法应运而生。Z语言作为一种软件工程语言和形式化方法,在软件文档规范化的应用中成效显著。近年来,国内外对Z语言的研究也逐渐增多。Z语言与其它符号系统相比,一个显著特点是它的规格说明可以用于推理和求精。以往的这种求精过程都由人工完成的,它自动求精实现却进展缓慢。本文以Z规格说明的自动求精为目的,通过约束Z语言中计算机不能实现或不易实现部分,设计出Z语言的一个子集Smart Z,并以标准C++和STL为工具,运用编译技术实现了Smart z规格说明中一阶逻辑算子自动求精。 判断计算机是否可以完成自动求精,关键取决于能否找到实现规格说明的语法、语义的算法。本文将语法、语义的实现问题归约到某一个可解问题,并通过在“通用计算机模型”——图灵机上运行这个可解问题的算法,来证明规格说明求精可判定性。Smart Z继承了Z语言的整型、集合和谓词等,同时保证了其规格说明可求精性,并以一套形式化的方法——正则表达式和EBNF范式描述了它的语言体系。本文使用编译技术实现Smart Z的语法分析、语义分析及向目标代码的转换,本文又针对规格说明的自身特点,对相关算法加以改进,为一阶逻辑算子自动求精的实现创造条件。Smart z的一阶逻辑算子包括量词和连接词等,本文给出它们的求精算法,并以一个实例演示了规格说明和逻辑算子的自动求精过程。 本文最后的结论是“Z语言经过适当的约束后,一阶逻辑算子的自动求精是可以实现的”,这是Z规格说明自动求精目标实现的一个重要前提,也是为实现自动化程序设计做出的一次有意义的尝试。

论文目录

• 摘要
• Abstract
• 1 绪论
• 1.1 课题背景
• 1.2 课题研究的主要内容
• 1.3 课题研究方法和步骤
• 2 Z语言约束和Smart Z的可判定性
• 2.1 Z语言的功能分析
• 2.2 约束问题的提出
• 2.3 Z语言的类型约束
• 2.3.1 原子类型约束
• 2.3.2 幂集类型约束
• 2.3.3 集合的约束与可判定性
• 2.4 Z语言的谓词约束
• 2.4.1 谓词的约束与可判定性
• 2.4.2 谓词与模式的可扩展性
• 2.5 小结
• 3 Smart Z语法设计
• 3.1 Smart Z的设计方法
• 3.1.1 形式语言的描述方法
• 3.1.2 词法描述和正则表达式
• 3.1.3 上下文无关文法及EBNF
• 3.2 Smart Z的词法
• 3.2.1 字母表
• 3.2.2 单词表
• 3.3 Smart Z文法详解
• 3.3.1 规格说明文法
• 3.3.2 段落文法
• 3.3.3 表达式文法
• 3.3.4 谓词文法
• 3.3.5 公理与模式文法
• 4 Smart Z的语义分析与实现
• 4.1 规格说明求精的基本步骤
• 4.2 词法分析
• 4.3 语法分析
• 4.4 语义分析
• 4.4.1 生成语义树
• 4.4.2 符号表管理
• 4.5 目标代码的生成
• 4.5.1 主程序的入口
• 4.5.2 STL与集合的实现
• 4.5.3 目标程序的生成
• 4.6 出错处理
• 4.7 表达式处理
• 4.7.1 表达式的功能分类及语法分析
• 4.7.2 表达式向逆波兰式的转换算法
• 5 一阶逻辑算子自动求精的实现
• 5.1 一阶逻辑算子的自动求精步骤
• 5.1.1 一阶逻辑算子的目标代码生成
• 5.1.2 一阶逻辑算子的目标代码顺序
• 5.2 一个模式求精的例子
• 6 结论
• 参考文献
• 附录A Smart Z词法
• 附录B Smart Z的词法DFA
• 附录C Smart Z文法
• 在学研究成果
• 致谢