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

递归问题循环不变式开发新策略的研究与应用

作　者: 杨庆红
导　师: 薛锦云
学　校: 江西师范大学
专　业: 计算机软件与理论
关键词: 循环不变式形式化方法算法程序 PAR方法递归问题
分类号: TP311.52
类　型: 硕士论文
年　份: 2003年
下　载: 119次
引　用: 3次
阅　读: 论文下载

内容摘要

软件形式化是提高软件可靠性和生产效率、实现软件自动化的有效途径。循环不变式在软件形式化方法中占有十分重要的地位，它是理解、证明和推导算法程序的基础和关键。因此目前许多算法和程序设计的著作和教材中，均广泛地使用了循环不变式的概念和技术。然而循环不变式的理论和开发技术尚很不完备，这直接影响了循环不变式在算法程序形式化开发中作用的发挥，导致大量复杂算法程序缺乏令人信服的推导和证明，使得许多计算机科学工作者对Dijkstra，Hoare和Gries等著名计算机科学家积极倡导的算法程序形式化开发方法的可行性和实用性产生了怀疑。为了克服已有循环不变式开发技术存在的局限性，薛锦云教授在两个国家自然科学基金课题“若干新的算法程序设计和证明方法研究”和“实用的软件形式化方法及其开发工具的研究”的资助下，对循环不变式的理论和方法进行了系统的研究，提出了关于循环不变式的新定义和新的开发策略，并在此基础上形成了一种实用的算法程序形式化开发方法（PAR方法）及其开发环境，在复杂算法程序及软件形式化开发中发挥了重要作用。本文是PAR方法及其开发环境研究的继续，也是薛锦云当前主持承担的国家自然科学基金项目“基于PAR方法的算法设计形式化和自动化研究”的重要研究内容。本文研究的主要目标是利用薛教授在开发循环不变式的新策略中提出的递归定义思想，探索一类递归定义问题的循环不变式开发技术，并应用于涉及组合数据结构的复杂算法程序的形式化推导和证明。具体研究成果如下： 1．进一步深入研究了循环不变式在算法程序形式化方法中的地位和作用； 2．对现有的循环不变式开发技术进行了分析和比较，剖析了其难以实用的原因； 3．基于现有循环不变式开发技术中的递归定义思想，提出了开发复杂递归问题循环不变式的两种新策略； 4．利用抽象程序设计语言Apla精确描述了6个典型树、图等问题的程序规约和求解算法程序，用上述提出的两种新策略开发了循环不变式，实现了严格的形式化推导或证明，并用PAR方法提供的算法程序自动转换系统将得到的Apla算法程序转换成对应的Delphi和C⁺⁺程序，均得到了正确的运行结果，大幅度地提高了这类复杂算法程序的可靠性和开发效率。总之，本文得到的结果可应用于一类复杂算法程序的形式化推导和证明，方法简单，应用方便，为实现算法设计的形式化和自动化作出了有益的贡献。

全文目录

第一章引言  5-16
  1.1 研究背景  5-6
  1.2 研究内容  6-7
  1.3 预备知识  7-16
第二章循环不变式在算法程序形式化方法中的作用  16-23
  2.1 利用循环不变式理解算法程序  16-17
  2.2 利用循环不变式证明算法程序  17-18
  2.3 利用循环不变式形式推导算法程序  18-23
第三章循环不变式现有开发技术的分析和探讨  23-35
  3.1 标准循环不变式开发策略  23-27
    3.1.1 删除后置断言中的合取分量  23-24
    3.1.2 替换后置断言中的常量为变量  24-25
    3.1.3 扩大后置断言中变量的变化范围  25-26
    3.1.4 联合前置断言和后置断言  26-27
    3.1.5 关于标准循环不变式开发策略的讨论  27
  3.2 状态迁移理论  27-28
  3.3 循环不变式的动态发现技术  28
  3.4 循环不变式的新定义和开发新策略  28-35
    3.4.1 关于循环不变式的新定义  29
    3.4.2 开发循环不变式的新策略  29-35
第四章递归问题循环不变式开发新策略的研究与应用  35-56
  4.1 递归问题循环不变式现有开发技术  35-37
  4.2 递归问题循环不变式开发新策略之一  37-42
  4.3 递归问题循环不变式开发新策略之二  42-56
    4.3.1 利用策略4.2求解对原数据结构进行变换的树、图递归问题  43-48
    4.3.2 利用策略4.2求解对原数据结构进行属性判断的树、图递归问题  48-52
    4.3.3 利用策略4.2求解元素处理顺序无规律的线形表递归问题  52-56
第五章总结  56-57
参考文献  57-60
致谢  60

相似论文

Web服务事务协调协议WS-TX的形式化分析与验证,TP393.09
基于PAR平台的最弱前置谓词生成器的设计与实现,TP311.11
卡箱式高速公路联网收费通行IC卡管理系统的设计与实现,TP311.52
基于Z规格的软件缺陷形式化方法,TP311.53
基于Hoare逻辑的软件形式化验证技术研究,TP311.52
基于形式化方法的统一软件模型及其应用,TP311.52
面向软件复用的组件形式化开发,TP311.52
基于串空间模型的形式化方法的扩展与应用,TP393.08
基于递推技术的算法程序设计方法的研究与应用,TP311.11
基于改进型遗传算法的面向路径测试数据生成,TP311.53
UML建模的形式化方法研究和应用,TP311.52
电子商务安全协议的一种形式化分析方法,TP393.08
形式化方法的理论及其影响,B812
基于行为时序逻辑模型检测的研究与应用,TP311.52
基于SPIN/Promela的UML模型验证工具设计与实现,TP311.52
PDA设备安全管理系统生成器的分析、设计和实现,TP311.52
Radl→Apla程序生成系统及其可靠性研究,TP311.52
Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用,TP311.11
PDA安全管理软件的若干关键技术研究,TP311.52
THP事务协调协议的形式化分析与验证,TP311.52
基于PVS的自稳定算法形式化分析,TP338.8