论B方法在抽象机库中的实践与应用
| 中文摘要 | 第1-3页 |
| ABSTRACT | 第3-6页 |
| 第一章 绪论 | 第6-9页 |
| ·问题的由来和相关背景知识 | 第6-7页 |
| ·B方法在国内外的研究现状 | 第7-8页 |
| ·本文研究工作及组织 | 第8-9页 |
| 第二章 形式化方法 | 第9-19页 |
| ·形式化方法简介 | 第9页 |
| ·目的 | 第9页 |
| ·发展进程 | 第9页 |
| ·形式规约 | 第9-10页 |
| ·形式验证 | 第10-14页 |
| ·演绎验证 | 第10-12页 |
| ·模型检测（算法验证） | 第12-14页 |
| ·关于形式化方法的讨论 | 第14-15页 |
| ·应用形式化方法的益处 | 第15-16页 |
| ·形式化方法存在的问题 | 第16页 |
| ·形式化方法的建议 | 第16-17页 |
| ·形式化方法的发展方向 | 第17-19页 |
| 第三章 形式化方法的分析和比较 | 第19-24页 |
| ·介绍几种形式化方法 | 第19-21页 |
| ·几种方法的比较和联系 | 第21-22页 |
| ·比较B、Z、VDM方法 | 第22-24页 |
| 第四章 B方法介绍 | 第24-47页 |
| ·B技术 | 第24-25页 |
| ·概要 | 第24页 |
| ·B方法设计的特点 | 第24页 |
| ·B方法的应用 | 第24-25页 |
| ·抽象机符号和广义代换 | 第25-30页 |
| ·语言符号 | 第25-27页 |
| ·构成 | 第27-30页 |
| ·抽象机（Abstract Machine） | 第30-31页 |
| ·规格说明语句 | 第31-40页 |
| ·证明义务（Proof obligation） | 第40-42页 |
| ·AMN的证明义务 | 第40-41页 |
| ·精化的证明义务 | 第41-42页 |
| ·精化(Refinement) | 第42-45页 |
| ·实现（Implementation） | 第45-47页 |
| 第五章 抽象机库的设计 | 第47-68页 |
| ·构造抽象机库 | 第47-58页 |
| ·证明义务 | 第58-63页 |
| ·机器STATE | 第58-59页 |
| ·机器SIMPLE | 第59-61页 |
| ·机器ARRANGE_OBJECT | 第61-63页 |
| ·精化过程 | 第63-66页 |
| ·精化TREE_OBJECT | 第63-65页 |
| ·精化ARRANGE_OBJECT | 第65-66页 |
| ·实现 | 第66-68页 |
| 第六章 结束语 | 第68-70页 |
| ·总结 | 第68-69页 |
| ·进一步的工作 | 第69-70页 |
| 参考文献 | 第70-73页 |
| 发表论文和科研情况说明 | 第73-74页 |
| 致谢 | 第74页 |
