学位论文 > 优秀研究生学位论文题录展示

基于符号计算方法的程序验证技术研究

作　者: 武斌
导　师: 杨路
学　校: 华东师范大学
专　业: 系统分析与集成
关键词: 程序正确性程序验证循环不变式终止性分析前置条件归纳断言映射
分类号: TP311.1
类　型: 博士论文
年　份: 2010年
下　载: 175次
引　用: 3次
阅　读: 论文下载

内容摘要

程序验证是计算机程序设计领域的前沿研究课题,如何保证程序正确性是计算机科学的一个重大挑战.近年来,随着符号计算理论的不断完善和程序验证中使用精确无误差的数学方法的要求,使用符号计算理论来解决程序验证中的相关问题被认为是一种有效途径.本文利用符号计算的思想和方法研究了程序验证领域的三个基本问题：循环不变式生成、程序终止性分析以及前置条件生成.循环不变式在程序的部分正确性验证中起着非常重要的作用,如何生成循环不变式也是程序验证领域的挑战之一.本文主要研究了多项式循环程序的不变式生成问题.首次将有限点集消去理想的思想和方法应用于多项式循环程序的不变式生成,设计了一个多项式时间复杂度的循环不变式自动生成算法,可生成多项式等式型循环不变式.程序的终止性分析问题也是长期以来为众多计算机科学家所关注的问题之一.本文主要研究了一类带有非线性循环条件和线性赋值的循环程序的终止性分析问题.通过计算线性赋值矩阵的约当标准型,确定循环条件在循环次数充分大时的符号,将这类循环程序的终止性分析问题转化为判断参系数半代数系统有无实解的问题.如果参系数半代数系统中的左端函数个数有限或者左端函数都具有整数周期,则这类非线性循环程序的终止性问题是可判定的.另外一个值得研究的问题是如何计算合理的前置条件,使得循环程序在满足该条件的前提下是终止的.本文基于一阶常系数差分方程组的求解技术,设计了一个高效、实用的前置条件生成算法.我们将程序的循环赋值语句转化为程序变量关于循环次数的差分方程组,计算差分方程组的闭形式解.然后将闭形式解代入循环条件,在循环次数充分大时,判断循环条件的符号,进而生成循环程序合理的前置条件.针对线性赋值程序给出了一个高效、实用的前置条件自动生成算法.进而,对于可求出闭形式解的非线性赋值循环程序以及运算可交换的多分支循环程序,也做了相应研究.研究结果表明,符号计算是验证程序正确性的一种行之有效的方法.我们期待将符号计算中的一些经典算法更深入、广泛地应用到程序验证,并集成、研发新的有前途的验证工具.

全文目录

摘要  6-7
Abstract  7-9
第一章绪论  9-27
  1.1 程序正确性研究方法概述  10-16
  1.2 程序正确性研究概况  16-20
  1.3 符号计算简介  20-25
  1.4 本文的选题和主要工作  25-27
第二章循环不变式的自动生成  27-61
  2.1 参系数半代数系统的实解分类及应用  27-34
  2.2 有限点集消去理想的Grobner基  34-40
  2.3 基于消去理想的循环不变式自动生成  40-54
  2.4 本章小结  54-61
第三章一类非线性循环程序的终止性分析  61-77
  3.1 齐次多项式函数循环条件的程序终止性分析  62-67
  3.2 一般情形  67-74
  3.3 本章小结  74-77
第四章循环程序终止的前置条件的自动生成  77-101
  4.1 差分方程组的求解  77-84
  4.2 前置条件的自动生成算法  84-95
  4.3 本章小结  95-101
第五章结束语  101-103
参考文献  103-121
致谢  121-123
攻读博士学位期间发表论文和参与科研情况  123-125

基于符号计算方法的程序验证技术研究

内容摘要

全文目录

相似论文