| 摘要 | 第1-11页 |
| Abstract | 第11-13页 |
| 第1章 绪论 | 第13-22页 |
| 1．1 研究背景 | 第13-14页 |
| 1．2 程序正确性验证概述 | 第14-17页 |
| 1．3 本文结果与创新点 | 第17-21页 |
| 1．3．1 程序的正确性的定义 | 第17-18页 |
| 1．3．2 正确性的证明方法 | 第18-21页 |
| 1．4 论文的结构 | 第21-22页 |
| 第2章 关于程序的正确性的讨论 | 第22-37页 |
| 2．1 程序的正确性(Correctness)的概念 | 第22-24页 |
| 2．1．1 语法正确性 | 第22-23页 |
| 2．1．2 语义正确性 | 第23-24页 |
| 2．2 程序正确性的验证方法 | 第24-36页 |
| 2．2．1 静态类型检查与测试 | 第24-26页 |
| 2．2．2 利用逻辑推理对程序结构的正确性进行验证 | 第26-32页 |
| 2．2．3 程序正确性验证的其他方法 | 第32-36页 |
| 2．3 小结 | 第36-37页 |
| 第3章 类型系统与类别代数 | 第37-60页 |
| 3．1 类型系统介绍 | 第37-39页 |
| 3．2 类别代数与出错处理 | 第39-45页 |
| 3．3 一个具有有限基的代数 | 第45-49页 |
| 3．4 利用Turing机停机问题的不可判定性解决代数系统的不可解性 | 第49-52页 |
| 3．5 类型系统可靠性的一个条件 | 第52-58页 |
| 3．5．1 不含空类型的可靠性与完备性 | 第53-56页 |
| 3．5．2 含空类型的可靠性 | 第56-58页 |
| 3．6 小结 | 第58-60页 |
| 第4章 算法语言中表达式的副作用问题 | 第60-68页 |
| 4．1 算法语言的指称语义 | 第61-62页 |
| 4．2 强制型语言中表达式的副作用问题 | 第62-64页 |
| 4．3 函数式语言中表达式副作用问题 | 第64-67页 |
| 4．4 小结 | 第67-68页 |
| 第5章 形式化工程的建模及验证 | 第68-79页 |
| 5．1 UML状态图简介 | 第68-71页 |
| 5．1．1 类图 | 第69页 |
| 5．1．2 状态图 | 第69-70页 |
| 5．1．3 利用状态图进行程序设计 | 第70-71页 |
| 5．2 基于状态图的正确性验证 | 第71-75页 |
| 5．2．1 设计栈操作的交互式状态机 | 第71-73页 |
| 5．2．2 正确性验证 | 第73-75页 |
| 5．3 基于栈操作用例规模的一个计算公式 | 第75-77页 |
| 5．4 小结 | 第77-79页 |
| 结论 | 第79-81页 |
| 参考文献 | 第81-88页 |
| 附录A：攻读博士学位期间发表的学术论文 | 第88-89页 |
| 附录B：一个抽象数据类型的说明(类C语言描述) | 第89-98页 |
| 附录C：攻读博士学位期间参与的主要科研项目 | 第98-99页 |
| 致谢 | 第99页 |
