论文部分内容阅读
针对类Java的面向对象语言m Java到类Dalvik的寄存器架构虚拟机Micro-Dalvik 的编译验证，给出了m Java语言和Micro-Dalvik的操作语义．从m Java语言程序到Micro-Dalvik虚拟机指令的编译分为两步，首先将m Java语言程序中的本地变量名转换为相应的序号，得到一个中间语言程序，再将该中间语言程序翻译成Micro-Dalvik虚拟机指令程序．在给出中间语言的操作语义后，构造了m Java语言程序与编译后的中间语言程序的语义保持定理并证明，以及构造了中间语言程序