| 摘要 | 第8-10页 |
| Abstract | 第10-11页 |
| 1 绪论 | 第12-36页 |
| 1.1 研究背景 | 第12-24页 |
| 1.1.1 编译器的正确性验证 | 第14页 |
| 1.1.2 编程语言的语义 | 第14-20页 |
| 1.1.3 编程逻辑和机械验证系统 | 第20-24页 |
| 1.2 研究动机和研究内容 | 第24-28页 |
| 1.2.1 研究动机 | 第24-26页 |
| 1.2.2 研究内容 | 第26-28页 |
| 1.3 国内外相关领域的研究工作 | 第28-34页 |
| 1.3.1 编译器自身的正确性验证 | 第29-32页 |
| 1.3.2 编译后程序的正确性验证 | 第32-33页 |
| 1.3.3 本节小结 | 第33-34页 |
| 1.4 论文主要创新点 | 第34-35页 |
| 1.5 本文组织结构 | 第35-36页 |
| 2 _mJava和Micro-Dalvik的抽象语法和语义 | 第36-62页 |
| 2.1 Isabelle/HOL概述和程序的统一表示 | 第36-38页 |
| 2.1.1 Isabelle/HOL概述和环境配置 | 第36-37页 |
| 2.1.2 程序的统一模型 | 第37-38页 |
| 2.2 _mJava的抽象语法和语义 | 第38-49页 |
| 2.2.1 _mJava的抽象语法和_mJava程序 | 第38-41页 |
| 2.2.2 _mJava程序的大步操作语义 | 第41-43页 |
| 2.2.3 _mJava程序的良构 | 第43-49页 |
| 2.3 Micro-Dalvik的抽象语法和动态语义 | 第49-60页 |
| 2.3.1 Micro-Dalvik的指令及程序 | 第49-52页 |
| 2.3.2 Micro-Dalvik的动态语义 | 第52-60页 |
| 2.4 本章小结 | 第60-62页 |
| 3 编译转换和语义等同证明 | 第62-88页 |
| 3.1 _mJava到Micro-Dalvik VM的编译 | 第62-69页 |
| 3.1.1 _mJava程序的编译方法 | 第62-66页 |
| 3.1.2 中间代码程序生成 | 第66-68页 |
| 3.1.3 目标Micro-Dalvik虚拟机代码生成 | 第68-69页 |
| 3.2 语义等同证明 | 第69-85页 |
| 3.2.1 Ji_prog的大步操作语义 | 第70-71页 |
| 3.2.2 J_prog到Ji_prog的语义等同性 | 第71-77页 |
| 3.2.3 Ji_prog到dvm_prog的语义等同 | 第77-84页 |
| 3.2.4 J_prog到dvm_prog的语义等同性 | 第84-85页 |
| 3.3 本章小结 | 第85-88页 |
| 4 Micro-Dalvik字节码验证和类型保持的编译 | 第88-114页 |
| 4.1 类型系统的可靠性 | 第88-90页 |
| 4.2 Micro-Dalvik的类型系统 | 第90-101页 |
| 4.2.1 相关概念和一个具体例子 | 第90-92页 |
| 4.2.2 类型ty的半格 | 第92-93页 |
| 4.2.3 状态类型的半格 | 第93-97页 |
| 4.2.4 数据流转换函数 | 第97-99页 |
| 4.2.5 Micro-Dalvik的良类型 | 第99-101页 |
| 4.3 Micro-Dalvik程序的类型可靠性 | 第101-105页 |
| 4.3.1 值与类型的一致关系 | 第101-103页 |
| 4.3.2 类型可靠性证明 | 第103-105页 |
| 4.4 字节码验证器和类型保持的编译 | 第105-111页 |
| 4.4.1 Micro-Dalvik字节码验证器 | 第105-110页 |
| 4.4.2 类型保持的编译 | 第110-111页 |
| 4.5 本章小结 | 第111-114页 |
| 5 总结和下一步研究工作 | 第114-118页 |
| 5.1 总结 | 第114-116页 |
| 5.2 下一步研究工作 | 第116-118页 |
| 参考文献 | 第118-128页 |
| 附录 | 第128-134页 |
| 附录1 算术加表达式的手工证明 | 第128-130页 |
| 附录2 mJava源语言表达式的语义规则 | 第130-132页 |
| 附录3 方法调用表达式语句的编译正确性证明(Isar证明语言) | 第132-133页 |
| 附录4 异常捕获处理语句的编译正确性证明(Isar证明语言) | 第133-134页 |
| 攻读博士学位期间发表的科研成果目录 | 第134-136页 |
| 致谢 | 第136页 |
