Object-Z证明责任产生器的设计和实现

摘要

近年来，为了保证各种软件的正确性和提高软件的可维护性、可重用性，人们对软件形式方法的研究越来越广泛和深入，形式方法的研究之所以能够迅速，除了因为其本身固有的优点，如精确、可以进行推理验证等，对形式方法的支持工具越来越多也是一个重要的原因。 本课题研究的是形式规格说明语言Object-Z的支持工具的集成的一部分——一个证明责任产生器。证明责任产生器的工作就是对规格说明进行动态检查，完成静态语法分析不能完成的工作，从而使规格说明的验证工作更加完善。而整个支持工具集成系统的完成，可以大大推广Object-Z，使其得到更广泛的应用，充分发挥它的优点。 本文从Obiect-Z的基本结构出发，提出了对规格说明产生证明责任的策略，从初始状态、前置条件、不变式、定义域检查这四个角度出发，验证规格说明初始状态的存在性、操作是否满足前置条件、操作结果是否满足不变式以及某些运算的操作数是否处于定义域中，从而实现对规格说明一致性的验证。同时，实现的工具提供了一个图形用户接口，用户可以通过该接口来输入自己想证明的性质，更进一步实施对规格说明一致性的验证。 本课题研究开发的证明责任产生器，以LATEX风格的Object-Z规格说明为输入，经过转换后产生证明责任，最终保存在”.tex”文件中，从定理证明器Z/EVES中导入即可证明。 由于采用了纯Java技术、Unicode码和字符流的输入输出方式，因此本软件是一个跨平台、跨语种的编辑器。只要通过Internet下载本软件，只要用户机器上有相应的Java虚拟机，就能够很容易地使用本软件。

目录

文摘

英文文摘

原创性声明及本论文使用授权说明

致谢

第一章引言

1.1软件工程

1.2形式方法

1.2.1形式方法与形式规格说明语言

1.2.2形式方法的优势和局限性

1.2.3定理证明

1.3课题的目标

1.4国内外本领域的研究现状

1.5主要工作

第二章形式规格说明语言简介

2.1形式规格说明语言-z

2.1.1 Z的语法和语义

2.1.2 Z语言的支撑工具

2.2面向对象的规格说明语言OBJECT-Z

2.2.1 Object-Z的基本语法

2.2.2 Object-Z的基本语义

第三章产生证明责任

3.1证明责任产生器

3.1.1证明责任

3.1.2上下文的产生

3.2证明责任的产生

3.2.1从基类中产生证明责任

3.2.2对于继承产生证明责任

第四章OBJECT-Z的LATEX表示

4.1词汇结构(Lexical Structure)

4.2规格说明

4.2.1章节(section)

4.2.2段落(paragraph)

4.2.3定理

4.2.4模式表达式

4.2.5谓词

4.2.6类结构

4.2.7特殊字符

4.2.8一个规格说明的实例

第五章证明责任产生器的设计与实现

5.1规格说明的转换

5.1.1对于基类的转换

5.1.2规格说明中含有对象

5.1.3继承结构的转换

5.1.4复合操作的转换

5.2产生证明责任的实现

5.3证明责任产生器的使用

第六章总结与展望

6.1课题研究总结

6.2将来的工作

参考文献

附录A LATEX语法