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

基于计算机代数的程序验证

作　者: 张志海
导　师: 夏壁灿
学　校: 北京大学
专　业: 应用数学
关键词: 程序验证终止性线性程序不变量计算机代数
分类号: TP311.1
类　型: 博士论文
年　份: 2011年
下　载: 89次
引　用: 0次
阅　读: 论文下载

内容摘要

本文从三个方面研究了如何验证一个程序的完全正确性:不变量生成、不变量检测、终止性分析.在不变量生成方面本文首先证明了由抽象解释生成的不变量都是归纳不变量,其次改进了Antoine Mine所提出的生成Zone抽象域和Octagon抽象域中不变量的方法,最后拓展了归纳不变量的定义以生成更多的不变量,本文的工作是第一个关于如何生成非归纳不变量的工作.在不变量检测方面,本文给出了一个判定一个断言是否为紧跟循环约束位置处的不变量的充要条件,并且对于那些定理不适用的情况下给出了另外的判定方法.本文成功地用这个方法找到了Wikipedia上Fibonacci搜索的一个错误.在终止性分析方面本文主要考虑了线性程序的终止性,包括线性循环约束和非线性循环约束两种情形.当循环约束为线性时本文改进了Ashish Tiwari的工作;当循环约束为非线性时本文证明了如果循环变元取值于整数,那么循环的终止性是不可判定的,对于循环变元取值于实数的情形本文设计了一个算法来判定它的终止性,这是关于有非线性循环约束的线性程序终止性的第一个结果.

全文目录

摘要  3-4
ABSTRACT  4-10
第一章绪论  10-18
  1.1 研究背景  10-12
  1.2 研究现状  12-16
  1.3 主要工作及行文结构  16-18
第二章不变量生成  18-50
  2.1 背景知识介绍  18-27
    2.1.1 循环归纳不变量和抽象解释  18-24
    2.1.2 Zone和Octagon抽象域  24-25
    2.1.3 演示抽象解释和Octagon抽象域  25-27
  2.2 改进Zone和Octagon抽象域  27-50
    2.2.1 抽象解释与归纳不变量  28-30
    2.2.2 基于量词消去的不变量生成  30-50
      2.2.2.1 对情形1的量词消去  31-38
      2.2.2.2 对情形2的量词消去  38-41
      2.2.2.3 对情形3的量词消去  41-44
      2.2.2.4 约束求解和生成尽可能强的不变量  44-46
      2.2.2.5 主算法的形式化描述及复杂度分析  46-47
      2.2.2.6 ∞算术  47-50
第三章不变量检测  50-60
  3.1 背景知识  50-51
  3.2 循环不变量的特征描述  51-53
  3.3 一种新的不变量―内循环不变量  53-55
  3.4 用内循环不变量调试程序  55-58
  3.5 生成非归纳不变量  58-60
第四章带有线性约束的线性程序的终止性  60-96
  4.1 背景介绍  60-64
  4.2 半代数系统和工具包―DISCOVERER  64-65
  4.3 一个基于符号计算的判定算法  65-76
    4.3.1 符号地计算(广义)特征向量  65-68
    4.3.2 主要算法  68-74
    4.3.3 例子  74-76
  4.4 正确性证明  76-84
  4.5 复杂性分析  84-88
  4.6 不可约情形  88-96
    4.6.1 一个充要条件  89-91
    4.6.2 算法  91
    4.6.3 例子  91-93
    4.6.4 复杂性分析  93-96
第五章带有非线性约束的线性程序的终止性  96-122
  5.1 背景介绍  96-98
  5.2 LP_1、LQ_1、LR_1在Z上的不可判定性  98-100
  5.3 判定LP_1在R上的终止性算法  100-109
    5.3.1 A~nX的一般表达式  100-102
    5.3.2 n 次迭代之后P_j(X) 的一般表达式  102-105
    5.3.3 非零最小值性质  105-108
    5.3.4 主要算法  108-109
  5.4 正确性证明  109-112
  5.5 判定LQ_1 和LR_1 在R上的终止性算法  112-114
  5.6 相关的证明和子算法  114-122
    5.6.1 命题5.3的证明  114-116
    5.6.2 计算公共周期的算法  116-118
    5.6.3 求极大有理无关组的算法  118-122
第六章结论和前景  122-124
参考文献  124-130
发表论文  130-131
致谢  131-133

基于计算机代数的程序验证

内容摘要

全文目录

相似论文