| 摘要 | 第1-5页 |
| ABSTRACT | 第5-9页 |
| 第1章 引言 | 第9-11页 |
| ·研究背景 | 第9-10页 |
| ·研究内容 | 第10页 |
| ·本文的组织 | 第10-11页 |
| 第2章 现有循环不变式开发技术研究分析 | 第11-31页 |
| ·循环不变式现有定义 | 第11-12页 |
| ·循环不变式现有开发技术 | 第12-29页 |
| ·标准循环不变式开发策略 | 第12-13页 |
| ·基于标准策略的自动生成循环不变式法——启发式RCPV 法 | 第13-16页 |
| ·循环不变式动态探测技术 | 第16-19页 |
| ·谓词抽象技术 | 第19-22页 |
| ·基于规则的符号执行分析法 | 第22-26页 |
| ·基于断言的循环不变式探测方法 | 第26-29页 |
| ·各类循环不变式探测技术分析 | 第29-31页 |
| 第3章 PAR 方法中的循环不变式新定义 | 第31-43页 |
| ·PAR 方法主要思想 | 第31-35页 |
| ·RADL 语言和APLA 语言 | 第32-35页 |
| ·循环不变式新定义和新开发策略 | 第35-38页 |
| ·循环不变式的新定义 | 第36页 |
| ·循环不变式新开发策略 | 第36-38页 |
| ·开发未知算法程序 | 第38-40页 |
| ·总体思想 | 第38页 |
| ·开发步骤 | 第38-39页 |
| ·开发实例 | 第39-40页 |
| ·开发已有算法程序循环不变式 | 第40-42页 |
| ·总体思想 | 第40-41页 |
| ·开发步骤 | 第41页 |
| ·开发实例 | 第41-42页 |
| ·评论与总结 | 第42-43页 |
| 第4章 循环不变式开发系统研究与实现 | 第43-55页 |
| ·循环不变式开发系统设计思想和方案 | 第43-46页 |
| ·系统的目标 | 第43页 |
| ·系统总体设计思想 | 第43-44页 |
| ·循环不变式开发系统图 | 第44-45页 |
| ·循环不变式探测系统功能模块说明 | 第45-46页 |
| ·循环不变式开发系统的实现 | 第46-48页 |
| ·“源语言分析原理”模块的实现 | 第46-47页 |
| ·“量词运算符对应关系”模块的实现 | 第47-48页 |
| ·循环不变式正确性证明 | 第48-54页 |
| ·预备知识 | 第49-50页 |
| ·实例讲解 | 第50-54页 |
| ·与现有开发方法比较 | 第54-55页 |
| 第5章 系统直观介绍 | 第55-60页 |
| ·系统界面简介 | 第55-56页 |
| ·若干事例 | 第56-60页 |
| 第6章 总结和展望 | 第60-61页 |
| 参考文献 | 第61-64页 |
| 致谢 | 第64页 |