（应用数学专业论文）c语言类的公理语义.pdf

摘要 随着程序设计的研究与发展，程序的正确性、可靠性、可维护性等问题受到普遍关注，所以 对程序规范与验证的形式化方法研究有重要的意义。目前，形式化方法的语义研究大致分为四个 分支：操作语义、指称语义、公理语义和代数语义【1 1 ，其中公理语义以程序逻辑为基础，利用最 弱( 宽容) 前置条件( w p ，w e a k e s tp r e c o n d i t i o n ；w l p w e a k e s tl i b e r a lp r e c o n d i t i o n ) 和不变式可以证明程 序的部分正确性和完全正确性，基于此，我们采用公理语义来证明面向对象程序设计语言的正确 性、可靠性和可维护性。 本论文首先在介绍形式化方法和公理语义的基础上，指出了h o a r e 规则和对象不变式在证明 程序部分正确性和完全正确性中的重要作用；其次，我们利用h o a r e 规则和对象不变式，类不变 式，静态数据成员的状态和实例数据成员的状态明确给出了类的公理语义 本文以c 撑语言为背景，重点讨论了类的的公理语义，同时也给出了相关的语言成分的公理 语义。主要工作包括： ( i ) 给出了类的公理语义，包括类的声明、类的静态方法、构造函数的公理语义以及类的 数据成员访问表达式的公理语义。 ( 2 ) 给出了与对象相关的公理语义，包括对象的创建，实例方法调用的公理语义。 ( 3 ) 给出了异常相关的公理语义，包括b r e a k c o n t i n u e 等语句的公理语义。 ( 4 ) 给出了委托、结构、接口等相关的公理语义。 关键词：对象不变式，公理语义，程序验证 a b s t r a c t w i t ht h ed e v e l o p m e n to fp r o g r a m m 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 y a n dm a i n t a i n a b i l i t y , s oo n m a n yf o r m a lm e t h o d so fp r o g r a m m i n gs p e c i f i c a t i o na n df o r m a lc o r r e c t n e s s p r o o fa p p e a rw 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 to ft h em e t h o d o l o g yf o rp r o g r a m m i n g d e s i g n w h i l eo b j e c t - o r i e n t e dp r i n c i p a l sa l ew i d e l yu s e da n dg a i ni n c r e a s i n gi m p o r t a n c ei nt o d a y s s 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 fi st h eh o a r em e t h o d i tu s e si n d u c t i v ef o r m u l a s c 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 rp 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 td e s c r i b e s t h er 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 dd a t as t r u c t u r e ，i ta l w a y sh o l d st r u ea f t e rt h eo b j e c tc r e a t i o na n do n t h ee n t r a n c ea n de x i to ft h em e t h o di n v o c a f 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 d p r o g r a mp r o o f u s i n go 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 fs t a t i cd a t am e m b e r sa n di n s t a n c e d a t am e m b e r s ，a n dh o a r ea x i o ms y s t e m ，w ed e f i n i t e l yg i v et h ea x i o m a t i cs e m a n t i c so fc l a s s i nt h i sp a p e lw em a i n l yd i s c u s st h ea x i o m a t i cs e m a n t i co fc l a s sf o rc 撑i n c l u d i n gt h ec o r r e l a t i v e c o m p o n e n t t h ec o n t e n to f t h ep a p e rc o v e r s ( 1 )g i v et h ea x i o m a t i cs e m a n t i c so fc l a s s i n c l u d i n gt h ea x i o m a t i cs e m a n t i c so fd e c l a r a t i o no f c l a s s ，s t a t i cm e t h o do fc l a s s ，c o n s t r u c t o ra n dd 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 co fo b j e c t i n c l u d i n gt h ea x i o m a t i cs e m a n t i c so ft h en e wi n s t a n c e c 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 ) g i v et h ea x i o m a t i cs e m a n t i co f e x c e p t i o n ，i n c l u d i n gb r e a k ，c o n t i n u ee t ca x i o m a t i cs e m a n t i c s ( 4 ) g i v et h ea x i o m a t i cs e m a n t i co fd e l e g a t e ，s t r u c t e n u me t c k e yw o r d s ：o b j e c 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 gv e r i f i c a t i o n l i 独创性声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成 果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发 表或撰写过的研究成果，也不包含为获得宁夏大学或其它教育机构的学位或证书而使 用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的 说明并表示了谢意。 研究生签名： 衫i 考q 辛 时间：m年f 月钿 关于论文使用授权的说明 本人完全了解宁夏大学有关保留、使用学位论文的规定，即：学校有权保留送交 论文的复印件和磁盘，允许论文被查阅和借阅，可以采用影印、缩印或扫描等复制手 段保存、汇编学位论文。同意宁夏大学可以用不同方式在不同媒体上发表、传播学位 论文的全部或部分内容。 ( 保密的学位论文在解密后应遵守此协议) 研究生签名 导师签名： ：衫瓣 l 了左艾 时间：聊年，月纠角 时间：2 夕fd 年r 月2 臼 寺。夏大学硕十学位论文第一章绪论 曼曼! 曼曼曼! 曼舅曼曼! 曼曼! 苎曼曼孽i 一；一一_ 一 ：；_ m i 曼曼! ! ! 皇曼! 曼! 蔓曼曼曼曼皇 第一章绪论 本章重点介绍c 撑语言的公理语义研究课题的来源和意义，目前国内外对本课题的图内研究 现状，及本课题研究的主要任务等内容。 1 1 课题选题背景 计算机语言的形式语义是目前计算机科学理论研究的两大方向之一，其研究成果对程序设计 语言、编译技术、应用软件、分布式系统等领域有重大的实际意义。 形式语义学的研究可以分为网大流派i 啦! 】：操作语义学，指称语义学、代数语义学和公理语 义学。其中公理语义是在程序正确性验证的基础上发展起来的，是在给定方法的前提下，验证某 种特定的性质是否成立。公理方法的基础是一个逻辑系统，包括一组公理及其推理规则，它区别 于经典逻辑的主要特点是把程序执行效果也考虑进逻辑系统中。 公理语义源自f l o y d 在1 9 6 7 年发表的沦文 a s s i g n i n gm e a n i n gt op r o g r a m s ”1 2 1 。他在该论文中 提出的程序语义描述方法被称为框图语义。他用一组谓词公式来刻丽程序在其运行的不同点上的 状态，称为断言，用以证明程序的部分正确性，即在假定程序运行终止的情况下，判断终止后那 些断言为真。h o a r e 把_ y l o y d 饼j 框图语义和程序正确性证明方法推广到具体的计算机语苦程序上来， 建屯了一套公理系统，称为h o a r e 公理系统，它是形式化证明中最常用的方法。对象在稳定状态 满足对象不变式，最早来自于h o a r e 的关于数据表示的止确性论文0 1 ，e i f i e l 语言最早应用了这一 思想。普遍的观点是把对象不变式看作构造函数调用的后置条件以及每个p u b l i c 方法的前置条件 和后置条件的一种简略的表达式。在面向对象程序的证明中离不丌对象不变式，同时在代码的研 发、修改、维护等方面对象不变式也给我们带来了很大的帮助。 1 2 课题选题依据 随着程序设计的研究与发展，程序的正确性、可靠性、可维护性等问题受到普遍关注。许多 程序规范与验证的形式化方法涌现出来，对程序设计方法学的发展起到了积极的推动作用。尽管 面向对象的方法在软件开发中得到广泛应用并取得了显著成就，但是这个领域的形式化方法仍然 是一个难题。在正确性证明中应用最广泛是h o a r e 方法，它利用逻辑推导来描述程序或程序片段 的输入输出关系。对象不变式，静态数据成员的状态和实例数据成员的状态，并结合h o a r e 公理 系统和指称框架，明确给出了类的公理语义。 在参考文献【1 l 中讨论了面向对象语言的各种语义模型，但它们讨论的是顺序的语言或者是 它的子集，对面向对象语言的特点做了很大的限制，i f i j 对类的描述涉及更少。对象不变式在面向 对象程序的形式化证明方面具有重要作用这方面的研究比较广泛，包括对象不变式的自动牛成、 宁夏大学硕十学位论文第一章绪论 确定、检测和应用 1 2 - 1 7 1 等。通过引入新的谓词和函数来确定公理语义的前置条件和后置条件，从 而描述类的公理语义。利用公理语义可以用于编译、解释c 群程序的生成，验证c 挣语言编写程序的 正确性。 1 3c 捍公理语义研究现状 以往针对面向过程程序设计语言的形式化已经做了很多。文献【4 l 给出c 语言的操作语义，文 献f 5 1 给出了c + + 语言的操作语义。在面向对象语言的描述中，h o a r e 和w i r t h 结合h o a r e 公理系统给 出t p a s c a l 语言的公理语义1 6 1 ，p e t e rb e r t e l s e n 采用指称语义给出了面向对象语言子集的形式化【丌， 其中对于类型安全的证明是通过i s a b e l l a h o l 来实现的。c 撑是基于c + + 和j a v a 的新世纪语言【2 6 j ，是 一种简单、现代、类型安全和面向对象的语言。目前针对c 撑语言的形式化工作研究很少，面向对 象语言的新特点给我们带来了新的机遇和挑战。 1 4 课题的主要工作和内容安排 本节主要简述本课题的主要工作和主要内容安排： 1 4 1 课题研究内容 以形式语义理论为基础，本文的主要研究工作是在c 群语言中对类的公理语义进行研究，以 下是具体的研究内容： ( 1 )给出c 群语言的类的继承的公理语义，包括类的声明、类的静态方法以及构造函数的 公理语义。 ( 2 ) 给出与异常相关的公理语义，包括b r e a k ，c o n t i n u e 语句的公理语义。 ( 3 ) 给出委托、接口、结构等相关语句的公理语义。 ( 4 ) 利用本文所描述的方法，有效地描述其它面向对象语言的公理语义，如c + + ，j a v a 等。 1 4 2 课题内容组织 本文对课题研究的内容技术方法进行了详细的阐述，论文的组织如下： 第一章绪论，总领全文。首先介绍了本课题研究的背景，选题依据以及该课题当前研究现状。 第二章公理语义和程序正确性证明的理论部分，首先从形式语义学的发展说起，给出了公理 语义与h o a r e 逻辑及程序正确性证明相关定理。 第三章主要是讲解c 撑语言类的公理语义，并给出了异常相关的公理语义。 第四章主要给出了委托、结构等相关的公理语义。 第证章总结本文所做的工作及指出进步研究的工作。 2 c j l 夏大学硕十学位论文第二章公理语义和程序正确性订f 明 i ； 一= _i i i i 皇曼皇曼量曼曼曼! ! ! 曼! ! ! 皇曼 第二章公理语义和程序正确性证明 语义学一词出自希腊文，它由动词转化而来，表示语言的意义。一般认为语言学的研究可分 为三部分：语法学，研究语言的形态结构。语义学，研究语言和它所指的对象之问的关系；语用 学，研究语言和它的使用者之间的关系。在计算机语言的范围内，语法学的研究已经相当成熟， 语用学是一个基本上没有被人们所认知的陌生世界，只有语义学是一个正在蓬勃发展的领域，它 是计算机科学中勇敢的探索者的乐园。 2 1 形式化方法 5 0 年代是计算机语言兴起的年代。在这一阶段的早期，计算机语言的设计往往主要强调其“方 便”的一面，而比较忽略其“严格”的一面，因i 面对语占的语义，甚至是语法，未下严格的定义，使 得语言的设计者和语言的实现者，以及语占的使用哲对于同一语言的语义缺乏共同的理解，造成 了一定程度上的混乱。c h o m s k y 关十语占分层理论，以及b a c k u s ，n u a r 关于上下文无关文法表示 形式的研究成果推动了语法形式化的研究。在a l g o l 6 0 的文本设计中第一次使用了b a c k u s n u a r 标准型表示语法，并且第一次在语言文本中明确地把语法和语义区分开来。在5 0 年代和6 0 年代问，面向语法的编译自动化理论研究得到了很大发展，使语法形式化研究的成果达到实用化 的程度。 语法形式化问题基本解决以后，人们开始研究语义形式化的问题。6 0 年代是计算机语言形式 语义学正式诞生的1 0 年，形式语义学的网大流派皆渊源子这一时期。其中，1 9 6 4 年被认为是操 作语义学和指称语义学的诞生年代，l a n d i n 关于操作语义的奠基性文章“表达式的机械化处理”和 s r t a c h e y 关于指称语义的奠基性文章“关于形式语义学”都问世于这一年。1 9 6 7 年则被认为是公理 语义诞生的年代，h o a r e 关于公理语义的奠基性文章“计算机程序设计的一个公理学基础”【3 】就发表 于这一年，最年轻的是代数语义学，它是在抽象数据类型理论的基础上发展起来的，虽然后者的 思想源臼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 - d 、组及g u t t a g 等人。 操作语义的基本思想是用抽象的方法描述语言中每一个成分的执行效果，以免所描述的语义 依赖于该语者实现时所用的具体计算机。通常的做法是设计一个抽象机，定义一组抽象状态，把 语言的语法表示成抽象的形式，然后指明抽象机每加工一个语言成分时将对状态作何种改变。这 种语义力- 法与语言实现的关系比较紧密，但是难以用数学方法处理，而且对语义描述者个人使用 的实现方法依赖很大。 计算机语言的指称语义被公认为标准的形式语义。指称语义的基本思想是用一组与语言成分 相对应的定值函数将程序的语法元素映射到语义域，使其对应干一个数学对象，用定义在对象上 的运算( 町递归定义) 给出程序的精确含义。在指称语义方法中，没有求值过程和执行过程的细 节，牛婪刻而数据加工的结果。典型的方法是把程序看作是沦域上的泛函以刻丽程序的数学结果， 3 宁夏大学硕卜学位论文第二章公理语义和程序正确件讦明 i i i ! 笪曼曼曼曼曼曼曼曼舅曼曼曼鼍曼曼曼曼曼曼量曼曼曼曼曼曼曼蔓曼曼曼曼曼曼曼曼! ! ! ! ! ! 曼曼曼曼曼曼曼曼曼曼曼曼曼曼曼曼! 曼曼曼! ! 曼蔓! 曼曼曼曼曼! 皂曼曼曼! 曼詈 而泛函的不动点是一个非常重要的概念，可用来严格地刻画循环程序和递归程序的含义。 公理语义具体见下面小节。 指称语义最早由c s t r a c h e y 提出，d s c o t t 奠定了其数学基础【l l 。因为使用了完全偏序、连 续函数和不动点等更为抽象的数学概念，因此也曾被称为“数学语义”【2 捌。指称语义学具有牢固的 数学基础，提供了最有深度和广度的可用技术，不仅用于程序设计语言的研究，而且已经拓展到 了软件工程、软件方法学、程序理论、计算语言学、通信以及数据类犁理论等诸多研究方向【4 。8 l 。 另一方面，指称语义方法用到了数理逻辑、泛函、拓扑学和形式语言等学科的许多概念，具有较 高的抽象层浏1 引。 代数语义学的基本思想是把描述语义的逻辑体系和满足这个逻辑体系的模型区分开来。任何 程序的操作语义或指称语义描述只给出该程序的一个语义模裂，而公理语义描述则只给出逻辑系 统，不深入讨论其可能的模型( 近年来这种情况己经有所改变，特别是对非h o a r e 型逻辑) 代数语 义方法的特点就是用代数方法来处理满足一个逻辑系统的各种模型，把模型的集合看成是一个代 数结构。因此，在代数语义中，除了要研究类似于健康性和完备性等公理体系的概念外，还要研 究模型之间的关系。简而言之，它要处理的是一整个模型族。 形式语义学文献中使用的技术和方法并不一定都能归入上面所说的四大流派，但这四大流派 确实代表了形式语义学中最重要的四个研究方向，相对地说，在公理语义和代数语义中，尚待研 究和解决的闯题比起操作语义和指称语义要多一些。 当前研究兴趣的集中点之一是各种非h o a r e 犁逻辑体系，在公理语义和代数语义中都有这种 情况。至于哪种逻辑最有前途，目前尚无定论。近年来类型理论倍受青睐，似乎义预示着研究 构造性逻辑的热浪即将兴起。总之，这里还是各种逻辑群雄逐鹿的局面。文献【2 2 】给出了形式化方 法的作用。 当前研究兴趣的另一个集中点是不确定和并发性分布式程序的形式语义。上面提到的三个方 面的形式语义研究还有很长的一段路要走。例如，操作语义的偏序推导和变迁系统，指称语义幂 域理论和不动点理论，都是研究分布式语义的有力的手段，但都还不完整。文献i l3 】总结了近年来 在形式化方面各工作小组所作的工作和成果。 2 2 公理语义与h o a r e 逻辑 公理语义是在程序正确性验证的基础上发展起来的，它是在给出一种方法的前提f ，验证某 种特定的性质是否成立。如： 研e x 】 x ：= p 尸 ， 表示若在执行赋值语句时前启条件p i x i e 成立，则在执行后，条件p 成立。因此，公理方法是以 个逻辑系统为丛础，包括一组公理及其推理规则，它区别于经典逻辑的主要之点是把程序执行 的效果也考虑进逻辑系统中。公理语义学的核心课题是研究这类逻辑系统的健康性和完备性。近 年来，模态逻辑和二时序逻辑以及无穷逻辑和构造性逻辑等一些非h o a r e 犁的公理语义方法陆续 出现，大大丰富了这。一领域的研究。 形式语义学文献中使用的技术和方法并不+ 定都能归入上面所说的四大流派，但这四大流派 4 宁夏大学硕i ：学位论文第二章公坪语义和程序正确性证明 确实代表了形式语义学中最主要的四个研究方向。 一般认为，公理语义渊源自f l o y d 在1 9 6 7 年发表的论文“a s s i g n i n gm e a n i n gt op r o g r a m s ”。他 在该文中提出的程序语义描述方法常称为框图语义。他用一组谓词公式来刻画程序在其运行的不 同点上的状态，称为断言，用以证明程序的部分正确性，即在假定程序运行能终止的情况下，判 断终止后那些断言能成立。因此，这里所说的状态不同于指称语义中所说的状态，这里的状态不 必包含所有变量的取值情况，而只需标明编程者所要求的程序的性质。例如，编程者可能希望程 序具有如下性质：如果初始变量值x 邓，则程序运行终止后，另两个变量z 和t 之间有关系z = t 成立。在这里x ，弘z ，t 究竟取哪个具体值是无关紧要的，这一点就与指称语义的要求不同。 f l o y d 方法的最大缺点就是它的结构性能比较差。如果一个语句由几个语句复合组成，人们希 望有一种方法能直接从各分量的正确性推导出整个复合语句的正确性，并进而把这个方法应用于 整个复合程序。f l o y d 方法很难担当这个任务。于是，一种改进的逻辑语义方法产生了，这就是 h o a r e 在1 9 6 9 年发表的那篇文章“a na x i o m a t i cb a s i sf o rc o m p u t e rp r o g r a m m i n g ”中首创的方法，通 常被人们称为h o a r e 逻辑【3 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 逻辑把r l o y d 的框图语义和程序正确性证明方法推广到具体的计算机语苦程序上，并 建立了一套公理系统，称为h o a r e 公理系统。在这个系统中，公理和命题的形式是： 尸 9 足 ， ( 2 2 1 ) 其中p 称为前置条件，q 代表一个程序，足称为后置条件。它的意思是：如果在程序( 或语句) q 执行前，前置条件p 成立，且9 的执行能终止，则在q 执行后，必有后置条件尺成立。 下面列出h o a r e 逻辑的五条基本公理，如下： ( 1 ) s k i p 规则： p s k i p p ， ( 2 2 2 ) 如果在s k i p 执行之前的状态下谓词p 为真，那么在s k i p 执行之后的谓词也为真，凶为该状态没 有发牛变化。 ( 2 ) 赋值规则。赋值语 i j 是计算机语言t i i 最常见的语句，如下： 工：= p ， 其中工是一个变量，e 是表达式。 如果要求谓词p 0 ) 在执行赋值表达是后为真，则在执行之前，谓诃地) 必须为真，即： p e x 】) x7 - e p ) ，( 2 2 3 ) 其中p e x 表示把谓侧尸中x 的所有自【| f 出现替换为e ，并把p 中所有约束变量换成e 中没有的 名字。 ( 3 ) 条件规则 条件语句：i f bt h e nq 1e l s eq 的公理形式是 ! ! 全皇! 鱼璺! ! 仝! ! 堡塑，( 2 2 4 ) p ) 矿bt h e n 岛e l s eq 2 r 5 p 夏大学硕r f j 学位论文笫二：章公珲语义和程碍正确性订明 曼曼皇曼鼍曼曼曼曼曼曼曼曼曼曼量曼曼曼曼寡曼曼! 曼! 曼! 皇! 曼曼曼! - ii ：ii z i_ _ i lil： 其含义是，若横线上面的断言都成立，则横线下面的断言也成立。横线上面以逗号隔开的断言按 合取计算。 ( 4 ) 复合规则 计算机语言的程序般都是语句的线性序列。因此有一个语句组合问题。不失一般性，这里 只考虑两个语句的顺序组合：q i ：q 2 ! 竺型墨幽幽( 2 2 5 ) 尸 q ；q t ) 。 复合规则表示：如果 毋g 尉和 埘q 2 n 是有效的，则 n q ；q 2 i f 也是有效的，即如果 在满足尸的状态下，9 的成功执行终止于满足月的状态，且在满足尺的状态下，q 2 的成功执行终止 于满足珀勺状，则在满足状态p 的状态下q l 和q 2 相继成功执行后，也终止于满足确状态。 ( 5 ) 循环规则 循环语句有不同的形式，这里采用一种形式作为代表，即w h i l e 语句： w h i l e b d oq 其中曰表示条件，q 是语句。对循环公理需要注意的是：第一，如果有某个条件尸，当它作为前 置条件时，执行q 不会对它产生影响，尸常被称作循环不变式；第二，终状态要满足尸且退出循 环时也要满足书，因此书应是w h i l e 语句的后置条件，于是 一鲨仝塑塑 ( 2 2 6 1 尸 w h i l eb d o q o d - 1 b 尸 定义1 以上的五条公理合在一起称为h o a r e 公理系统，以h 代表。 ( 6 ) 推断规则 p q r , r - - s ；( 2 2 7 ) 尸) g s ) p q r , t - - ) p ( 2 2 8 ) 丁 烈埘 ( 7 ) 析取规则 ! 墨! 垡型墨! 垡堡 ( 2 2 9 ) # v ，q 尺) ( 8 ) 合取规则 ! ! 型墨! 塑垒堡! 阻l o ) p 娥墨 r 。 ( 9 ) 穷举规则 ! 生! 垡坠：! 墨! 望翌 ( 2 2 1 1 ) # v v vt q r 、 ( 1 0 ) 换名规则 ! 竺型壁一一 ( 2 2 1 2 ) p y x q 【y x l r y x 】 。 其中x 在尸，q 尺中均为自变量( 可不出现) j ，是一个新的变量。 ( 1 1 ) 框架j ! i l 则 6 宁夏大学硕十学位论文第一：章公理语义和程序正确件证明 p q p ( 2 2 13 ) 若条件p 和q 没有公共变量，则q 的执行应对尸没有影响。 2 3 程序正确性证明 直观地说，所谓一段程序是正确的，是对满足一定条件的输入、输出而言，通常把满足这个 程序段的输入条件和输出条件分别称为该程序的输入断言和输出断言，常用 ) ，力表示。这 里，x ，y 分别表示输入信息和输出信息。 严格的程序正确性定义一般分为部分正确性、终止性和完全正确性三种类型，分别定义如下： 定义l ( 部分正确性) 若对每个使得，( d 为真，并且程序计算终止的输入信息l0 ( f j 弋f ) ) 为真， 称程序尸关于，和q 是部分正确的。即： 1 ( 0a p , 1 0o ( i ，p ( f ) ) ， 这里，尸( f ) 表示与输入的信息f 相对用的程序p 的输出信息，p 上表示程序尸终止。 定义2 ( 程序终止性) 若对每个使得，( f ) 为真的输入信息f ，程序计算终止，称程序p 对， 是终止的，即： ，( f ) 3p 、i ， 定义3 ( 完全正确性) 若对每个使得，( f ) 为真的输入f ，程序的计算都终止，并且d ( f ，( 功为 真，称程序尸关于，和d 是完全正确的，即： ，( f ) 3p0 d ( f ，p ( 劝 显然，程序的完全正确性等价于该程序是部分正确的且又是终止的。为此，程序的完全正确 正确性证明通常分为部分正确性和终止性两部进行。研究程序完全正确性的方法丰要有： ( 1 ) 证明部分正确性的方法： a f l o y d 的不变式断占法 b m a n n a 的子目标断言发 c h o a r e 的公理化方法 ( 2 ) 证明终止性方法： a f l o y d 的良序集方法 b k u n t h 的计数器方法 c m a n n a 等人的不动点方法 ( 3 ) 证明完全正确性的方法： a m a n n a 等人对h o a r e 公理化方法的推广 b b u r s t a l l 的问断言方法 c d i j k s t r a 的弱谓词变换方法及强验证方法 2 3 1 部分正确性 证明程序部分正确性的公理化方法就是依据以上几条公理和规则进行的。推理过程中般有 两种形式： 7 宁夏大学硕十学位论文第：章公理语义和程序正确忡i j 下明 ( 1 ) 根据给出的不变式断言，建立一些引理，根据这些引理和公理，对程序p 中的每一个赋 值语句f i 导出相应的不变式语句 p 9 r 。根据这些不变式语句和上述的几条规则逐步 组成越来越长的程序段，一直到推出 烈x ) 尸 l ( 工，z ) 为止。这样，就证明了程序p 的部分正确性。 ( 2 ) 从不变式语句 烈x ) 尸 吵( 墨z ) 出发，利用有关的规则将它逐步分解，一直到将所有的语句推演为逻辑表达式( 即检查 条件) 。然后证明这些逻辑表达式成立。这样，就证明了程序的部分正确性。 1 不变式断言法 下面以例l 说明该方法证明程序部分正确性的过程。 例l 设x ，y 是正整数，下面程序是求x , y 的最大公约数z 的程序，即z = g c d ( x , y ) 。 i n tx ，y , z ，s p r o g r a m g o d r e a d ( x ，y ) ； w h i l ex ! = o i f ( ) ， x ) y 2 y 。x ； e l s e s 2 x ： x = y ； y 。s ； 矛7 ； ) 8 宁夏大学硕十学位论文第二章公理语义和程序正确性证明 程序的流程图如图2 1 所示 i ( x ) z - - y 1r 厂、 l 姗 0 ( x 。p ( x ) ) 图2 1 求最大公约数 证明： ( 1 ) 建立输入、输出断言和循环不变式。 设x ，y 的初始值为勒抛，可分别建立输入断言厶输出断言d 、不变式三如。f ： 舷) ：x o 0a 儿0a ( 而o v 0 ) ； d # ) ：z = g c d ( x o , y o ) ； 上( j f ：x 0ay 0 ( x o o vy o 0 ) g c d ( x ，力= g c d ( x o ，) ( 2 ) 在每条路径上建立验证条件。 a 瑟取) 成立，当第一次到达上处时，o ) 成立，l l 七l r j x = x o , y = y o ，可得图中c l 处的验证条件l ： c l o r ) ：【x o o y o 0 ( o o v y o 0 ) 】 = ，【而0 a y 0 o ( x o 0 v y o o ) a g c d ( x o ，虬) = g c d ( x o ，) 】 b 当y x 时，回到三，可得途中c 2 出的验证条件2 ： 9 宁夏大学硕十学位论文 第一二章公理语义和程序正确忡t i f 明 曼曼皇曼曼曼舅曼曼曼曼舅舅蔓曼舅皇曼iiii i ii ； 一 u l 曼曼曼曼寰鼍! 曼舅曼篡曼曼! 曼曼曼曼曼曼曼曼! 曼! 舅 c ， ) ：【工0 y o ( x 0 v y o ) 】 g c d c x , y ) 。g c d ( x o ，) x 0 y 明 j 【戈o y - x 0 ( x 0 v y x o ) g c d ( x ，y 一_ x ) = g c d ( x o ，) 】 c 当心时回到三，可得图c 3 处的验证条件3 ： c ，( j f ，y ) ： 【x 0 y 0 a ( x 0 v y o ) 】 g c d ( x , 力 = g c d ( x o ，y o ) x 0 y 0 为真 当y 0 时，g c d ( 0 哼 可由( x = 0 g c d ( x , y ) = g c d ( x o ，y o ) ) = y = g c d ( x o ，y o ) 该程序的部分正确性证毕。 2 公理化方法 定义4 不变式语