（计算机软件与理论专业论文）java虚拟机语言的部分计值及其正确性证明.pdf

j a v a 虚拟机语言的部分计值及其正确性证明 摘要 、 【部分计值是一种软件转换技术，它可以根据部分输入对程序进行例 l 化。完成程序中只依赖于给定的那部分输入的计算，最终得到高效的剩 余程序。部分计值技术可以作为软件的优化工具，但是更重要的是，当 部分计值器可以将其自身作为输入，它就能够把程序语言的解释器自动 转换成编译器。由于编译器的研究在计算机科学和应用中的重要性，这 个领域吸引大量的研究者。近三十年来人们研究和实现了许多语言的部 分计值器，但是其中绝大多数都是基于函数式语言，逻辑式语言和命令 式语言的，而这与面向对象语言是当今计算机科学的主流语言的状况是 不相称的，所以我们认为研究面向对象的语言下的部分计值技术是很有 理论意义和应用价值的。 j a v a 语言是当今应用最广泛的面向对象的语言之一，但是到目前为止 对j a v a 语言的部分计值工作还是做的相当少的，这有两个原因。第一， 面向对象语言本身的操作语义和指称语义就比较复杂，没有一个比较完 整的和一致的形式系统来刻划它；第二，j a v a 语言由于具有平台无关性， 所以它有两层结构。j a v a 程序首先要编译成j a v a 虚拟机语言写的字节代 码然后再由j a v a 虚拟机来解释执行。所以相比而言，对字节代码做研究 要比对j a v a 语言本身做研究要来得更为有效。j a v a 语言是解释执行的， 所以其执行速度要比编译执行的c + + 之类的语言慢一个数量级，而解 释就是在j a v a 虚拟机这一层上执行的，因此瓶颈就在字节代码解释到目 标代码这个过程中。但是到目前为止，除了传统的采用解释器的j a v a 编 译系统，即时编译器( t ) 的出现对j a v a 性能有了很大的改善。但是因为 这些优化都是针对字节码在虚拟机中的运行方案的，字节代码的效率并 没有提高，而部分计值技术正是代码转换技术中的一种。因此我们的部 、7 分计值的理论研究就选择基于j v m l 字节代码。彳 i 本文给出了一个j v m l 子集的在线部分计值器。在线部分计值器是由 静态参数的具体值一步计算完成而得到剩余程序，它产生剩余程序的时 间比离线部分计值器少得多。我们按照开发的过程逐步详细的定义了相 应的j v m l 的子集j v l v i l o 、j v m l l 和j v m l 2 。最后定义的j v m l 2 语言 是一个比较完整的面向对象的语言子集，有基本的分支和循环语句以及 简单的算术逻辑语句。我们首先对每一个子集给出相应指令序列的程序 语义。然后构造了相关的部分计值器，并且形式化的给出了计值规则， 最后证明了计值规则的正确性。迄今为止，这是世界上第一个对j v m l 在线部分计值器进行的正确性证明。证明主要包括了几个定理用于证明 表达式和语句在一定的环境下通过部分剩余( p a r t i a l r e s i d u a l ) 计值和全 局( t o t a l ) 计值有不变性。 关键词：j v m l ，语义函数，部夯舞值，计值规则，正确性证明 p a r t i a le v a l u a t i o n o fj a v av i r t u a lm a c h i n e l a n g u a g ea n di t sc o r r e c t n e s s p r o o f a b s 蛋r a c t p a r t i a le v a l u a t i o ni sak i n do fs o f t w a r et r a n s f o r m a t i o nt e c h n i q u et h a t i s a b l et os p e c i a l i z ep r o g r a mo na n yg i v e np a r t i a li n p u t s i n c et h en e wp r o g r a m i n t e g r a t e st h e s ei n p u tv a l u e s ，i ti s as p e c i a lc a s eo ft h ei n i t i a l + p r o g r a m ，a n d t h e r e f o r ec o n s i d e r e ds p e c i a l i z e d t h er e s u l t i n gs p e c i a l i z e dp r o g r a mo n l y c o n t a i n st h er e m a i n i n gc a l c u l a t i o n st h a td e p e n do nt h eu n a v a i l a b l ei n p u t v a l u e s ，a n dt h e r e f o r ew i l lb e m o r ee f f i c i e n tt h a nt h eo r i g i n a lp r o g r a m p a r t i a l e v a l u a t i o nc a ns e f v ea sa p r o g r a mo p t i m i z a t i o n t o o l , b u tm o r ei m p o r t a n t l y , i t m a yt r a n s f o r mt h ei n t e r p r e t e r o fap r o g r a m m i n gl a n g u a g et oi t s c o m p i l e r , w h e nt h ep a r t i a le v a l u a t o ri ss e l f - a p p l i c a b l e b e c a u s eo ft h eg r e a ti m p a c to f c o m p i l e r si nt h ec o m p u t e r s c i e n c ea n d t e c h n o l o g y , t h i sa r e a h a sa t t r a c t e dal o t o fr e s e a r c he f f o r t s a sa r e s u l t ，m a n yp r a c t i c a lp a r t i a le v a l u a t o r sh a v ee m e r g e d d u r i n gt h el a s tt h r e ed e c a d e s b u tu n f o r t u n a t e l y , m o s to ft h e ma r eb a s e do n f u n c t i o n a l ，l o g i c a l a n di m p e r a t i v el a n g u a g e s h o w e v e rt h e o b j e c to r i e n t e d l a n g u a g ei st h em a i n s t r e a ml a n g u a g ei nc o m p u t e rs c i e n c et o d a y s ow et h i n k t h er e s e a r c ho n p a r t i a le v a l u a t i o na b o u to b j e c t - o r i e n t e dl a n g u a g ei ss i g n i f i c a n t i nb o t h t h e o r ya n dp r a c t i c a lf i e l d j a v ai so n eo ft h em o s t w i l d l yu s e dl a n g u a g e si nt h ew o r l d b u tu pt on o w t h er e s e a r c ho f p a r t i a le v a l u a t i o no nj a v ai sr a t h e r r a r e t h e r ea r et w or e a s o n s o n ei sb e c a u s et h eo p e r a t i o n a la n dd e n o t a t i o n a ls e m a n t i c so f o b j e c t o r i e n t e d l a n g u a g e i s v e r yc o m p l e xa n di n f a c tn of o r m a l s y s t e m i sd e c e n ta n d c o n s i s t e n te n o u g ht od e s c r i b et h el a n g u a g e t h eo t h e ri s b e c a u s ej a v ai sa p l a t f o r mi n d e p e n d e n tl a n g u a g ea n di th a sat w ol e v e ls t r u c t u r e j a v a p r o g r a m s s h o u l db et r a n s l a t e di n t ob y t e c o d ef i r s ta n dt h e nb ei n t e r p r e t e db y t h ej a v a v i r t u a l m a c h i n e c o m p a r a b l y , t h e r e s e a r c ho nj a v av i r t u a l m a c h i n e l a n g u a g ei sm o r ei m p o r t a n tt h a no nt h ej a v al a n g u a g er s e l j a v ai sa n i n t e r p r e t e rl a n g u a g e ，s oi t se x e c u t i o ns p e e di sf a rb e l o wt h ee x e c u t i o ns p e e d o f c o m p i l e rl a n g u a g e sl i k ec + + t h e r e f o r et h eb o t t l e n e c ki si nt h ep r o c e s so f i n t e r p r e t i n gt h eb y t e c o d et ot h eo b j e c tc o d e a l t h o u g hal o to f o p t i m i z a t i o n t e c h n i q u e sh a v e b e e nu s e do n j a v a , m o s to f t h e mf o c u so nt h e i m p r o v e m e n t o f t h ev r t u a lm a c h i n e t h e e f f i c i e n c y o fb y t e - c o d e i s n t i m p r o v e d , a n d f o r t u n a t e l yp a r t i a le v a l u a t i o ni sak i n do fc o d et r a n s f o r m a t i o nt e c h n i q u e s o w ec h o o s eo u rr e s e a r c h o f p a r t i a le v a l u a t i o no nj v m lb y t e c o d e a no n - l i n ep a r t i a le v a l u a t o rf o rp a r to fj v m li sf o r m a l l yd e f i n e da n d p r o v e nt o b ec o r r e c ti n m yt h e s i s a n o n l i n e p a r t i a l e v a l u a t o rp r o d u c e s r e s i d u a lp r o g r a m t h r o u g ho n e s t e pc a l c u l a t i o no nt h ec o n c r e t ev a l u eo f s t a t i c p a r a m e t e r s ，a n di t sp r o d u c t i o nt i m ei sm u c hl e s st h a nt h eo f f - l i n eo n e w e h a v ed e f i n e dj v m l o ，j v m l la n dj v m l 2t h a ta r ep a r t so fj v m l t h r o u g ho u r d e v e l o p m e n tp r o c e s s t h ej v m l 2i s a c o m p a r a b l yc o m p l e t ep a r t o f o b j e c t o r i e n t e dl a n g u a g e t h a th o l d sc o n t r o ls t a t e m e n t sa n di t e r a t i o ns t a t e m e n t s ； i ta l s oh o l d sb a s i c l o g i c a la n d m a t h e m a t i c a ls t a t e m e n t sa n d e x p r e s s i o n s s o a t f i r s t ，w es h o wt h es e m a n t i c so fp a r to fj v m l i nd e t a i l s t h e nw es h o wt h e c o r r e s p o n d i n gd e f i n i t i o no fp a r t i a l e v a l u a t i o na n di nt h ee n dw ep r o v et h e c o r r e c t n e s so ft h e p a r t i a l e v a l u a t o r a sf a ra sw ek n o w , t h i si st h ef u - s t c o r r e c t n e s sp r o o fo fa no n - l i n ee v a l u a t o rf o rj v m li nt h ew o r l d t h ep r o o f c o n s i s t so fs e v e r a lt h e o r e m ss h o w i n gt h ec o r r e c t n e s so f p a r t i a le v a l u a t i o na n d t h ei n v a r i a n c eo fc e r t a i np r o p e r t i e so ft h ee n v i r o n m e n t su n d e r p a r t i a l r e s i d u a l a n dt o t a le v a l u a t i o n k e y w o r d s ：j v m l ，s e m a n t i c sf u n c t i o n , p a r t i a le v a l u a t i o n ，e v a l u a t i o nr u l e s ， 1 1 背景 第一章引论 计算机的出现是上个世纪最大的技术革命之一。人们把大量重复机械性的工作交 由计算机完成以提高生产效率和确保质量。现在，计算机软件和硬件无论在规模和功 能上都在不断增大，而且这种趋势随着社会生产对计算机系统的愈加依赖而迅速加 快。但是系统复杂程度的提高往往使得出现设计错误的几率增加，而人们对计算机系 统的过分依赖导致了在很多情况下错误变得不可接受。因此计算机软件工程的一个主 要目标就是：无论系统有多么复杂，确保它的正确性在设计实现过程中得到有效的保 证。人们尝试了许多方法来实现这一要求，包括设计实现过程的严格管理，实现后的 反复测试等等，但是其中最严格的毫无疑问是形式化方法( f o r m a lm e t h o d ) 。形式化 方法以数学的语言、技巧和工具对系统进行规范、实现和验证。虽然由于形式化方法 还是或多或少依赖于人，从而使得错误仍然可能发生，但是这种依赖性已经大大减弱 了。同时形式化也帮助我们更精确的理解和完善目标系统，揭示原先设计中可能存在 的矛盾、歧义和漏洞。形式化方法或者数学方法的出现与计算机本身的出现几乎是同 步的，如果考虑对图灵机、l a m b d a 演算的研究，甚至可以认为更早。但是早年的研 究与应用的差距极大，形式化方法处理的对象过于抽象，最终实现的系统对非专业人 员过于复杂难用。但是目前，研究者已经把实际系统作为研究对象，并完成了一些令 人印象深刻的实用项目。工业界也开始关注形式化方法在实践中的巨大潜力，投入大 量的人力物力进行研发。形式化方法主要用于规范( s p e c i f i e a l i o n ) 和验证( v e h f i e a f i o n ) 中。 规范就是描述系统及其所需要满足要求的过程。非形式化方法主要使用自然语言 进行规范，由于自然语言先天不可避免的歧义性，所以往往造成疏漏。而形式化规范 是基于数学方法严格定义了语法和语义的人工语言，因此可以避免大量歧义性错误， 同时也方便了对系统进行严格的正确性证明。软硬件系统的规范包括系统的功能、内 部结构和性能参数等，其中系统功能的形式化规范最为成熟。在一般系统中，我们可 以严格描述系统的输入输出函数比如使用指称语义，状态迁移所需要满足的前提和后 置条件，甚至可以刻画系统的交互行为。规范过程本身也为设计人员提供了一个加深 和澄清对目标系统理解的机会。同时规范文档是系统的用户与设计者，设计者与实现 者，实现者与测试者之间进行交流的工具，它也为系统的源代码提供了一个高层次的 描述，而便于系统的维护。 而验证则是检查所设计的系统是否满足预先的要求的过程。工业界现在主流的解 决方案是模拟系统所要面对的运行环境，测试它在一些边界条件和反复运行等情况下 是否达到设计规范。但是这类方法无法覆盖系统可能面对的所有情况，因此很不严格。 而形式化验证则在公理化的基础上，构建对系统正确性的数学证明。因此只要保证所 使用的公理和推理规则在目标系统中成立，那么系统的正确性也就成立了。虽然形式 化方法并不能百分之一百确认系统满足规范，但是我们把问题归结到最简单的一些期 望系统满足的公理和推理规则，而这些都是与具体的规范是无关的，并且数量较少。 形式化方法有很多种，其中有一种是定理证明方法。定理证明方法在一般意义上是不 可判定的，就是说不存在图灵机，它能在输入某个命题后，输出它是否是个真命题， 因此一般需要人的介入( 启发性方法) 。 我的硕士研究生阶段的主要研究工作就是对一个新建立的系统进行正确性证明。 工作可以分两部分： 1 对j a v a 语言的一个子集所对应的j a v a 虚拟机语言的部分计值技术进行研究，给出 了它的语义，然后给出其相应的o n l i n e 的j a v a 部分计值器的计值规则 2 讨论部分计值器的正确性概念，给出了该部分计值器的正确性证明。 1 2 部分计值 部分计值( p a r t i a le v a l u a t i o n ，p e ) 是一种能够进行程序例化( p r o g r a m s p e c i a l i z a t i o n ) 的系统软件工具：在给定原程序部分的输入的情况下，对程序进行转 换、例化和优化，完成所有那些只依赖于给定的那部分输入的计算，最终得到所谓的 剩余程序( r e s i d u a lp r o g r a m ) 。而剩余程序作用在余下的那部分输入后、得到的结果 应该与源程序作用在全部的输入参数而得到的结果相一致。部分计值的理论基础就是 递归函数论中k l e e n e 的s m 1 1 定理。 假定原程序p r o g r a m 只有两个输入参数x 1 ，x 2 。如果我们固定第一个参数x l - d ， 那么部分计值器( p a r t i a le v a l u a t o r ) 应该在指称语义上满足，对于任意的e ，如下等 式始终成立： p e ( p r o g r a m j 妒- p 孕弧d p r o g r a m d ( e ) = p r o g r a m ( d , e ) 容易看出，满足这一方程的最简单的程序就是： l e tx v - - di np r o g r a m ( x 1 ，x 2 ) 显然我们应该要求的更多。在操作语义上，部分计值技术要保证p r o g r a m d 有尽 可能好的时间和空间复杂度。因此从另一个角度看，部分计值器就是在给定 p r o g r a m ( x l ，x 2 ) 和第一个参数d 后的对程序l e tx l = di np r o g r a m ( x l ，x 2 ) 的一个优化器。 考虑到对于一个完善的部分计值器，如果在不给定任何输入的情况下，也应该可以对 原程序中的可计算部分完成计算，因而它可以被用作优化工具。 但是作为其最重要的应用是，部分计值为程序编译和编译器的自动生成和优化提 供了新的技术上的可能性。在七十年代，日本的f u t a m u r a l 2 1 和前苏联的t u r c h i n t 3 1 以及 e r s h o v 4 1 分别独立指出：如果部分计值器具有自作用能力，换言之，它可以把自身( 或 其自身的编码) 作为输入，那么就能把给定语言的解释器( i n t e r p r e t e r ) 转换成编译 器( c o m p i l e r ) 。更进一步，甚至可以得到编译器的自动生成器( c o m p i l e r - g e n e r a t o r ) 。 这就是著名的所谓f u t a m u r a 三映射( f u t a r r l u r ap r o j e c t i o n ) ： 4 ( 2 ) ( 3 ) t a r g e t 2 p e ( i n t e r p r e t e r , s 0 1 f f c e ) t a r g e ti n p u t2o u t p u t 2 i n t e r p r e t e r ( s o u r c e ，i n p u t ) 2 p e ( i n t e r p r e t e r , s o u r c e ) i n p u t c o m p i l e r = p e ( p e ，i n t e r p r e t e r ) c o m p i l e r s o u r c e2 t a r g e t = p e ( i n t e r p r e t e r , s o u r c e ) = p e ( p e i n t e r p r e t e r ) s o u e c e c o m p i l e r - g e n e r a t o r = p e ( p e ，p e ) c o m p i l e r - g e n e r a t o ri n t e r p r e t e r= p e ( p e ，p e ) = p e ( p e ，i n t e r p r e t e r ) = p e 0 e ，p e ) i n t e r p r e t e r 由于编译是程序语言技术的核心，对其的研究开发一直贯穿着整个计算机科学的 发展。传统的编译器开发都是手工的，错误难以避免，无论是优化还是对其正确性的 证明都异常困难。而使用部分计值，可以把解释器自动转换成编译器。众所周知，编 译器的实现需要考虑两个约束时间：编译时的程序输入和运行时的参数输入；而解释 器只要考虑一个约束时间：运行时的程序和参数输入。因此解释器比编译器更容易实 现，同时正确性也相应的更容易保证。所以只要同时保证部分计值器的正确性和高的 优化效率，就可以得到正确及比较高效的编译器。 12 2 在线部分计值器和离线部分计值器 部分计值器可以分为两种：在线部分计值器( o n l i n ee v a l u a t o r ) 和离线部分计值 器( o f f - l i n ee v a l u a t o r ) 。 在线部分计值器是由静态参数的具体值一步计算完成而得到剩余程序。离线部分 计值器分为两个阶段，约束时间分析( b i n d i n gt i m ea n a l y s i s ，b t a ) 和例化过程 ( s p e c i a l i z a t i o n ) 。首先约束时间分析根据程序参数的约束信息，跟踪参数在程序中的 传播和运算过程，分析得到程序内部所有参数、中间变量和中间运算过程的约束信息， 而对原程序进行标记( a n n o t a t i o n ) 。然后由例化器在标记过的原程序和输入参数的基 础上产生所需的剩余程序( r e s i d u a l ) 。 b t a ( p r o g r a m ，b i n d i n g - i n f o r m a t i o n ) = p r o g r a m 。o t a t e s p e c n 也i z 0 r ( p r o 筝锄a m m ，s t a t i c - p a r a m e t e r ) ；p m 驴姗槭d i l e 一般情况下，在线部分计值器产生剩余程序的时间比离线部分计值器短的多，但 是离线部分计值器由于在约束时间分析阶段能分析出程序的全局信息，因而它能更好 的适合实际应用程序。 5 1 1 2 3 部分计值的研究现状 国外对部分计值的研究极大部分集中在串行语言，如基于函数式语言的 l a m b d a m i x l q ，基于p r o l o g 语言的l o g i m i x 川，基于c 语言的c - m i x l 8 i ，这些成果在 j o n e s ，o o m a r da n ds e s t o f l 的书( 9 】中有详细的介绍，此书总结了9 3 年之前部分计值的 理论和应用成果。9 3 年之后串行语言部分计值研究也有较大进展。 最值得一提的是函数式语言的部分计值，它是所有部分计值中最成功的，这是因 为函数式语言相对于一般命令式语言有一个更大优点，即它没有副作用，而l a m b d a 演算，由著名的c h u r c h - r o s s e r 定理保证了在部分计值过程中，推迟或者提前某些运 算不会改变程序的语义，因此，部分计值器的正确性自然而然的得到了保证。 相比而言，命令式语言部分计值的研究就显得困难重重，它的研究目前主要集中 在c 、p a s c a l 语言，象基于c 语言的c m i x ，基于p a s c a l 语言子集i m p o 的部分计值【l 。 虽然有一些论述命令式语言部分计值理论的文章i ll ，”j ，而且c 和p a s c a l 语言的语法 是现成的，但针对这些复杂的语法结构的计值规则繁多，光是完成一个很小的语言子 集就要做大量工作。 随着并行计算机，工作站集群和计算机网络的迅猛发展，并行语言逐渐成为程序 设计语言的主流。同时由于现实世界是一个并行系统，并行语言对于描述客观现象也 更为自然，编写的程序在并行计算机或者是网络运行效率也更高。因此研究相应于并 行语言的自动化技术不仅在理论上，同时在实际应用中有着重要的意义。 但是就是在理论上研究并行语言都困难重重，因为到目前为止，也没有公认的具 有串行语言中l a m b d a 演算的地位的并行演算系统或者说模型。现在国际上研究的并 行模型主要有c c s 【l 、n 演算f 1 4 j 及其它们的变种。而并行语言部分计值器的研究国 内开始于杨酷和旷海蓉i l 驯的工作，随后陈翌佳i l6 l 和王明文1 1 7 j 做了进一步的工作。 12 4 部分计值的正确性证明 从历史上看，部分计值这个概念早在1 9 6 4 年就由l o m b a r d i 和r a f f a e l 提出了1 1 8 l ， 但直到1 9 8 5 年当c o p e n h a g e n 大学j o n e s l 3 9 1 的研究小组公布他们的研究结果，部分计 值才引起广泛的重视。自从那时候起，大家都把精力放在了开发强有力的部分计值器 上，而且主要是函数式语言和面向逻辑语言的部分计值器。而第一篇关于命令式语言 部分计值器的论文是由e b h o v 和他的合作者n o v o s i b i r s k 于七十年代末发表的。其实 当时就是针对a l g o l - 6 8 的一个小子集而傲的工作。后来，大家才陆续给出了一些关于 c 语言和类p a s c a l 语言的部分计值器的论文，而这些命令式语言才是现实世界的主流 语言。 1 9 9 9 年u w e m e y e r 在他的论文i l 叫中给出了一个p a s c a l 的子集，并且做了些修改， 命名为i m p o 。那是一个没有子例程和数据类型的完整语言，但是简略成只有w h i l e 循环。他在论文中给出了i i n p o 的部分计值器的正确性证明，这个证明实际上用的是 归纳法，并且在不同的环境中使用了等价关系进行证明。这是迄今为止第一个在线部 分计值器的正确性证明( 至少就我所知道的) 。 虽然关于带有记录类型、数组类型和指针类型的强类型语言的部分计值器已经被 研究过了，但是对这样的部分计值器的正确性证明还没有给出。按照u w em e y e r 的 说法，他的方法可以推广到这类部分计值器中去。 6 2 1j a v a 语言 第二章j a v a 语言及其字节代码 j a v a 语言是由s u nm i e r o s y s t e m s 为了支持基于i n t e m e t 的产品而设计的一个简单 的、面向对象的、可移植的程序设计语言。尽管很多学生和开发人员曾经或者现在正 在使用c 、c + + 、f o r t r a n 、p a s c a l 和b a s i c 等语言进行程序设计，j a v a 语言利用它在 网络上的独特优势逐渐成为i n t e m e t 上最受欢迎的开发及编程语言。j a v a 语言的广泛 应用是因为它在网络编程方面有传统程序设计语言难以比拟的优点。首先，作为一种 程序设计语言，它简单、不依赖于机器的结构、具有可移植性、健壮性，并且提供了 并发机制；其次，它最大限度地利用了瞬络，其a p p l e t 可以在网络上传输而不受机器 和操作系统地限制。 但由于j a v a 语言是解释执行的，所以其执行速度要比编译执行的c + + 之类的 语言慢一个数量级，这大大制约了j a v a 语言的发展。许多公司都在致力于改进j a v a 编译系统，尤其是j a v a 虚拟机( j a v av i r t u a lm a c h i n e ) 的工作，以期改善j a v a 程序执 行速度慢的缺点。到目前为止，除了传统的采用解释器的j a v a 编译系统，即时编译 器( f l i t ；j u s t i nt i m e ) 的出现对j a v a 性能有了很大的改善。但是因为这些优化都是针对 字节码在虚拟机中的运行方案的，字节代码的效率并没有提高【2 0 l 。现在从事提高代码 效率研究的主要领域是代码转换( c o d et r a n s f o r m a t i o n ) 或者称作程序转换( p r o g r a m t r a n s f o r m a t i o n ) 。部分计值是代码转换研究领域的一个分支，它能够从程序运行环境 和程序自身所包含的已知条件，自动对程序进行例化，生成执行效率更高的程序代码， 缓解j a v a 在平台无关性和执行速度上的矛盾。该技术已经用于一些命令式语言，但 在面向对象式语言领域的研究尚处于起步阶段。 j a v a 语言的部分计值器可以算是部分计值研究领域中的最新的研究方向，在这方 面的研究成果很少。s c h u l t z 和l a w a l l 等人采用通过j a v a - t o - c 编译器将j a v a 程序转 换成c 程序，然后用c 语言的部分计值器t e m p o 2 1 1 计值的办法，已经构造了一个接 近实用的j a v a 计值系统 z z l 。 而由t o k y ou n i v e r s i t y 的m a s u h a r a 和y o n e z a w a 提出的字节代码饲化( b y t e c o d e s p e c i a l i z a t i o n ，b c s ) t 2 习则是以j a v a v i r t u a l m a c h i n e l a n g u a g e ( j v m l ) 【2 4 1 的子集j v m l i 为计值对象，又在s t a t a 和a b a d i 用来构造j a v a 类型系统的类型规则( t y p i n g r u l e s ) 2 5 2 6 1 中选取部分规则描述约束时间分析算法，部分计值后生成经例化的字节码程序。 其中用到了r u n - t i m es p e c i a l i z a t i o n ( r t s ) 技术，r t s 技术就是通过运行时的值 产生有效的例化程序的一种技术。它能够在编译时建立编译过的本机代码碎片( 叫做 模板c e m p l a t e ) ，然后通过仅仅拷贝这些模板而产生例化程序。因为r t s 技术禁 止使用某些优化技术，所以通过它产生的程序比通过静态部分计值技术产生的程序效 率低些。 2 2j a v a 虚拟机语言 2 2l 什么是j a v a 虚拟机 什么是j a v a 虚拟机0 a v a v i r t u a lm a c h i n e ) 呢? 我认为j a v a 虚拟机可以定义为：运 行经过编译的j a v a 目标代码的计算机的实现。它能运行的j a v a 程序，既包括独立的 j a v a 应用程序( a p p l i c a t i o n ) ，也包括下载到诸如i n t e r n e te x p l o r e r ，n e t s c a p en a v i g a t o r 等w e b 浏览器中的a p p l e t 。 一般认为，j a v a 虚拟机是建立在实际的处理器基础上的假想的计算机。在j a v a 语言刚刚推出的一段时间里，j a v a 虚拟机都是通过软件仿真的方法实现的。经过编译 的j a v a 目标代码，我们称为j a v a 字节代码( b y t e - c o d e ) ，再经过本地计算机上的j a v a 解释器的解释，或者经过编译器的编译，就可以运行了。 j a v a 虚拟机不但可以软件实现，也可以用硬件实现。既可以是假想的计算机，也 可以是像s u n v i i c r o e l e e t r o n i c s 公司实现的处理器那样的实用的计算机。当然，目前大 多数的j a v a 虚拟机还是用软件方法实现的。但是，对于j a v a 虚拟机规范来说，是无 论哪种实现都要遵从的。 2 22j a v a 程序生成可执行代码的过程 许多程序设计语言通过对源程序进行编译和链接，直接生成可执行的代码。而 j a v a 语言和它们不同，它的这个过程包括j a v a 程序的编译，字节代码的装入、校验、 解释或者编译。 j a v a 程序首先经过编译，生成字节代码。这个过程由程序开发者的j a v a 编译程 序完成。字节代码的层次大致相当于汇编语言一级。当然，它并不是针对某种特定的 计算机硬件平台的。对变量和方法( 相当于函数1 的引用，并不在编译过程中确定为数 值引用。即通过具体的偏移量的值引用，而是将符号引用的信息保存在字节代码中。 字节代码的装入、校验、解释或者编译，由本地计算机的解释器或者编译器完成。 首先，类装入器装入程序所需要的所有代码，包括程序中调用( u s e ) 、包含( c o n t a i n ) 、 继承( i r d a e r i 0 的所有类的代码。每个类都被装入一个独立的名字空间内，彼此之间只 有通过符号引用才能互相作用。本地的类和外部的类在地址空间上是区分开的。所有 的类都装入以后，可执行代码的内存布局就被确定。由符号引用到内存地址空间的查 询表也建立起来了。然后，字节代码校验器对装入的字节代码进行校验，以排除错误 和不安全的因素。最后，目前通常由解释器解释执行字节代码。但是，解释执行的速 度较慢，一般比c 语言慢1 5 倍左右。而如果编译执行，速度将基本能和c 语言匹敌。 2 23j a v a 虚拟机规范 为j a v a 虚拟机指定规范的一个最明显的理由就是要保证j a v a 代码在任何系统上 都能够运行。凡是符合j a v a 虚拟机规范的实现，都是百分之百兼容的。j a v a 虚拟机 对其实现做出了具体的规定。 j a v a 虚拟机的体系结构直接支持j a v a 语言的这些基本数据类型，包括b y t e 、s h o r t 、 i n t 、l o n g 、f l o a t 、d o i l b l e 和c h a r 。它们的定义是独立于具体的平台的，这为j a v a 程序 的可移植性打下了基础。规范没有对o b j e c t 的内部结构作特殊的要求。由于在各种计 算机体系结构中，寄存器的设置千差万别，所以j a v a 虚拟机采用了面向堆栈的体系 结构，只设置了数量很少的寄存器。这几个寄存器是程序计数器，栈顶指针，运行环 境指针和局部变量指针。这种设置减少了只有少数寄存器或者非通用寄存器的计算机 上实现的困难。而对于拥有较多寄存器的计算机，可以通过具体实现时的优化以充分 利用计算机的资源。j a v a 虚拟机的局部变量和操作数栈都是3 2 位的，l o n g 和d o u b l e 类型需要占据两个3 2 位空间。除了以上方面的内容，j a v a 虚拟机还对运行环境、无 用单元收集堆、方法区、指令集和限制等方面做了规定。 j a v a 虚拟机的程序代码存储在类文件( c l a s s ) 中。每个类文件包含了一个j a v a 类 或者j a v a 接口的编译后的代码。j a v a 虚拟机对类文件的格式做出了规定。 j a v a 虚拟机的指令由操作码和操作数组成。操作码为8 位，理论上最多能够设计 2 5 6 条指令。目前，只有其中的一部分( 2 0 4 条) 被使用。操作数的数目依指令的不同 而不同。除了表跳转指令l o o k u p s w i t c h 和t a b l e s w i t c h 是4 字节对齐以外，其他的指令 都是字节对齐的。 2 3j a v a 虚拟机的体系结构和指令集简介 2 31 支持的数据类型 j a v a 虚拟机支持的j a v a 语言的基本数据类型： b y t e ：1 字节有符号补码整数 s h o r t ：2 字节有符号补码整数 i n t ：4 字节有符号补码整数 l o n g ：8 字节有符号补码整数 f l o a t ：4 字节刀旺 e 7 5 4 单精度浮点数 d o u b l e ：8 字节e e 7 5 4 双精度浮点数 c h a r ：2 字节无符号u i l i c o d e 字符 几乎所有的j a v a 类型检查都是在编译的时候完成的。上面列出的原始数据类型 的数据在j a v a 执行时不需要用硬件标记。操作这些原始数据类型的数据的字节代码 本身就已经指出了操作数的数据结构。例如i a d d ，l a d d ，f a d d 和d a d d 指令都是把两 个数相加，其操作数类型分别是i n t ，l o n g ，f l o a t 和d o u b l e 。 虚拟机投有给b o o l e a n ( 布尔) 类型设置单独的指令。b o o l e a n 型的数据是由整数 指令，包括整数返回来处理的。b o o l e a n 型的数组则是用b y t e 数组来处理的。 9 虚拟机规范使用i e e e 7 5 4 格式的浮点数，并且支持逐步下溢。不支持i e e e 格式 的计算机在运行j a v a 数值计算程序时可能会非常慢。 虚拟机支持的其他数据类型包括： o b j e c t 对一个j a v ao b j e c t 对象的4 字节引用 r e t u r n a d d r e s s 4 字节，用于i s r ，r e t ，j s rw ，r e tw 指令 用j a v a 虚拟机的字节代码表示的程序应该遵守类型规定。j a v a 虚拟机的实现应 该拒绝执行违反了类型规定的字节代码程序。 2 32 寄存器和局部变量 虚拟机在任何时候都是在执行一个单独方法的代码，p c 寄存器包含下一个要执 行的字节代码的地址。 每个方法都有一个为它分配的存储器空间，用于存放：一个局部变量集，由v a t s 寄存器引用；一个操作数栈，由o p t o p 寄存器引用；一个“运行环境”结构，由f l a m e 寄存器引用。 局部变量和操作数栈的大小在编译时就可以得到，“运