循环不变式开发技术研究

摘要

高可靠性软件是当今软件开发的热点问题。确保算法程序逻辑结构正确最理想途径是算法程序的形式化推导和证明。循环不变式在软件形式化方法中占有十分重要的地位，它是理解、证明和推导算法程序的基础和关键。使用形式化方法来证明或推导算法程序无法回避的一个问题就是给出正确的循环不变式。但是循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一。自形式化方法出现以来，众多专家致力于循环不变式的开发，提出了许多循环不变式开发技术，如谓词抽象技术、动态探测技术等。这些技术能探测出较简单问题的循环不变式，但是却无法处理复杂问题。 从本质上来说，循环不变式刻画了循环变量的变化规律和循环程序的特征，因此一个循环程序的循环不变式并非轻易就能得到，尤其是对复杂算法的来说，必须在对循环程序的算法本质有充分理解的基础上才能找到。而现有的循环不变式定义不能反映出循环不变式的本质，基于现有循环不变式定义的技术缺乏理论上的指导，在探测循环不变式的过程中具有试探性和盲目性，又因为本身技术上的限制，因而无法得出复杂问题的循环不变式。 薛锦云教授及其学术团队分析了大量算法程序的本质特征及其与循环不变式关系[15]～[20]，发现现有循环不变式定义的不足，提出了关于循环不变式的新定义和基于新定义之上的循环不变式开发技术，并在此基础上形成了一种实用的算法程序形式化开发方法—PAR方法及其开发环境，在复杂算法程序及软件形式化开发中发挥了重要作用。本文是PAR方法及其开发环境研究的继续，也是薛锦云主持承担的国家自然科学基金项目“基于PAR方法的算法设计形式化和自动化研究”和973前期预研项目“形式化方法制导的软件自动化研究”的重要研究内容。 本文主要的工作是对现有循环不变式定义和现有开发技术进行深入研究，并与PAR方法中的循环不变式开发技术进行比较，指出了现有开发技术的不足之处；同时基于薛锦云教授提出的循环不变式新定义和新开发技术，探讨、研究并初步实现了循环不变式自动开发系统。具体研究成果如下： 1．深入研究了循环不变式定义； 2．对循环不变式标准开发策略和现有较新的几种循环不变式开发技术进行了分析和比较，剖析了其难以适用的原因： 3．详细分析了PAR方法循环不变式新定义和新开发策略，以其作为基础提出了循环不变式开发系统的新模型，并初步实现循环不变式自动开发系统； 4．使用Dijkstra最弱前置谓词法对开发出的循环不变式进行正确性证明。

目录

文摘

英文文摘

声明

第1章引言

1.1研究背景

1.2研究内容

1.3本文的组织

第2章现有循环不变式开发技术研究分析

2.1循环不变式现有定义

2.2循环不变式现有开发技术

2.2.1标准循环不变式开发策略

2.2.2基于标准策略的自动生成循环不变式法──启发式RCPV法

2.2.3循环不变式动态探测技术

2.2.4谓词抽象技术

2.2.5基于规则的符号执行分析法

2.2.6基于断言的循环不变式探测方法

2.3各类循环不变式探测技术分析

第3章PAR方法中的循环不变式新定义

3.1 PAR方法主要思想

3.1.1 RADL语言和APLA语言

3.2循环不变式新定义和新开发策略

3.2.1循环不变式的新定义

3.2.2循环不变式新开发策略

3.3开发未知算法程序

3.3.1总体思想

3.3.2开发步骤

3.3.3开发实例

3.4开发已有算法程序循环不变式

3.4.1总体思想

3.4.2开发步骤

3.4.3开发实例

3.5评论与总结

第4章循环不变式开发系统研究与实现

4.1循环不变式开发系统设计思想和方案

4.1.1系统的目标

4.1.2系统总体设计思想

4.1.3循环不变式开发系统图

4.1.4循环不变式探测系统功能模块说明

4.2循环不变式开发系统的实现

4.2.1"源语言分析原理"模块的实现

4.2.2"量词运算符对应关系"模块的实现

4.3循环不变式正确性证明

4.3.1预备知识

4.3.2实例讲解

4.4与现有开发方法比较

第5章系统直观介绍

5.1系统界面简介

5.2若干事例

第6章总结和展望

参考文献

致谢