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