| 摘要 | 第1-6页 |
| ABSTRACT | 第6-11页 |
| 第一章 绪论 | 第11-15页 |
| ·研究背景 | 第11-13页 |
| ·课题的研究意义 | 第11-12页 |
| ·国内外研究现状 | 第12-13页 |
| ·研究内容 | 第13-14页 |
| ·课题的研究目标 | 第13-14页 |
| ·本文的工作 | 第14页 |
| ·本文的内容组织 | 第14-15页 |
| 第二章 契约式设计与程序验证 | 第15-22页 |
| ·契约式设计 | 第15-17页 |
| ·程序验证 | 第17-21页 |
| ·基于归纳断言的程序验证 | 第17-20页 |
| ·契约式设计与程序验证 | 第20-21页 |
| ·本章小结 | 第21-22页 |
| 第三章 VeriJava 项目介绍 | 第22-28页 |
| ·VeriJava 整体方案 | 第22-23页 |
| ·VeriJava 语言扩展 | 第23-26页 |
| ·契约的表示方法 | 第23-24页 |
| ·语言扩展的优缺点 | 第24-26页 |
| ·VeriJava 编译器 | 第26-27页 |
| ·本章小结 | 第27-28页 |
| 第四章 VeriJava 静态验证器的设计与实现 | 第28-57页 |
| ·静态验证器的构架 | 第28-29页 |
| ·前端翻译器 | 第29-46页 |
| ·VeriJava 中的 Guarded Command 语言 | 第29-33页 |
| ·从VeriJava 到Guarded Command 语言的转换 | 第33-36页 |
| ·前端翻译器的设计与实现 | 第36-46页 |
| ·验证条件生成器 | 第46-52页 |
| ·从GC 语言到验证条件的转换 | 第46-50页 |
| ·验证条件生成器的设计与实现 | 第50-52页 |
| ·定理证明器 | 第52-55页 |
| ·Simplify 定理证明器 | 第52-54页 |
| ·VeriJava 中对 Simplify 的使用 | 第54-55页 |
| ·后端处理器 | 第55-56页 |
| ·本章小结 | 第56-57页 |
| 第五章 实验与评估 | 第57-60页 |
| ·实验介绍 | 第57-58页 |
| ·结果与评估 | 第58-59页 |
| ·本章小结 | 第59-60页 |
| 第六章 全文总结 | 第60-62页 |
| ·文章总结 | 第60页 |
| ·展望 | 第60-62页 |
| 参考文献 | 第62-65页 |
| 附录 1:实验源代码 | 第65-70页 |
| 致谢 | 第70-71页 |
| 攻读学位期间发表的学术论文目录 | 第71页 |
