基于时间逻辑的程序正确性验证

摘要

目前计算机软件的发展受着多种因素的影响，它滞后于硬件，其安全性、可靠性和稳定性一直是人们关注的几个重要问题。随着软件的大型化、模式化，以及安全性需求的日益提高，人们对软件质量的要求起来越高，尤其是对软件的正确性要求。软件质量问题由来已久，由于在许多关键领域运行的软件质量问题而引发重大损失甚至灾难并不少见。
　　 基于调试的方法有很大的局限性。在一些经过调试并投入运行的系统程序或应用程序中还存在着隐患。因此，为了保证程序的正确性，必须从理论上研究有关程序的正确性证明的方法。计算机科学家用完全形式化的方法来证明程序同功能归约的一致性，保证程序的正确性。形式化证明把程序完全正确性问题归结为部分正确性和终止性的证明。
　　 本文提出了一种新的基于形式化理论的程序自动验证方向：即在程序抽象证明中引入时间逻辑。时间逻辑是在一阶逻辑的基础上通过显式地引进时间变量而得到的一种逻辑。本文用这种逻辑描述程序设计语言各个语言成分的语义，验证程序的性质，以及软件规范。结合利用编译技术实现的编译器，针对C语言类型定义、变量定义、运算符、表达式、语句、函数定义及函数调用的语义，将源程序翻译为时间逻辑公式。最后利用数学原理证明程序性质和规范是否符合需求分析和设计阶段所要达到的目标。
　　 本文以ANSIC程序为输入对象，详细描述了该编译器的词法分析、BISON生成的语法分析、语义分析、语法树生成等模块的构造与实现，并给出时间逻辑公式验证的几种证明模式。

目录

文摘

英文文摘

声明

1 绪论

1.1 研究背景

1.1.1 程序验证概述

1.1.2 运用编译技术的优点

1.2 国内外研究发展与现状

1.3 本文研究目的及主要工作

1.4 论文章节安排

2 时间逻辑

2.1 时间逻辑语言

2.2 归结原理

2.2.1 子句集

2.2.2 命题逻辑中的归结原理

2.2.3 替换与合一

2.2.4 谓词逻辑中的归结原理

3 程序设计语言的公理语义

3.1 类型定义的语义

3.2 变量定义的语义

3.3 运算符和表达式的语义

3.4 语句的公理语义

3.5 函数定义的公理语义及函数规范

3.6 函数调用的公理语义

3.7 有关公理

4 翻译C程序成时间逻辑公式的过程

4.1 词法分析

4.2 语法分析

4.2.1 语法分析技术

4.2.2 语法分析的实现

4.2.3 BISON输出程序的分析

4.3 语义分析

4.3.1 语义分析概述

4.3.2 语义分析实现

4.4 符号表

5 基于时间逻辑的程序验证

5.1 一般原理

5.2 验证实例

5.3 证明模式

结 论

参考文献

攻读硕士学位期间发表学术论文情况

致 谢