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

wushy

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

2021-1-27 09:36 上传

点击文件名下载附件
下载积分: 威望 -5

) [3 o, c( ?/ F' m& i! }

nut1

mJava到Micro-Dalvik虚拟机的编译验证，收藏了。