（计算机软件与理论专业论文）java语言的类和多态性的公理语义.pdf

大连理工大学硕士学位论文 摘要 本文以j a v a 语言为背景，重点讨论了类的继承和多态性的公理语义，同时也给出 了必要的及相关的语言成分的公理语义。主要工作包括： ( 1 ) 给出了类的公理语义，包括类的声明、类的静态方法、构造函数的公理语义以 及类的数据成损访问表达式的公理语义。 ( 2 ) 给出了与对象相关的公理语义，包括对象的创建，实例方法调用的公理语义。 ( 3 ) 数组也是对象，我们给出了与数组相关的公理语义，包括数组实例仓建表达式 和数组访问表达式的公理语义。 ( 4 ) 因为类的继承和多态性是面向对象程序设计语言的一种机制，而非一种语言成 分，故以不同于上述三类语言成分的方式描述它们的公理语义。 随着程序设计的研究与发展，程序的正确性、可靠性、可维护性等问题受到人们的 普遍关注。许多程序规范与验证的形式化方法涌现出来，对程序设计方法学的发展起了 积极的推动作用。但是尽管厦向对象的方法在今天的软件开发中得到广泛应用并取得显 著的成就，这个领域的形式化正确证明方法仍然是一个难以解决的问题。在正确性证明 中最广泛应用的方法是h o a r e 方法，它利用推导公式来描述程序或程序片断的输输出 关系。对象不变式描述了面向对象数据结构中元素间的关系，在对象创建后以及方法引 用前后它总为真。对象不变式在面向对象程序的证明中具有重要作用。利用对象不变 式，类不变式，静态数据成员的状态和实例数据成员的状态，并结合h o a r e 公理系统， 我们明确给出了类的公理语义。 多态性是面向对象程序设计的个重要特点，也是难点，在使用时最容易发生错误 和误解。在用公理语义描述多态性的时候，由于我们使用的描述方法是静态的，而被描 述对象是动态的，所以在描述多态性的时候需要做大量工作。本文通过引入新的谓词和 函数确定了用公理语义描述多态性的前置条件和后置条件，从而描述了多态性的公理语 义。 利用我们给出的公理语义可以用于编译、解释j a v a 程序的生成；验证用j a v a 语言 编写的程序的正确性。 关键词：对象不变式：公理语义；程序验证 j a v a 语言的类和多态性的公理语义 a x i o m a t i cs e m a n t i c so fc l a s sa n d p o l y m o r p h i s m f o rj a v a a b s t r a e t i nt h i sp a p e r , w e m a i n l y d i s c u s st h ea x i o m a t i cs e m a n t i c so fc l a s sa n dp o l y m o r p h i s mf o r j a v a , i n c l u d i n g t h ec o r r e l a t i v ec o m p o n e n t l ec o n t e n to f t h e p a p e r c o v e r s ： ( 1 ) g i v e t h e 莉0 1 n a d cs e m a n t i c s o f c l a s s ，i n c l u d i n gt h ea 】【i o l 删cs e m a n t i c so f d e c l a r a t i o n o f c l a s s ，s t a t i cm e t h o do f c l a s s ，c o n s t r u c t o ra n d d a t am e m b e r s ( 2 ) g i v et h ea x i o m a t i cs e m a n t i c so f o b j e c t , i n c l u d i n gt h ea x i o m 甜cs e m a n t i c so f t h en e w i n s t a n c ec r e a t i o ne x p r e s s i o na n dt h ei n s t a n c em e t h o di n v o c a t i o n ( 3 ) a r r a y i sa n o b j e c t , s ow eg i v e t h ea x i o m a t i cs e m a n t i c s o f a r r a y , i n c l u d i n g t h ea x i o m a t i c s e m a n t i c s o f a r r a y c r e a t i o n e x p r e s s i o na n da r m y a c c e s se x p r e s s i o n _ ( 4 ) t h ei n h e r e n c eo fc l a s sa n dp o l y m o r p h i s mi sam e c h a n i s mr a t h e rt h a nal a n g u a g e c o m p o n e n t , s o i ti sd e s c r i b e di nt h ed i f f e r e n t w a y s f r o mt h ea b o v et h r e ek i n d s w i t ht h ed e v e l o p m e n to f p m 掣m n n l i n gd e s i g n , p e o p l ep a ya t t e n t i o nt ot h ec o r r e c t n e s s ， r e l i a b i l i t ya n dm a i n t a i n a b i l i t ya n d s oo n m a n yf o r m a lm e t h o d so f p r o g r a m m i n gs p e c i f i c a t i o n a n df o r m a lc o e s s p r o o fa p p e a r , w h i c ht a k ea ni m p o r t a n tr o l ei nt h ed e v e l o p m e n t o ft h e m e t h o d o l o g yf o rp r o g r a m m i n gd e s i g n w k ko b j e c t - o r i e n t e dp r i n c i p a l sa r ew i d e l yu s e da n d g a i ni n c r e a s i n gi m p o r t a n c e i n t o d a y ss o f t w a r ed e v e l o p m e n t , t h ef o r m a lc o r r e c t n e s sp r o o f i s s t i l l ah a r dp r o b l e m t h em o s tw i d e l yu s e dm e t h o di nt h ef o r m a lc o r r e c t n e s sp r o o fi st h eh o a r e m e t h o d i tn s e si n d u c t i v ef o r m u l a sc h a r a c t e r i z i n gi n p u t o u t p u tr e l a t i o n s h i p so fp r o g r a m so r p r o g r a ms e g m e n t s o b j e c ti n v a r i a n t d e s c r i b e st h e r e l a t i o n s h i po ft h eo b j e c t - o r i e n t e d d a t a s t r u c t u r e i ta l w a y sh o l d st r u ea l t e rt h eo b j e c tc r e a t i o na n do nt h ee n l r a n c ea n de x i to ft h e m e t h o di n v o c a t i o n o b j e c ti n v a r i a n ti si m p o r t a n ti nt h eo b j e c t - o r i e n t e dp r o g r a m p r o o f u s i n g o b j e c ti n v a r i a n t s , c l a s si n v a r i a n t s ，t h es t a t eo f s t a t i cd a t am e m b e r sa n di n s t a n c ed a t am e m b e r s ， a n dh o m ea x i o m s y s t e m , w ed e f i n i t e l yg i v et h e a ) 【i o l a t i cs e m a n t i c so f c l a s s p o l y m o r p h i s mi s a ni m p o r tc h a r a c t e ra n dh a r dt ob eu n d e r s t o o di nt h eo b j e c t - o r i e n t e d p r o g r a m m i n gd e s i g n , s o i t se a s yt om a k eam i s t a k ew h e n u s m g i t 、) i v h e nd e s c r i b ei t sa x i o m a t i c s e m a n t i c s ，t h e r ea r eal o to f t a s k sw h i c hs h o u l db er e s o l v e db e c a u s ew eu s es t a t i ca t t r i b u t e st o d e s c r i b ed y n a m i ca t t r i b u t e s t l l i sp a p e ri n t r o d u c e sn e w p r e d i c a t i o na n df u n c t i o nt 0s e l e c tt h e p r e c o n d i t i o na n dp o s t c o n d i t i o n , w ed e s c r i b et h ea x i o m a t i cs e m a n t i c so f p o l y m o r p h i s m u s i n gt h ea x i o m a t i c s e m a n t i c sw h i c ha g i v e n w ec a nc o m p i l ea n di n t e r p r e t et h e p r o d u c t i o n o f j a v a p r o g r a m ；t h e y a l s oc a nc h e c kt h ec o h e c t n e s so f t h e p r o g r a m s k e yw o r d s ：0 b j e e ti n v a r i a n t ；a x i o m a t i cs e m a n t i c s ；p r o g r a m m i n g v e r i f i c a t i o n 独创性说明 作者郑重声明：本硕士学位论文是我个人在导师指导下进行的研究 工作及取得研究成果。尽我所知，除了文中特别加以标注和致谢的地方 外，论文中不包含其他人已经发表或撰写的研究成果，也不包含为获得 大连理工大学或其他单位的学位或证书所使用过的材料。与我一同工作 的同志对本研究所做的贡献均已在论文中做了明确的说明并表示了谢 意。 作者签名：焦渔塑日期：型：三：至l 大连理工大学硕士学位论文 引言 计算机语言的形式语义是目前计算机科学理论研究的两大方向之一，其研究成果对 程序设计语言、编译技术、应用软件、分布式系统等分支领域有重大的实际意义。 程序语义是指程序的含义，形式语义学是对形式语言及其程序采用形式系统进行语 义定义的学问。目前形式语义学可分为四大流派【1 】：操作语义学，指称语义学，代数语 义学，公理语义学。其中公理语义是在程序正确性验证的基础上发展起来的，它不像其 它语义学方法那样，对程序语义做宏观的全局性描述，而只是给出一种方法，使人们 能在给定的前提下，验证某种特定的性质是否成立。公理方法的基础是一个逻辑系统， 包括一组公理及其推理规则，它区别于经典逻辑的主要之点是把程序执行的效果也考虑 进逻辑系统中。 一般认为，公理语义渊源自f l o y d 在1 9 6 7 年发表的论文“a s s i g n i n gm e m a i n gt o p r o g r a m s ”【2 】2 。他在该文中提出的程序语义描述方法常称为框图语义。他用一组谓词公 式来刻画程序在其运行的不同点上的状态，称为断言，用以证明程序的部分正确性，即 在假定程序运行能中止的情况下，判明中止后哪些断言能成立。 h o a r e 把f l o y d 的框图语义和程序正确性证明方法推广到具体的计算机语言程序上 来，并建立了一套公理系统，称为h o a r e 公理系统，它也是形式化证明中最常用的方 法。对象在稳定状态，满足某些数据不变性的思想，也就是对象不变式，最早来自于 h o a r e 的关于数据表示昀正确性论文 3 ，e i f f e l 语言最早应用这一思想。普遍的观点是 把对象不变式看作构造函数调用的后置条件以及每个p u b l i c 方法的前置条件和后置条件 的一种简略的表达方式。在面向对象程序的正确性证明中离不开对象不变式，同时在代 码的开发、修改、维护等方面对象不变式也有帮助。在我们给出的公理语义中，基本上 都涉及了对象不变式。 以往针对面向过程程序化设计语言的形式化已经做了很多。 4 】给出了c 语言的操 作语义，而 5 给出了c _ h 的操作语义。在h o a r e 公理系统的基础上，h o a r e 和w i r t h 合 作给出了p a s c a l 语言的分程序的公理语义和过程的公理语义以及联立子程序的公理语 义，并在此基础上给出了p a s c a l 语言的公理语义【6 】。但j a v a 语言是面向对象语言，面 向对象程序设计语言的新特点给我们带来了新的机遇和挑战。 在对面向对象的描述中，早期的p a s c a l 语言中给出了基于类的形式化，但只给出了 类程的公理语义 1 】，类程的一般形式如下： c l a s s t ： j a v a 语言的类和多态性的公理语义 b e g i n c l ，c 2 ，c 1 1 诸变量的说明 p r o c e d u r ep 1 ；q 1 ； p r o c e d u r ep 2 ；q 2 ； p r o c e d u r ep m ；q m ； q e n d ； 其中p i 是过程名，q i 是相应的过程体，这些过程作用于诸变量c j 之上，q 是初启 程序，可用于给诸c j 赋值。可以在过程前加上类型说明，此时过程成为函数。t 是类程 名。 在说明了类程之后，可以用它来说明变量，此处我们采用了p a s c a l 的形式： v a r t l ，t 2 ，t k ：t ； 抽象数据类型的一个特点是，把对数据施行的操作和数据本身约束在一起了，因 此，对诸t i 可施行的操作只能是那些p i 。为了区别，把t i 和p i 结合在起形成过程调 用，即 t i p i 表示调用的过程属于t i ，它也可以是函数调用，此时写成： x ：- - t i p i 然后在此基础上，针对j a v a 语言的形式化做的很少。p e t e rb e r t e l s e n 采用指称语义 给出了j a v a 语言子集的形式化【7 ，其中对于类型安全的证明是通过i s a b e l l e h o l 来实 现的。但尚未全部完成，仍在继续。 面向对象程序设计在程序的形式化方面给我们带来了很大便利，如面向对象系统在 某种意义上是合成的，所以它们可以按层分开形成协作定向的集合，它们的属性和职责 都已单独定义好，这有助于找到前置条件，后置条件和不变式：对象状态和方法之间的 紧密耦合使得容易选择方法调用的前置条件，后置条件和不变式：通过继承机制，抽象 类到具体类的规范可以精确表达，面向对象程序语言的这个特点弥补了形式分析。但也 给我们提出了新的问题，如通过继承，类可以逐步修改并增加新的功能，新类与旧类以 复杂的方式交互，而多重继承产生多个上下文并使得问题更复杂；动态绑定的非预期邦 定或对正确使用的错误理解，使得问题的描述更加复杂等。 在参考文献 8 9 1o 1 1 q h 讨论了j a v a 语言的公理语义，但它们讨论的是序列化的 j a v a 语言或者是它的子集，对j a v a 语言的特点做了很大限制，并没有完全体现j a v a 语 一2 一 大连理工大学硕士学位论文 言的特性，而对于类和多态性的描述涉及的很少。对象不变式在面向对象程序的形式化 证明方面具有重要作用，这方面的研究比较广泛，包括对象不变式的自动生成 1 2 1 、确 定、检测【1 3 1 4 】 1 5 】和应用 1 6 【1 7 等。本文在系统总结和学习前人在面向过程程序语 言以及在面向对象程序语言形式化描述的成果的基础上，通过深入分析j a v a 语言的特 点，明确给出了j a v a 语言中与类和多态性的公理语义。 利用我们给出的公理语义，我们可以更深入的了解j a v a 语言在类，对象以及多态 性等方面的特点 1 8 1 9 1 1 2 0 ，并进而理解面向对象程序设计语言的特点。同时，利用我 们给出的公理语义，并结合前人给出的j a v a 语言各种成分的公理语义，可以形式化的 证明j a v a 程序的正确性，从而解决了面向对象程序设计在形式化证明方面遇到的难 题。当然，要完全按照j a v a 语言规范给出各种成分的公理语义，还有许多工作要做， 如把异常处理机制也考虑进去，这就需要更多的人在这方面付出更多的努力。 一3 一 j a v a 语言的类和多态性的公理语义 1 形式化方法及公理语义 语义学( s e m a n t i c s ) - - 词出自希腊文，它由动词转化而来，表示语言的意义。一一般认 为语言学的研究可分为三部分：语法学，研究语言的形态结构；语义学，研究语言和它 所指的对象之间的关系；语用学，研究语言和它的使用者之间的关系。三者合在起， 组成了指号学的最重要部分。在计算机语言的范围内，语法学的研究已经相当成熟，语 用学是一个基本上没有被人们所认知的陌生世界，只有语义学是一个正在蓬勃发展的领 域，它是计算机科学中勇敢的探索者的乐园。 1 1 形式化方法 5 0 年代是计算机语言兴起的年代。在这一阶段的早期，计算机语言的设计往往主 要强调其“方便”的一面，而比较忽略其“严格”的一面，因而对语言的语义，甚至是 语法，未下严格的定义，使得语言的设计者和语言的实现者，以及语言的使用者对于同 一语言的语义缺乏共同的理解，造成了一定程度上的混乱。c h o m s k y 关于语言分层理 论，以及b a c k u s ，n a u r 关于上下文无关文法表示形式的研究成果推动了语法形式化的 研究。其结果是，在a l g o l 6 0 的文本设计中第一次使用了b a c k u s n a u r 标准型表示语 法，并且第一次在语言文本中明确地把语法和语义区分开来。后来，在5 0 年代和6 0 年 代1 日j ，面向语法的编译自动化理论研究得到了很大发展，使语法形式化研究的成果达到 实用化的程度。 语法形式化问题基本解决以后，人们逐渐把注意力集中到语义形式化方面。6 0 年代 可以说是计算机语言形式语义学正式诞生的1 0 年，形式语义学的四大流派皆渊源于这 一时期。其中，1 9 6 4 年被认为是操作语义学和指称语义学的诞生年代，l a n d i n 关于操 作语义的奠基性文章“表达式的机械化处理”和s t r a c h e y 关于指称语义的奠基性文章 “关于形式语义学”都问世于这一年。1 9 6 7 年则被认为是公理语义诞生的年代，h o a r e 关于公理语义的奠基性文章“计算机程序设计的一个公理学基础” 2 1 就发表于这一 年，最年轻的是代数语义学，它是在抽象数据类型理论的基础上发展起来的，虽然后者 的思想源自1 9 6 7 年问世的s i m u l a 6 7 ，但正式把它提到抽象数据类型高度的是l i s k o v 和 z i l l e s 在1 9 7 4 年的工作，而把它进一步上升为代数语义学则是7 0 年代中期以后的事 了。当时的主要代表人物有g o g u e n 等人的a d j 小组及g u t t a g 等人。 操作语义的基本思想是用抽象的方法描述语言中每一个成分的执行效果，以免所描 述的语义依赖于该语言实现时所用的具体计算机。通常的做法是设计一个抽象机，定义 一组抽象：汰态，把语言的语法表示成抽象的形式，然后指明抽象机每加工一个语言成分 d 大连理工夫学硕士学位论文 时将对状态作何种改变。这种语义方法与语言实现的关系比较紧密，但是难以用数学方 法处理，而且对语义描述者个人使用的实现方法依赖很大。 指称语义的基本思想是使语言的每一个成分对应于一个数学对象，该对象称为该语 言成分的对象，它不像操作语义那样涉及语言成分的执行过程，而是只考虑各成分执行 的最终效果，并认为此最终效果应不依赖于其执行过程。由于语言成分可以是很复杂 的，甚至让人怀疑这样的指象在数学上是否存在的程度。s c o t t 创建的论域理论解决_ ， 这个问题，从而为指称语义学奠定了坚实的理论基础。后来的s m y t h 和p l o t k i n 等人建 立了幂域理论，为不确定的和并发的以及分布式程序的指称语义奠定了基础。 公理语义具体见下一节。 代数语义学的基本思想是把描述语义的逻辑体系和满足这个逻辑体系的模型区分开 来。任何程序的操作语义或指称语义描述只给出该程序的一个语义模型，而公理语义描 述则只给出逻辑系统，不深入讨论其可能的模型( 近年来这种情况已经有所改变，特别 是对非h o a r e 型逻辑) 代数语义方法的特点就是用代数方法来处理满足一个逻辑系统的 各种模型，把模型的集合看成是一个代数结构。因此，在代数语义中，除了要研究类似 毋健康性和完备性等公理体系的概念外，还要研究模型之间的关系。简而言之，它要处 理的是一整个模型族。 戴形式语义学文献中使用的技术和方法并不一定都能归入上面所说的四大流派，但这 四大流派确实代表了形式语义学中最重要的四个研究方向。相对地说，在公理语义和代 数语义中，尚待研究和解决的问题比起操作语义和指称语义要多一些。 当前研究兴趣的集中点之一是各种非h o a r e 型逻辑体系，在公理语义和代数语义中 都有这种情况。至于哪一种逻辑最有前途，目前尚无定论。有人看好时序逻辑，有人欣 赏无穷逻辑。近年来类型理论倍受青睐，似乎又预示着研究构造性逻辑的热浪即将兴 起。总之，这里还是各种逻辑群群雄逐鹿的局面。文献 2 2 给出了形式化方法的作用。 有分就有合。也有人研究如何构造一个超级逻辑体系，把各种具体的逻辑系统都容 纳进去，例如e d i n b u r h 学派的i n s t i t u t i o n 理论。 当前研究兴趣的另一个集中点是不确定和并发性分布式程序的形式语义。上面提到 的三个方面的形式语义研究还有很长的一段路要走。例如，操作语义的偏序推导和变迁 系统，指称语义幂域理论和不动点理论，都是研究分布式语义的有力的手段，但都还不 完整。文献【2 3 总结了近年来在形式化方面各工作小组所作的工作和成果。 操作语义和指称语义并没有失去其生命力。有两个情况使操作语义的的研究保持着 一定的势头。其一是p l o t k i n 在1 9 8 1 年发明的结构化操作语义，给人们操作语义重新焕 一5 一 j a v a 语言的类和多态性的公理语义 发青春之感：以机构化操作语义为基础的变迁系统已普遍用于各类语言，包括分布式语 言的语义描述中。其二是在论述其它语义的正确性时，操作语义至今仍常被作为“参照 系”而使用。至于说到指称语义，则在不少计算4 j t * 4 学家的心目中，它仍然是一种“标 准”的语义描述方法。 四种语义方法融合的倾向值得注意。它的一种表现是各方法之间的边界逐渐模糊， 互相采用对方的长处，有些语义方法已很难绝对地划入某一阵营。另一种表现是有人试 图建立一种超级方法体系，把四种现有方法都纳入其中作为子方法，在程序的不同开发 阶段根据各方法的特点量才录用。 l - 2 公理语义 公理语义是在程序正确性验证的基础上发展起来的，它不像其它语义学方法那样， 对程序语义作宏观的全局性描述，而只是给出一种方法，使人们能在给定前提下，验证 某种特定的性质是否成立。如： p 【e 悯) x ：飞 p ) 。 表示若在执行赋值语句肝e 前条件p 【嘲成立，则在执杼后条件p 成立。因此，公 理方法的基础是一个逻辑系统，包括一组公理及其推理规啦咤区别手经典逻辑的主要 之点是把程序执行的效粟也考虑进逻辑系统中。公理语义学的梆心课题是研究这类逻辑 系统的健康性和完备性。近年来，一些所谓的非h o a r e 型的公理语义方法陆续出现，如 模态逻辑和时序逻辑以及无穷逻辑和构造性逻辑等，大大丰富孓这一领域的研究。 形式语义学文献中使甩的技术和方法并不一定都能归入上面所说的四大流派，但这 四大流派确实代表了形式语义学中最主要的四个研究方向。 一般认为，公理语义渊源自f l o y d 在1 9 6 7 年发表的论文“a s s i g n i n gm e a n i n gt o p r o g r a m s ”。他在该文中提出的程序语义描述方法常称为框图语义。他用一组谓词公式 来刻画程序在其运行的不同点上的状态，称为断言，用以证明程序的部分正确性，即在 假定程序运行能终止的情况下，判明终止后那些断言能成立。因此，这里所说的状态不 同于指称语义中所说的状态，这里的状态不必包含所有变量的取值情况，而只需标明编 程者所要求于程序的性质。例如，编程者可能希望程序具有如下性质：如果初始变量值 x = y ，则程序运行终止后，另两个变量z 和t 之间有关系z = t 成立。在这里，x ，y z ，t 究 竟取哪个具体值是无关紧要的，这一点就与指称语义的要求不同。 f l o y d 方法的最大缺点就是它的结构性能比较差。如果一个语句由几个语句复合组 成，人们希望有一种方法能直接从各分量的正确性推导出整个复合语句的正确性，并进 而把这个方法应用于整个复合程序。f l o y d 方法很难担当这个任务。于是，一种改进的 6 大连理工大学硕士学位论文 逻辑语义方法产生了，这就是h o a m 在1 9 6 9 年发表的那篇文章“a na x i o m a t i cb a s i sf o r c o m p u t e r p r o g r a m m i n g ”中首创的方法，通常被人们称为h o a r e 逻辑 2 1 。 自从h o a r e 逻辑问世以后，公理语义学的研究基本上围绕三个方面进行。第一个方 面是运用这个逻辑手段去描述计算机语言中各种各样成分的语义。第二个方面是深入研 究h o a r e 逻辑中尚不清楚或尚待解决的理论问题，例如它的健康性和完备性问题。第三 方面是寻找h o a r e 逻辑以外的其他逻辑手段，它们可以用来弥补h o a r e 逻辑的不足，或 处理那些h o a r e 逻辑解决不了的问题。 h o a r e 逻辑把f l o y d 的框图语义和程序正确性证明方法推广到具体的计算机语言程 序上来，并建立了套公理系统，称为h o m e 公理系统。在这个系统中，公理和命题的 形式是： p ( q 球( 1 2 1 ) 其中p 称为前置条件，q 代表个程序，r 称为后置条件。它的意思是：如果在程 序( 或语句) q 执行前，前置条件p 成立，且q 的执行能终止，则在q 执行后，必有 后置条件r 成立。现在许多文献中习惯于采用另一种书写方法，突出前置条件p 和后 置条件r ，把它们圈起来，形式为： ( p q ( r ( 1 2 2 ) 下面列出h o a r e 逻辑的四条基本公理，如下： ( 1 ) 赋值公理。赋置语句是计算机语言中最常见的语句( k n u t h 的一个统计表明，在 f o r t r a n 程序中，赋值语句占全部语句数的5 0 ) 赋值语句，如下： x = e 其中x 是个变量，e 是表达式。 如果要求谓词p ( x ) 在执行赋值表达式后为真，则在执行之前，谓词p ( e ) 必须为真， 此即： p e x 】) x = e p 一7 一 ( 1 2 3 ) j a v a 语言的类和多态性的公理语义 其中p e x 表示把谓词p 中x 的所有自由出现均代之以e ，并把p 中所有约束变量 换成e 中没有的名字。 ( 2 ) 条件公理 条件语句：i f bt h e n q 1 e l s e q 2 的公理形式是 ! ! 全皇! 鱼! 墨! ：! ! 全二皇! 望2 1 墨! e fb t h e nq 1e l s eq 2 q ( 1 2 4 ) 其含义是，若横线上面的断言都成立，则横线下面的断言也成立。横线上面以逗号 分开的诺断言按合取计算。 ( 3 ) 组合公理 计算机语言的程序一般都是语句的线性序列。因此有一个语句组合问题。不失一般 性，这里只考虑两个语句的组合：q i ；q 2 1 1 1 堡! 墨! ! ! 墨! 堡! 三! p ) q l ；q 2 r ) ( 1 2 5 ) 这里的分号表示两个语句的组合。 ( 4 ) 循环公理 循环语句有不同的形式，这里采用一种形式作为代表，即w h i l e 语句： w h i l e b d o q o d 其中b 表示条件，q 是语句。对循环公理的考虑是，第一，如果有某个条件p ，当 把它作为前置条件时，程序q 的执行不会对它产生影响，则不管q 执行多少遍也不会 对它发生影响。p 常被称作循环不变式。第二，条件b 不成立是不再执行语句q 的前 提，因此也应是w h i l e 语句的后置条件，于是 ! ! ! 垒墨! ! 望! ! ! p w h i l e b d o q o a b p 定义1 以上的四条公理合在一起称为h o a r e 公理系统，以h 代表。 8 一 ( 1 2 ，6 ) 大连理工大学硕士学位论文 ( 5 ) 推断公理 ! ! ! 翌! 墨! ! 墨二三兰 p ) q s ) ! ! ! 望i 墨! ：! = 三竺 r ) q r ) ( 6 ) 析取公理 析取公理的一个特殊情况是穷举公理 ! 墨! 叟! 墨! ：! 墨! 望! 墨! ( 墨v 最) q r ) ( 7 ) 合取公理 ! ! ! 望! 墨! ! ! ! ! 望! 墨! ! p i q r 。 r ：) ( 8 ) 穷举公理 ! 墨! 垡! 墨! = = ：! ! 墨! 璺! 墨! ev bv v 只) q r ) ( 9 ) 换名公理 ! ! ! 望! 墨! p y x 】) q y 胡 r y x ) 其中x 在p ，q ，r 中均为自由变量( 可不出现) y 是一个新变量。 ( 1 0 ) 框架公理 9 ( 1 2 7 ) ( 1 _ 2 8 ) ( 1 2 9 ) ( 1 2 1 0 ) ( 1 2 1 1 ) ( 1 2 1 2 ) j a v a 语言的类和多态性的公理语义 p q p ) ( 1 2 1 3 ) 条件p 和q 没有公共变量，则q 的执行应对p 没有影响。 1 3 公理语义的完全正确眭 完全正确性的研究是公理语义研究中不可或缺的重要组成部分，但是多年来人们的 研究工作主要集中在部分正确性方面。完全正确性的研究成果不大丰富的原因，第一， 在于它的形式化程度没有达到描述部分正确性的公理系统那样的高度，第二，也许更主 要的是部分正确性只涉及程序的局部性质，而完全正确性却关系到程序的全局性质，其 难度要大得多。因此，在已有的成果中，理论成分较少而技术成分较多。但这并不影响 完全正确性的重要性，继续进行深入的研究是十分必要的。 证明一个程序的完全正确性主要有两条途径，第一条途径是把停机问题和部分正确 性分开处理，把两部分结果合在起，就得到了程序的完全正确性：第二条途径是建立 一个统一的公理系统，试图一举证明完全正确性。实际上，d i j k s t r a 的谓词变换函数、v p 就包含了这样的思想。 对于依赖经验的程序的证明中，最困难的挑战是写出由输入条件和输出条件构成的 精确规范。另一个是找到适合完成程序证明的不变式。面向对象程序提供一个更直觉的 方式来构造这些约束 2 4 】。因为对象是模拟现实概念并且按照性质和它们自身约束来构 造，所以发现这些约束应该更容易和更直接。 一个面向对象系统是正确的，如果组成它的所有类都是正确的。一个类是正确当且 仅当关于它的约束满足 2 5 1 ： ( 1 ) 对于除构造函数以外的每个公共方法，在方法执行前的所有不变式和前置条 件的有效性蕴含着方法结束后所有不变式和后置条件的有效性； ( 2 ) 对于每个构造函数假定当进入构造函数时，所有的属性值初始化为它们相应 类型的默认值，所有前置条件的有效性蕴含着所有不变式的有效性。 像传统程序语言的正确性定义一样，前置条件，后置条件和不变式定义了指定面向 对象系统的方式。但是，由于面向对象程序语言的特殊特点，h o a r e 方法如不扩展将不 能处理整个系统。 1 4 与异常有关的语句的公理语义 异常由于如下三种原因发生： 1 0 一 大连理工大学硕士学位论文 ( 1 ) 当j a v a 虚拟机检测到程序执行进入非正常状态时所抛出的异常 2 6 】。例如：表 达式计算过程中出现除数为零；请求内存分配失败； ( 2 ) 在多线程环境下，由于执行t h r e a d 类中的s t o p 方法，所引发的异常 ( 3 ) 由t h r o w 语句的执行所引发的异常 公理语义的主要目的之一就是证明程序的正确性。像上面( 1 ) 中所说的“除数为零” 这种异常，纯粹是程序错误引起的；“内存不够”这种异常，可能是由于程序错误引起 的。由于程序错误引起的异常，理论上可以通过程序验证的方法发现。但是“内存不 够”这种异常，也可能是与机器的规模相比程序所要求的资源太多了。这种类型的异常 与程序的运行环境有关，并不是由程序本身错误引起的，理论上这种异常不能够通过程 序验证的方法发现。对于这类与程序运行环境有关的异常，程序员应该检测到这些并加 以处理。在本文中，我们只关心由t h r o w 语句抛出的异常。 为了描述j a v a 语言的公理语义，引入四个全局变量，r e a s o n ，eo b j ，l a b e l 和v a l u e 可以认为这四个全局变量由j a v a 虚拟机自身来管理，它们的含义如下： ( 1 ) r e a s o n ：一个字符串变量，每个语句执行结束之后，该变量的值被自动设置 为语句的完成原因，如果语句正常完成，r e a s o n 的值为n u l l ，否则值为一个字符串， 描述完成原因。如下面的例子： 执行t h r o we ；之后r e a s o n 的值为“t h r o w ”。 r e t u r n ：语句的执行后，终止原因为“r e t u r n w i t h n o v a l u e ”。 r e t u r n e x p ：语句的执行后，终止原因为“r e n a n w i t h v a l u e ”。 ( 2 ) eo b j ：一个j a v a 1 a n g z h r o w a b l e 型的对象，初值为n u l l ，当执行t h r o w 语句 时，eo b j 自动设置成t h r o w 语句所抛出的异常对象，当执行c a t c h , r e t u m 语句时， eo b j 又被自动置为n u l l 。r e a s o n 和eo b j 相结合可以表示“t h r o ww i t hv a l u e n ”， ( 3 ) l a b e l ：一个字符串变量，当执行b r e a ki d e n t i f i e r 或c o n t i n u ei d e n t i f i e r 时，这个 变量的值被自动设置成i d e n t i f i e r 。r e a s o n 和l a b e l 相结合可以表示“c o n t i n u ew i t h l a b e li d e n t i f i e r ”和“b r e a kw i t hl a b e li d e n t i f i e r ”。 ( 4 ) v a l u e ：每当表达式计算正常完成时，这个变量被自动设置成表达式的值。 r e a s o n 和v a l u e 相结合可以表示“r e t u r n w i t h v a l u ev ”。 1 4 “f 语句的公理语义 1 4 1 1 语法 i f ( e x p ) s l e l s e s 2 j a v a 语言的类和多态性的公理语义 1 4 1 2 语义 ( 1 ) 计算表达式e x p ，如果因为抛出异常而突然完成，则i f 语句也因为“t h r o w ”突 然完成。 ( 2 ) 如果e x p 正常完成，则视e x p 为t r u e 或f a l s e ，分别计算s l 或s 2 。如果s 2 正常 完成，则i f 语句正常完成；如果s 1 或s 2 因某种原因突然完成，则i f 语句因同样原因突 然完成。 1 4 1 3 公理语义 1 4 1 3 1 表达式e x p 的计算正常完成，执行s 1 或者s 2 时正常完成，则有： p e x p q r e a s o n = n u l l ， q v a l u e s l ( r r e a s o n = n u l l ) 面搽丽雨磊i 瓦而瓦面石而矿一 ( 1 4 1 ) ( p e x p q r e a s o n = n u l l ， q v a l u e s 2 孟 r e a s o n = n u l l 面丽面两磊西面习面丽丽磊面一 ( 1 4 2 ) 1 4 1 3 2 表达式e x p 的计算正常完成，执行s i 或者s 2 时突然完成，则有： 盟咝竺黑f 型( e x p ) 卷e l s 篙es 罴r 坠e a s o 罴nx 等型( 1 4 3 ) p )s2 月= ”7 1 1 1 1 翌丝尘墨竺璺堡翌三竺! 坐! ! 坠二! 圭丝! 墨! 墨尘型璺里型三兰尘兰兰! 竺! ( 1 4 4 ) p f ( e x p ) s le l s e ( r r e a s o n = x 上面两条公理可进一步合并为如下公理 p e x p q r e a s o n = n u l l ， q v a l u e s l r r e a s o n = x ) ， ! 坠二! 墨塑! 兰21 墨2 尘丝! 型三羔! ( 1 4 5 ) p f ( e x p ) 墨e l s e ( r 2 r e a s o n = x ) v ( r 2 r e a s o n = y ) 。 1 4 1 3 3 表达式e x p 的计算突然完成 p e x p q r e a s o n = ”t h r o w ” 层一o b j = 工) pf(exp)stelse$2qreason=throwae_obj=x ( 1 4 6 ) 。1 2 大连理工大学硕士学位论文 1 4 2r e t u r n 语句的公理语义 1 4 2 1 语法 ( 1 ) r e t u r n ； ( 2 ) l t u l ne x p ； 1 4 2 2 语义 ( 1 ) r e t u r n ；试图传递控制权给引用者，语句总因“r e m mw i t hn ov a l u e ”，而突然完 成。 ( 2 ) r e t u r ne x p ；语句首先计算e x p ，如果计算e x p 由于某种原因突然完成，则 r e t u r n 语句由于同样原因突然完成，否则得到e x p 的值v ，那么整个r e t u r n 语句因为 “r e t u n lw i t hv a l u ev ”而突然终止。 1 4 2 3 公理语义 1 4 2 3 1 没有返回值的i