mJava到Micro-Dalvik虚拟机的编译验证

• 作者: 何炎祥 张晓瞳 江南
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 编译验证 定理证明 操作语义 机器检测 寄存器架构 面向对象语言
• 年，卷（期）: 2016,（7）
• 所属期刊栏目: 学术论文
• 页码范围: 1619-1629
• 页数: 11页
• 分类号: TP311
• 字数: 10936字
• 语种: 中文
• DOI: 10.3969/j.issn.0372-2112.2016.07.015

摘要

针对类Java的面向对象语言m Java到类Dalvik的寄存器架构虚拟机Micro-Dalvik 的编译验证，给出了m Java语言和Micro-Dalvik的操作语义．从m Java语言程序到Micro-Dalvik虚拟机指令的编译分为两步，首先将m Java语言程序中的本地变量名转换为相应的序号，得到一个中间语言程序，再将该中间语言程序翻译成Micro-Dalvik虚拟机指令程序．在给出中间语言的操作语义后，构造了m Java语言程序与编译后的中间语言程序的语义保持定理并证明，以及构造了中间语言程序的语义与编译后的Micro-Dalvik虚拟机程序的语义保持定理并证明．整个形式化编译验证在定理证明助手Isabelle／HOL中进行了机器检测．m Java语言和Micro-Dalvik虚拟机分别对Java语言和Dalvik虚拟机进行了抽象，是我们兼顾语言的真实性和形式化的清晰性的结果．但是，所有形式化的语义严格遵从语言规范中的定义，并与Dalvik VM的实现保持一致，从这种意义上讲，该编译器并不是一个实验性质的假想编译器，而是有其实用意义的．

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	江南	武汉大学计算机学院	18	70	4.0	8.0
3	何炎祥	武汉大学计算机学院	179	1866	22.0	35.0
9	张晓瞳	武汉大学计算机学院	4	6	2.0	2.0