JAVA虚拟机语言的部分计值及其正确性证明

摘要

该文给出了一个JVML子集的在线部分计值器.在线部分计值器是由静态参数的具体值一步计算完成而得到剩余程序,它产生剩余程序的时间比离线部分计值器少得多.我们按照开发的过程逐步详细的定义了相应的JVML的子集JVML<,0>、JVML<,1>和JVML<,2>.最后定义的JVML<,2>语言是一个比较完整的面向对象的语言子集,有基本的分支和循环语句以及简单的算术逻辑语句.我们首先对每一个子集给出相应指令序列的程序语义.然后构造了相关的部分计值器,并且形式化的给出了计值规则的正确性.迄今为止,这是世界上第一个对JVML在线部分计值器进行的正确性证明.证明主要包括了几个定理用于证明表达式和语句在一定的环境下通过部分/剩余(partial/residual)计值和全局(total)计值有不变性.

目录

文摘

英文文摘

第一章引论

1.1背景

1.2部分计值

1.2.1概述

1.2.2在线部分计值器和离线部分计值器

1.2.3部分计值的研究现状

1.2.4部分计值的正确性证明

第二章Java语言及其字节代码

2.1 Java语言

2.2 Java虚拟机语言

2.2.1什么是Java虚拟机

2.2.2 Java程序生成可执行代码的过程

2.2.3 Java虚拟机规范

2.3 Java虚拟机的体系结构和指令集简介

2.3.1支持的数据类型

2.3.2寄存器和局部变量

2.3.3操作数栈

2.3.4 Java虚拟机语言指令集

第三章带有分支预测的JVML0及其计值规则

3.1 Java0

3.2 JVML0

3.3 JVML0的语义函数

3.3.1表达式的语义函数

3.3.2语句的语义函数

3.4JVML0的计值规则

3.4.1表达式计值规则

3.4.2语句计值规则

第四章JVML0部分计值器的正确性证明

4.1正确性的定义

4.2JVML0部分计值器的正确性证明

第五章JVML1及其部分计值器的正确性证明

5.1JVML1

5.2 JVML1的语义函数

5.3 JVML1的计值规则

5.4 JVML1部分计值器的正确性证明

第六章JVML2及其部分计值器的正确性证明

6.1 JVML2

6.1.1概述

6.1.2语法范畴

6.1.3 JVML2的定义

6.2 JVML2的语义函数

6.3 JVML2的计值规则

6.4 JVML2部分计值器的正确性证明

参考文献

致谢

攻读学位期间发表的学术论文目录