基于JML的垃圾收集验证
| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-10页 |
| 1 引言 | 第10-15页 |
| ·研究背景和意义 | 第10-11页 |
| ·相关研究工作 | 第11-13页 |
| ·垃圾收集验证 | 第11-12页 |
| ·JML | 第12-13页 |
| ·主要贡献和创新点 | 第13-14页 |
| ·研究内容和组织结构 | 第14-15页 |
| 2 相关技术和原理 | 第15-25页 |
| ·形式化程序验证和契约式设计 | 第15-19页 |
| ·经典Hoare逻辑 | 第15页 |
| ·契约式设计 | 第15-16页 |
| ·契约的内涵 | 第16页 |
| ·契约式程序设计 | 第16-19页 |
| ·契约式程序动态分析 | 第19-20页 |
| ·程序不变量检测工具 | 第20-24页 |
| ·动态分析工具Daikon | 第21-22页 |
| ·静态分析工具ESC/Java | 第22-23页 |
| ·Daikon与ESC/Java的组合 | 第23-24页 |
| ·动态分析工具JMLC/JMLRAC | 第24页 |
| ·小结 | 第24-25页 |
| 3 JML简介 | 第25-34页 |
| ·JML的特点 | 第25-26页 |
| ·JML的相关工具集 | 第26-27页 |
| ·JML的实例 | 第27-29页 |
| ·JML的语法简介 | 第29-33页 |
| ·小结 | 第33-34页 |
| 4 垃圾收集 | 第34-48页 |
| ·垃圾的定义及产生 | 第34-35页 |
| ·垃圾收集 | 第35-39页 |
| ·垃圾收集的基本概念和定义 | 第35-36页 |
| ·经典垃圾收集算法 | 第36-37页 |
| ·用户程序和垃圾收集器的交互方式 | 第37-38页 |
| ·垃圾收集的安全性问题 | 第38-39页 |
| ·停止式标记-清扫算法 | 第39-42页 |
| ·原理及算法 | 第39-41页 |
| ·堆数据结构形式定义 | 第41-42页 |
| ·渐进式标记-清扫算法 | 第42-47页 |
| ·渐进式的垃圾收集 | 第42-44页 |
| ·写拦截器 | 第44-45页 |
| ·原理及算法 | 第45-47页 |
| ·小结 | 第47-48页 |
| 5 验证垃圾收集器 | 第48-69页 |
| ·提取垃圾收集器中所有模块的不变量 | 第48-51页 |
| ·停止式垃圾收集的JML形式规范 | 第51-55页 |
| ·渐进式垃圾收集器规范 | 第55-60页 |
| ·使用JMLC编译垃圾收集器 | 第60-61页 |
| ·使用JMLRAC运行垃圾收集器 | 第61-63页 |
| ·比较分析 | 第63-67页 |
| ·小结 | 第67-69页 |
| 6 结论与展望 | 第69-70页 |
| 参考文献 | 第70-73页 |
| 作者简历 | 第73-75页 |
| 学位论文数据集 | 第75页 |
