单元赋值语句型循环不变式的开发方法研究

摘要

“软件危机”的出现，对于软件的可靠性和生产效率提出了更高的要求，形式化开发软件是一个很好的解决办法。而形式化开发软件就是要保证能对算法程序进行正确的推导和证明。而循环不变式是算法程序进行推导和证明的基石。任何一个循环程序都存在一个循环不变式，它在循环执行前和每次迭代后都能成立，当达到循环退出条件时，它产生了循环的最后结果。然而循环不变式无论是手工开发，还是自动构造一直都是一个巨大的挑战。本团队承担了国家自然科学基金重大国际合作项目:若干软件新技术及其在PAR平台中的实验研究。其中研究方向之一就是循环不变式的构造和自动探测。 本文首先分析了国内外对循环不变式的定义及其开发方法的研究现状。然后介绍了本团队基于问题求解序列递推关系的循环不变式开发方法。接着介绍单元赋值语句型循环不变式的开发方法:按照PAR方法中的循环不变式开发策略，首先开发出抽象的单元赋值语句型循环程序的循环不变式，即抽象的单元赋值语句型循环不变式，并用Dijkstra最弱前置谓词方法进行了形式化的证明，然后对于具体的单元赋值语句型循环程序，将其对应的抽象的单元赋值语句型循环不变式进行参数实例化即可得到所需的单元赋值语句型循环不变式。最后在本研究团队已有循环不变式自动生成系统中实现了单元赋值语句型循环不变式的自动生成。 本文的创新点有如下3个方面: 1.对单元赋值语句和单元赋值语句型循环程序进行了抽象，使得该方法具有一定的普遍性和典型性。 2.运用Dijkstra最弱前置谓词方法对开发出的抽象的单元赋值语句型循环不变式进行了形式化证明。 3.在本研究团队已有的循环不变式自动生成系统上扩充实现了单元赋值语句型循环不变式的自动生成。

目录

声明

摘要

第1章 引言

1．1 研究背景

1．2 研究内容

1．3 本文的结构

第2章 国内外对循环不变式定义及其开发方法的研究现状

2．1 循环不变式定义

2．2 循环不变式开发方法研究现状

2．2．1 循环不变式标准开发策略

2．2．2 基于抽象解释的循环不变式开发方法

2．2．3 基于约束求解的循环不变式开发方法

2．2．4 循环不变式的动态开发方法

2．3 本章小结

第3章 基于问题求解序列的递推关系的循环不变式开发方法

3．1 PAR方法的指导思想和关键技术

3．2 PAR方法的语言机制

3．3 循环不变式的新定义和新开发策略

3．3．1 循环不变式的新定义

3．3．2 循环不变式的新开发策略

3．4 开发未知算法程序

3．4．1 开发步骤

3．4．2 应用举例

3．5 开发已有算法程序循环不变式

3．5．1 开发步骤

3．5．2 应用举例

3．6 本章小结

第4章 单元赋值语句型循环不变式的开发方法

4．1 单元赋值语句及其循环不变式开发的指导思想

4．1．1 单元赋值语句

4．1．2 指导思想

4．2 两种单元赋值语句型循环不变式开发步骤

4．3 循环不变式确认及程序正确性证明

4．3．1 预备知识

4．3．2 正确性验证

4．4 应用举例

4．5 本章小结

第5章 开发方法系统实现

5．1 循环不变式生成系统简介

5．1．1 循环不变式生成系统图

5．1．2 系统界面介绍

5．2 实现案例

第6章 总结和展望

参考文献

致谢

在读期间公开发表论文(著)及科研情况