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