| 摘要 | 第1-4页 |
| Abstract | 第4-8页 |
| 第一章 绪论 | 第8-15页 |
| ·研究背景和意义 | 第8-10页 |
| ·相关研究情况 | 第10-14页 |
| ·主要研究工作 | 第14-15页 |
| 第二章 形式化方法和PAR 方法 | 第15-25页 |
| ·形式化方法 | 第15-19页 |
| ·形式化方法的研究内容 | 第16-17页 |
| ·形式化方法的分类 | 第17-18页 |
| ·形式化方法的能力和局限 | 第18页 |
| ·形式化方法在高可信软件开发中的重要性 | 第18-19页 |
| ·PAR 方法 | 第19-25页 |
| ·PAR 方法/PAR 平台简介 | 第20页 |
| ·算法设计语言Radl | 第20-22页 |
| ·抽象程序设计语言Apla | 第22-25页 |
| 第三章 Isabelle 定理证明器的剖析 | 第25-37页 |
| ·定理证明器的分类 | 第25-26页 |
| ·Isabelle 定理证明器的剖析 | 第26-32页 |
| ·Isabelle 定理证明器的特点 | 第26-28页 |
| ·Isabelle 定理证明器的系统结构 | 第28-30页 |
| ·Isabelle 定理证明器的理论 | 第30-31页 |
| ·Isabelle 定理证明器的证明方法 | 第31-32页 |
| ·Isabelle 定理证明器的规则/策略 | 第32-37页 |
| ·规则 | 第32-35页 |
| ·策略 | 第35-37页 |
| 第四章 Isabelle 在PAR 方法/PAR 平台中的应用 | 第37-70页 |
| ·PAR 方法开发算法程序 | 第37-39页 |
| ·算法程序正确性的证明方法 | 第39-44页 |
| ·Floyd 的归纳断言法 | 第40页 |
| ·Hoare 公理方法 | 第40-42页 |
| ·Dijkstra 最弱前置谓词方法 | 第42-44页 |
| ·Isabelle 验证使用PAR 方法/PAR 平台开发的算法程序 | 第44-67页 |
| ·Isabelle 验证算法程序的工作流程 | 第44-46页 |
| ·数组和算法程序的验证 | 第46-48页 |
| ·数组段最小和算法程序的验证 | 第48-52页 |
| ·Hanoi 塔非递归算法程序的验证 | 第52-58页 |
| ·二叉树遍历非递规算法程序的验证 | 第58-67页 |
| ·Isabelle 验证 PAR 平台中部分的转换代码 | 第67-70页 |
| ·选择语句转换规则的验证 | 第67-68页 |
| ·循环语句转换规则的验证 | 第68-70页 |
| 第五章 总结与展望 | 第70-71页 |
| ·工作总结 | 第70页 |
| ·下一步工作目标 | 第70-71页 |
| 参考文献 | 第71-76页 |
| 致谢 | 第76-77页 |
| 攻读学位期间参与的科研项目 | 第77页 |
| 攻读学位期间发表(完成)的学术论文目录 | 第77页 |
