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

Formal Verification of _mJava Compiler Targeting Micro-Dalvik Virtual Machine

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

This paper introduces a formal verification of mJava compiler targeting Micro-Dalvik virtual machine （VM）where m Java is an object-oriented language similar to Java,and Micro-Dalvik is a Dalvik-like VM of the register-based architecture.The operational semantics of m Java and Micro-Dalvik VM are defined.The compiler operates in two sta-ges.First it replaces the names of local variables by their corresponding indices and hence translates mJava into an intermedi-ate language.Then it generates the Micro-Dalvik VM instructions.After defining the operational semantics of the intermedi-ate language,the correctness of the two stages are formulated in terms of the preservation of the semantics and is proved re-spectively.The whole formalization is machine-checked in the theorem proof assistant Isabelle/HOL.The m Java language and Micro-Dalvik VM are more abstract than the comparable Java and the Dalvik VM,respectively,which is a result of a compromise between the the realism of the language and the clarity of the formalization.However,mJava language and Mi-cro-Dalvik VM exhibit core features of an object-oriented programming language and a register-based architecture,respec-tively,and thus in this sense,this verified compiler is non-trivial.