（系统分析与集成专业论文）可证编译器.pdf

华东师范大学硕士学位论文 目录 学位论文独创性声明 本人所呈交的学位论文是我在导师的指导下进行的研究工作及取得的研究 成果。据我所知，除文中已经注明引用的内容外，本论文不包含其他个人已经 发表或撰写过的研究成果。对本文的研究做出重要贡献的个人和集体，均已在 文中作了明确说明并表示谢意。 作者签名： 学位论文使用授权声明 本人完全了解华东师范大学有关绦留、使用学位论文的规定，学校有权保 留学位论文并向国家主管部门或其指定机构送交论文的电子版和纸质版。有权 将学位论文用于非赢利目的的少量复制并允许论文进入学校图书馆被查阅。有 权将学位论文的内容编入有关数据库进行检索。有权将学位论文的标题和摘要 汇编出版。保密的学位论文在解密后适用本规定。 学位论文作者签名：i h 丘拳 日期：艘雌：丛f 。 导师签名：百能 日期： 卫n 。拿魄! f 兰查堑蔓盔兰堡主兰垡笙茎一一 垦墨 o r i g i n a l i t yn o t i c e i np r e s e n t i n gt h i st h e s i si np a r t i a lf u l f i l l m e n to f t h er e q u i r e m e n t sf o rt h em a s t e r s d e g r e ea te a s tc h i n an o r m a lu n i v e r s i t y , 1w a r r a n t t h a tt h i st h e s i si so r i g i n a la n da n y o ft h et e c h n i q u e sp r e s e n t e di nt h et h e s i sh a v e b e e nf i g u r e do u tb ym e a n yo ft h e r e f e r e n c e st ot h ec o p y r i g h t ，t r a d e m a r k ，p a t e n t ，s t a t u t o r yr i g h t ，o rp r o p r i e t yr i g h to f o t h e mh a v eb e e ne x p l i c i t l ya c k n o w l e d g e da n di n c l u d e di nt h er e f e r e n c e ss e c t i o na t t h ee n do f t h i st h e t i s s i g n a t u r e ： c o p y r i g h tn o t i c e ih e r e i na g r e et h a tt h el i b r a r yo f e c n us h a l lm a k ei t sc o p i e sf r e e l ya v a i l a b l ef o r i n s p e c t i o n if u r t h e ra g r e et h a te x t e n s i v ec o p y i n g o f t h et h e s i si sa l l o w a b l eo n l yf o r s c h o l a r l yp u r p o s e s ，i np a r t i c u l a r , s t o r i n gt h ec o n t e n to f t h i st h e s i si n t or e l e v a n t d a t a b a s e s ，a sw e l la sc o m p i l i n ga n dp u b l i s h i n gt h et i t l ea n da b s t r a c to f t h i st h e s i s ， c o n s i s t e n tw i t h ”f a i r 惦e ”a sp r e s c r i b e di nt h ec o p y r i g h tl a wo f t h ep e o p l e s r e p u b l i co f c h i n a 啦咖糟：山噼血牡 2 华东师范大学硕士毕业论文 可证编译器 摘要 编译器的定义就是一段程序，它能读一些用抽象( 几乎是数学的) 记号表 述的用户程序并将其翻译成更晦涩难懂的但能在计算机上直接运行的机器码。 一个严重的问题是许多编译好的程序含有错误，些错误甚至会导致程序崩溃。 检测和消除这些错误就需要艰辛的劳动，即费时耗力的调试过程。 为了减少错误或者写出正确的编译程序，并且尽量避免艰辛的调试过程， 计算机科学家在这几十年来做了大量的工作：比如最初的为程序加入断言，到 后来的精化程序。 本文就是用软件实现编译器代码生成的一篇论文。它能把o c c a m 语言翻 译成自定义的类汇编代码。 o c c a m 语言是一种简洁的面向过程的语言，它非常类似于流行于世的c 、 p a s c a l 等语言，而且比c 更加简洁明了。更为重要的是，o c c a m 语言以其能够 处理并行和通信的特性，使其在2 1 世纪仍有重要的研究价值。因此，对o c c a m 的编译就显得尤为重要，这也是本文选用o c c a m 的原因。 本文的特色就在于综合了前人的证明思路，不但给出了完整的o c c a m 语 言编译子旬，而且用数学定理和模拟的方法证明了编译程序的正确性( 无需测 试，代码生成是完全正确的) 。具体来说，本文采用精化的理论，证明o c c a m 语言和类汇编代码之间是有精化关系的，而这种证明过程中的数学定理形式， 被直接写成编译程序的子句。因此，编译程序本身的正确性就毋庸质疑。但数 学定理的形式与常用的c 、j a v a 等语言有一定差距，为了不节外生枝，我们采 用人工智能的p r o l o g 语言对o c c a m 语言实行编译。对于处理并行和通信的 o c c a m 部分，直接采用定理的方式是有困难的，因此本文采用仿真的办法，来 浇明我们最后完成的类汇编代码，执行的操作都在源程序允许的范围之内，来 说明编译程序的正确性。本文的独创性也就在这里：第一次将两种方式用在一 起来证明编译的正确，并且在文章的后面，给出了完全模拟编译的环境并给出 实验结果。 关键词形式化，精化，规范，模拟 华东师范大学硕士毕业论文 可证编译器 a b s t r a c t c o m p i l e r i sd e f i n e da sa p r o g r a n w h i c h c a l lt r a n s l a t es o m e a b s t r a c t ( m o s t l y m a t h e m a t i c s ) l a n g u a g e si n t oc o d e s ，u s u a l l ym o r ec o m p l i c a t e d ，w h i c hc a r ld a nd i r e c t l yi nc o m p u t e r b u tas e r i o u sp r o b l e mi st h a tm o s tp r o g r a m sh a v ee r r o r s ，a n ds o m ee r r o r sc a nb l o wu pp r o g r a m s 。 f i n d i n ga n dc o r r e c t i n gt h e s ee r m r s ，o rd e b u g g i n g ，a r ct i m ea n d e f f o r tc o n s u m i n g ， i no r d e rt ow r i t ec o r r e c tc o m p i l e rp r o g r a m so rr e d u c ee r r o r s c o m p u t e rs c i e n t i s t sh a v et r i e d m a n yw a y ss i n c e19 6 0 s ：f o re x a m p l e ，a d d i n gs o m ea s s e r tt ol a n g u a g e ，a n dr e f i n e m e n tc a l c u l u se t s t h ea i mo ft h i sp a p e ri st oi l l u s t r a t eh o wt od e s i g nc o r r e c tc o m p i l e ra n dw r i t es o m ec o d ei n o r d e rt ot r a n s l a t eo c c a ml a n g u a g ei n t oa s s e m b l ec o d ew h i c hi sd e f i n e di nt h i sp a p e r o c c a m i sap r o c e s s i n gl a n g u a g e 埘t 1 1s i m p l ea n dg r a c e f u lm e a n i n g o c c a mi ss i m i l a rt os o m ep o p u l a r l a n g u a g el i k ec ，p a s c a l ；a n di ti ss i m p l e rt h a nc a n dt h em o s ti m p o r t a n tt h i n g ，o c c a mc a n d e a lw i t hp a r a r e l la n dc o m m u n i c a t ep r o b l e m s ，s oi t i sv e r yp o p u l a ra n dh a v eg r e a tv a l u ei n2i c e n t u r y t h a ti st os a y , c o m p i l i n go c c a m i sv e r yi m p o r t a n t a n dt h a t st h er e a s o nw h yw es e l e c t o c c a m t h ec h a r a c t e r i s t i co ft h i sp a p e rl i e si ns ：m t h e s i z i n gf o r e f a t h e r s m e t h o d so fi d e n t i f i c a t i o n w e p r o v i d et h eo c c a ml a n g u a g ea n dt h ec o m p i l i n gc l a u s e s f u r t h e r m o r e ，t h ec o i t e c t n e s so fc o m p i l e r i sp r o v e db ym a t h e m a t i ct h e o r e mm a ds i m u l a t i o n ( t e s ti sn o tn e c e s s a r y , a st h ec o d ep r o d u c e di s c o m p l e t e l yc o r r e c t ) r e f i n e m e n tt h e o r yi su s e dt op r o v et h a tr e f i n e m e n tr e l a t i o nb e t w e e no c c a m l a n g u a g e a n da s s e m b l el a n g u a g ee x i s t s + a n dt h em a t h e m a t i ct h e o r e mf o r mi nt h i sk i n do f i d e n t i f i c a t i o nc o u r s e ，i sw r i t t e na st h ec l a u s eo f t h ec o m p i l e rd i r e c t l y t h e r e f o r e ，t h ec o m p i l e ri t s e l fi sc o r r e c t b u tt h e r ea r es o m ed i f f e r e n c e sb e t w e e nt h ef o r mo f m a t h e m a t i c st h e o r e ma n dt h ec o m m o np r o g r a m m i n gl a n g u a g es u c ha sc ，j a v a i no r d e rt oa v o i d c o m p l i c a t i o n ，w ea d o p tp r o l o gl a n g u a g eo fa r t i f i c i a li n t e l l i g e n c ew h i c hc a nc o m p i l eo c c a m l a n g u a g e h o w e v e r , i ti sd i f f i c u l tt od e a lw i t ht h ep a r a l l e la n dc o m m u n i c a t i o np r o b l e m si no c c a m b yu s i n gt h et h e o r e mp r o v ed i r e c t l y , s ow eu s et h es i m u l a t i o nm e t h o dt oe x p l a i nt h a ta s s e m b l e c o d e sf i n i s h e df i n a l l ya n do p e r a t i o nc a r r i e do u ta r ew i t h i nr a n g et h a ts o n r c ep r o g r a ma l l o w s t h e c h a r a c t e ro ft h i sp a p e ri s ：i ti st h ef i r s tt i m et op r o v et h ec o r r e c t n e s so fac o m p i l e rb yt w od i f f e r e n t w a y s ，a n da tt h ee n do f t h i sp a p e r , w ep r o v i d et h ee n v i r o m n e n tc o m p i l e di nc o m p l e t es i m u l a t i o na n d t e s t i n g k e yw o r d s f o r m a lm e t h o d ，r e f i n e m e n t ，s p e c i f i c a t i o n ，s i m u l a t i o n 2 华来师范大学硕士毕业论文 可证编译嚣 1 1 概述 第一章绪论 本文主要围绕编译程序的正确性进行讨论。编译程序自六十年代以来就成为计算机的核 心，在计算机中起着举足轻重的作用。而且，伴随着计算机技术的发展，编译程序也扮演着 越来越重要的角色。而自程序的正确性证明被提出来之后，对编译程序的讨论就一直在进行 中，可证编译器的思想，也越来越成熟”。我们在这里说的正确性，是指编译程序在把 源语言翻译成目标语言的过程中，必须保证其行为( 语义) 的正确性，而且这种正确性必须 是可以被证明的“”。 本文并不是将一种源语言完整正确地翻译成目标代码而是对面向过程中的赋值、条件、 循环结构以及处理并行和通信的语句给出数学定理的编译规则，这些规则对于保证编译器的 正确性非常重要”1 ，而且，也容易根据这些规则写出完整的可用于工程的编译程序。 本论文 将整个编译过程分成如下几个部分： 源语言与目标语言介绍 过程语言编译过程 并行与通信语言编译过程 编译程序的p r o l c ( ；实现 下面分别对上述几个部分进行概括地介绍。 1 i 1 源语言与目标语盲介绍 本文要进行编译的源语言是o c c a m 。1 语言的一个子集，采用o c c a m 的原因是： 首先，o c c a m 语言是一种命令式语言，在顺序、分支、循环语句中十分类似c 、p a s c a l 等语言，较有普遍性，而且，o c c a m 语言又相当简单，使我们可以集中要讨论的问题，而不 至于陷入繁琐的细技末节中( 比如类型检查、书写格式等) 。 其次，o c c a m 的魅力在其并发、通信的特性上，因为当今时代，并行处理已成为计算机 的热门话题。o c c a m 将并行、通信等现代技术表达的相当简洁，而将大量的工作交给编译器 来处理。下面在写编译器的时候，会对各种技术有较详细全面的介绍。 作为一个例子，我们在下面给出个o c c a m 源程序的形式( 文法将在以后的篇幅中介绍) ： 华东师范大学硕士毕业论文可证编译器 i n tx ，y ： c h a no fi n tc ： p a r c15 ： s k i p ： p a r y ：= 6 ： w h i l ey ( 1 0 y ：= y + l ： p a r c ? x ： i fx = 5 x ：2 x + l ： 本文的任务就是将这种源程序翻译成目标代码，而目标代码主要在自定义的自动机上运 行。 自动机( 文献 9 对此有其解释) 有一个寄存器( 执行代码) ，一个指针，一个存储器( 存 储代码) 能够执行如下类似命令： l d l ( a d d r ) 可以将地址从内存取到存储器 a d c ( c o n )将常数与寄存器中的值相加后放入寄存器 s t a r t ( p ) 调度进程p 详细的介绍将在下文给出。采用这种定义的做法是为了避免与硬件相关，本文对编译程 序的讨论不应该因为硬件的不同丽不同，也不应该因为多c p u ，或分布式的区别而有所改变， 所以本文将问题的讨论限制在符号上是有益的。 1 1 2 过程语言编译过程 对于普通的顺序，分支，循环语句，我们采用在同一个公理系统下精化的证明方式保证 编译的正确“”3 。首先给出精确意义下的编译规范。比如说，我们首先将目标程序中的地址 与源程序中的变量建立一种对应关系，然后，把目标代码的实现用高级语言程序表示。比如： “ l o a d ( n ) = a ，p ：- m 疗】，p + i a q - c j u m p ( k ) = p ：= ( p + l 司a p t ) 等 这样，两个程序就同属个逻辑空间，而编译程序c 就是这两种程序的一个函数关系， c ( p ) = q 如果能够证明是p 的精化“，那么阀题就解决了。本文就是用这种证明方式保证编译 的正确，并给出已经证明的规则。 比如： c ( s e q p k ，p ) s f m m j f c ( p i ) s l l m q a r ) 华东师范大学硕士毕业论文 可证编译器 c ( s e q p 2 ，只】) 锄甲q 而这种编译规范与p r o l o g 语言极其相似我们用p r o l o g 就直接写成 c ( s e q 口j r 】，s ，f ，m ) ： c ( p ，s ，l ，m 1 ) ， c ( s e qr ，l ，f , m 2 ) ， a p p e n d ( m i ，m 2 ，m ) ， 上面的规则由于已经正确，所以下面的编译语句也是正确的( 当然我们必须假定相信 p r o l o g 编译器) 。 1 1 3 并行与通信语言编译过程 而对于o c c a m 的并行，通信特性“1 ，我们首先制作一个调度函数，将o c c a m 的进程细 分块，并且决定他们执行的先后顺序和通信，然后用模拟来保证正确，所谓模拟就是在目标 程序的实现和源程序之间建立一个映照，然后证明出对于目标程序的每一步，源程序都有相 应的动作与之对应，从而完成证明过程。 1 1 4 编译程序的p r o l o g 实现 本论文用人工智能p r o l o g 语言“作为编译程序的实现语言，原因是因为本文是通过数学 的定理，精化规则“”“7 1 来保证编译过程的正确。本文给出的编译规范大部分是数学定理的性 质。而p r o l o g 作为一种逻辑语言，与数学定理的模式非常相似，用p r o l o g 写的程序，就像 证明用的定理一样，而如果采用流行的c ，b a s i c ，会增加把数学定理编译成c 的工作量，而 更为糟糕的是：如果那样做，把数学定理能否正确的编译成c 语言，又成为一个问题，还需 要另起炉灶，重新证明。因此，实际上，本文重点讨论的是编译规范的问题，和对并行的调 度处理。在本论文的第6 章，我给出了部分的p r o l o g 代码，供大家参考。 1 2 国内外研究历史及现状 对于编译程序的正确性问题，计算机学家们做过了大量的尝试来解决。他们所采用的方 法，根据定义的源语言及目标语言的语义的不同或者根据编译过程的不同而呈现出多种多样 的形态。最早进行这种尝试的，当属m c c a r t h y 及p a i n t e r ”，他们用操作语义3 对一个简 单的表达式语言的正确性进行了解释；至于用数学算法进行证明的，则开始于b u r s t a l l 和 l a n d i n 在传统的编译算法中，正确性的证明可用下图简单的表达出来：这个图表最早是由m o r r i s 给出的，它也是建立在b u r s t a l l 和l a n d i n 工作的基础之上。 兰墨婴苎查堂堡主望些垒塞 源语言 目标代码 可证编译器 源代码语义反编译目标代码语义 相似的，我们也可以建立在指称语义的基础上对程序的正确性进行证明：事实上，虽然 上面的方法是基于代数的，但是可以看成是对源语言及目标语言的一种指称的定义，而进行 这方面尝试的当属p o l a k 。”他的方法要比上面的图表简单些，因为他在源语言及目标语 言中采用相同的语义模式，这样，在上面图表的d e c o d i n g 箭头，对p o l a k 来说只是一个恒等 的变换。 尽管在定义源语言与目标语言时的语义各有不同，但是在证明编译程序正确性问题上的 方法却大同小异，上面的方法橛括起来，无外乎以下凡步： 源语言与目标语言的语法表示 他们的语义 语法语义之间的变换函数 编译程序本身的表示 可以将源语言及目标语言进行比较的变换关系 上面方法的不同仅仅是在每一步的解释方式上有所差别而已。在之后的一段时间，也有 好多编译程序的设计是采用如此的方法：例如d e s p e y r o u x 的方法就非常相似于上面图表 的方法，除了它是用关系而不是函数来代替箭头，这样做的优点在于可以解释非确定的语言， 其他的方法，例如文献 2 3 ，采用观测相等的意义来定义源语言与目标语言的代数意义。 从以往的经验来看，尽管已出现了形形色色的证明方法，但是要简化这种证明过程仍然 是一种挑战，关键的原因在于在规范与程序之间有一道鸿沟，必须采用一个关系或者函数来 对两者进行转换，这样才能使两者之间存在可比性。有什么更好的方法昵? 解决的方法是：把规范空间与程序空间进行统一，而这一点已经成功做到，在程序的统 性理论中，程序空间被理解成规范空间的子集，这种方法可用精化理论进行很好的解释， 我们将在下文给出精化理论的简要介绍。 华东师范大学硕士毕业论文可证编译器 1 3 本文的组织结构 除去本章，可以将整个文章看作是三部分： 第一部分是对本文需要的背景知识进行必要的介绍，其中共分为两章 第二章对正确性证明中需要用到的逻辑和格的相应的知识进行概括地介绍。 第三章主要介绍用于我们定义编译规范的精化理论，这一理论是写规范的核心问题。 第二部分是对源语言o c c a m 和目标汇编代码进行介绍，这一部分的重点是其数学的定理。 第四章对源语言o c c a m 进行概括的非形式化的介绍，突出其并行通信的特性。 第五章详细介绍o c c a m 源语言与机器指令的文法表示及形式化的介绍其语义。 第三部分是编译的规范和实现。有了前面的基础，这一部分的实现是顺理成章的事情。 第六章详细介绍过程语句编译程序的实现过程及理论依据。 第七章介绍通信和并行部分的实现过程，这一章重点是介绍我们用p r o l o g 模拟情 况。 第八章总结与展望。 另外，本文给出了三个附录： 附录l 简要介绍了p r o l o g 语言的语法，附录2 给出了调 度程序的代码及举例论证，附录3 是硕士期间发表的论文。 华东师范大学硕士毕业论文 可证编译嚣 第二章谓词格理论简介 这一章主要的目的就是对本文以后要用到的逻辑和格的理论作一些简要地介绍，为精化 理论和后面的介绍打个基础。如何证明数学定理将在下文中逐渐展开。 在下面的讨论中，我们用标准的集合论和逻辑符号来表示相关的概念。比如我们用 r ，f ，、b ，b c ，b y e ，b j c ，b c 分别表示t r u e ，f a l s e ，逻辑非，和取，析取，蕴含，等价等 操作。而当然我们用v 表示任意符号而j 表示存在符号等等。 2 1 偏序关系和完备格 一个偏序关系是指一个二元组( s ，) ，其中s 是一个元素集合而是一个定义在s 上 的二元关系( 偏序关系) 。其中对任意的x ，y ，z 属于s ，满足下面的三条性质： 1 x x 2 ( x y ) ( y z ) j ( x c z ) 3 ( x y ) a ( v c x ) j ( x = y ) 如果对s 中的任何两个元素之间都可相互比较：( x y ) v ( y x ) ，这种关系就称为全 序关系。定义集合s 的一个子集t ，我们说x ( e s ) 是t 的一个上界，如果对任意的y t ， 满足y x 丽我们称x 为t 的最小上界，如果满足： 1 x 是t 的上界 2 对t 的任意上界y 有x y 。 类似地，我们可以定义集合t 的下界及最大下界。我们用符号上来表示集合s 的最小元， 如果对任意的x e s ，有上x 。而符号t 来表示集合的最大元，如果对任意的x s ，有x t 给定集合s 及偏序关系( t ，) 我们在s 专y 函数集合上定义关系： d d ，g = ，0 ) ，g ( x ) vx s 另外，如果( s 。) 是个偏序关系，则f ：s 专t 被称为单调的，如果 x 与yj ，( 曲，( y ) v x ，y s 我们用 s - t 来表示s 到t 的单调函数。 完备格是一个偏序关系，在这个关系中的任何子集中都包含有最小上界与晟大下界。也 就是说，任何完备格都有最大元和最小元，我们下面写出两个非常出名的完备格所满足的性 质，其他有趣的内容请大家参阅其他的参考书： 兰查塑翌查鲎堡主兰兰竺丝墨 旦堡塑堡量 任何有限元的全序集都是完备格。 如果s 是一个偏序关系而t 是一个完备格，那么 s t 是一个完备格。 一个完备格的简单例子是布尔集合 t r u e ，f a l s e ) ，偏序关系就定义为蕴含关系：最小上界 v 与最大下界a 就是逻辑中相应的的并与交运算。 格中的最小元为f a l s e ，而最大元为t r u e 。实际上，这是一个完备分配格，因为它满足 对任意的a ，b ，c 有： a a ( b vc ) = ( a a b ) v ( a ac ) a v ( b a c ) = ( a v b ) a ( a v c ) 实际上，这是一个布尔格，因为对每一个元素，其逆元存在。下文中将用b o o l 来表示 这种格。 2 2 谓词格 程序通常来说可以理解成是在一个状态空间中对其中的变量进行某种操作。通常，我们 用s t a t e 来表示那些所有可能的状态集合( 用等量关系来刻画偏序关系) 。从实际来讲，我 们还需要一些方式来刻画某些特殊的状态，例如一个程序的初始状态集合和一个程序的终止 时的状态集合。而这一切都可以用状态空间上定义的布尔函数来刻画。 由于s t a t e 组成一个偏序关系，雨b o o l 是一个完备格，因此 s t a t e - - ) b 0 0 1 仍然是一个 完备格。另外，由于s t a t e 是离散的，因此 s t a t e - - ) b 0 0 1 与s t a t e - ) b o o l 是等同的。我们把 它称为谓词格。谓词ab 的最小上界定义为a v b ( 逻辑或操作) ；而最大下界定义为口 6 ( 逻 辑与操作) 。 在谓词完备格中，最小元为f a l s e ，用来描述空的状态集合，而最大元为t r u e ，用来描 述所有可能的状态集合。这些操作可被定义如下： ( a vb ) = x a ( x ) v b ( x ) “ ( a a b ) = x a ( x ) a b ( x ) t r u e = x t r u e “ f a l s e = x f a l s e 这里我们用xx t 来表示一个l a m b d a 简化( 匿名函数) 。在上面的定义中，x 在s t a t e 中取值，而格中的序关系是指谓词中的蕴含关系。它可以定义如下： 附 a j b = vx a ( x ) 等b ( x ) 华东师范大学硕士毕业论文 可证编译器 2 3 谓词转换格 上面提到的谓词格理论为d i j k s t r a 对程序的定义提供了理论依据。d i j k s t r a 认为，程 序就是一种谓词转化( 一个从谓词到谓词的函数) ，通常符号w p ( p ，a ) = c 表示如果程序p 在初始状态满足它的最弱前置谓词c ，它将最终终止于一个状态，并且此状态满足后景谓词a 。 另外，从名称中我们也可以推测出，最弱前置谓词的意思是它可以晟大可能的使程序终止并 满足后置谓词a 。应当指出的是，这一点对应着h o a r e 逻辑中的完全正确性而非部分正确性。 这就是说程序执行后不但会满足谓词a ，而且必将终止。 谓词转换格( p r e d t r a n ) 是一个谓词格到另外一个的所有单调函数的集合 p r e d i c a t e - ) p r e d i c a t e 。我们用p ( a ) 表示( 它等价于d ij k s t r a 的w p ( p ，a ) ) 。 而谓词转换格中的序关系被定义为： d e f p c ：q= v a 。p ( a ) q ( a ) 很明显，p r e d t r a n 是一个完备格。因此，它的任何子集都有最小上界( u ) 与最大下界 ( n ) ( u ，n 在程序中称为不可决定性) 。其定义也显而易见： “ ( p u q ) = a p ( a ) v q ( a ) 彘f ( p e t q ) = a o p ( a ) q ( a ) 耐 t r u e = xa t r u e 村 f a l s e = a - f a l s e 我们通常的程序结构就可以看作是谓词转换格。作为例子，我们定义s k i p ( 谓词转换格 中的恒等变换) 赋值以及顺序语句： d 盯 s k i p = 8 a x ：= e= a o a x 卜e “ p ：q = a o p ( q ( a ) ) 这里，a e x l - - e 意味着在运算结果中把a 中出现的x 由e 来代替。 2 ，4 谓词转换格的性质 d i j k s t r a 已经提到，有5 条基本性质( 5 个健康条件) 用来刻画不同的程序语言。下面 列举如下： 华东师范大学硕士毕业论文 可证编译器 ( 我们用a ，b 来表示谓词而p 来表示程序) 1 ( f a l s e ) = f a l s e 2 如果a b 那么p ( a ) 等p ( b ) 3 p ( a ) p ( b ) ：p ( a a b ) 4 p ( a ) v p ( b ) = p ( a vb ) 5 p ( 3 i l i o * a i ) = 3 i ：i 0 ：p ( q ) 对所有的谓词序列a on 。满足只要对任意的i o 有q j 成立。 应该注意的是，谓词转换格产生的语言未必满足上述性质。例如，第四条性质仅仅满足 于可决定性的语言，对于非决定性的语言，试举反例如下： p = ( x ：= 2nx ：= 3 ) a = ( x = 2 ) b = ( x = 3 ) 则 p ( a ) = “胃词转换格中的n 定义) x ：= 2 ( x = 2 ) x ：= 3 ( x = 2 ) = f 赋值定义) t r u eaf a l s e = f a l s e 类似的，我们可以推导出p ( b ) = f a l s e 并且就有p ( a ) v p ( b ) = f a l s e 也非常容易验证 p ( a v b ) = t r u e 。由此可见，第4 条性质并非总被满足。而实际上，p ( a ) v p ( b ) p ( a v b ) 则总是有效的。 在p r e d t r a n 这个完备格中，对于规范定义是非常有益的，但是通常情况下它们是不能被 编译的。以上的性质中，只有单调性( i fa 专bt h e np ( a ) 专p ( b ) ) 是在p r e d r r a n 中总被满 足的。 华东师范大学硕士毕业论文 可证编译器 第三章精化理论演算 精化理论演算“”主要立足于解决以下两个问题： l ，对于给定的一个规范和程序，我们如何能够证明程序实现了规范? 2 ，我们怎样从一个规范出发，最终在保证正确的前提下得到计算机可以执行的程序”“? 而规范和程序都可以看作是一个更普遍概念中的特例，即看作是各个代理商( a g e n t ) 之间 的契约。这样，精化就可以看作是契约之间的一种关系，更准确地说，是格上的一种序关系。 而正确性则是指一种特别的精化( 即程序和规范之间的序关系) 。 虽然精化理论在本论文中起到举足轻重的作用，但是详尽的介绍精化理论则是另外几本 书。本文在此只对精化理论作一些概括性的介绍。 3 契约 让我们从最简单的概念开始介绍：契约。首先考虑一组代理，其中的每一个都具有改变 世界的能力。而这些代理们和他们伙伴之间相互作用的行为就被称为契约。 在继续讨论之前，我们对本章中将要用的符号做一点介绍。我们用带有前缀的圆点来表 示函数的应用。例如。f z 。而不是传统中的，( x ) ( 这样做的原因是因为在后面的讨论中要 用到复合函数的表示，而且在我们下面的讨论中，用s e t x 比用s e t ( x ) 要自然的多) 。我们 用a 斗君来表示所有的厂：a o b 的函数集合。而函数在这里可以是高阶的。也就是说，一 个函数的取值仍然可以是函数。例如：如果函数厂是a 哼( 嚣专c ) 中的函数，而a 是a 中的 一个元素，那么厂4 就是丑一c 中的函数。如果b 是b 中的一个元素，那么( 厂a ) j 5 就是c 中 的元素。因为函数的取值是左结合的，因此( 厂口) 6 可以简写为f a b 。 3 。1 1 状态空间及状态转化 我们假定世界是用一个状态( s t a t e ) 仃来描述。丽状态空间表示所有状态的集台。 一个代理通过函数，来改变当前的状态，从而得到一个新的状态厂矿。我们通常写成 来 代表状态9 , o 转变成为f 盯，而把这种改变称为更新行为。 这里，一个特殊的例子是指恒等变换。i d ：寸这个函数实际上并不改变状态空间。 即i d 莎= 盯。我们通常用s k i p f f i 来表示这种行为。 华东师范大学硕士毕业论文可证编译器 下面我们来讨论一个状态含有n 个属性：x i _ 。其中的每一个属性都可以被观察到并 且每一个都独立于其他的属性，这些属性就是我们平时所说的程序变量。而这个属性的取值 ( v a l u e ) ：v a l x 是一个取决于状态的函数，在状态空间中将属性x 赋值。通过观察变量，我 们可以得到关于状态空间的某些信息。对于每一个属性薯，我们用一个称为更新的函数s e t 一 来改变状态空间而使得属性耳得到一个新的值。s e t x a 盯表示一个新的状态，在这种状态下， 我们将值a 赋给x 而不改变其他属性的值。 状态改变在通常我们是用赋值来实现。例如，x ；= t + x ，描述了一个从状态盯到状态 s e t t n 盯的变化。而这里d = v a l x z t r + v a l x ，盯是代表状态盯中表达式t + x j 的值。 这种赋值的行为这里就写作： 。 3 1 2 契约 前文己经提过，契约用来规范代理的行为。一种规范是要求代理的行为必须按照某种顺 序进行，而这一点就被称为顺序执行行为：s ；曼i ；最，而其中的每一个s 都是代理所必需 执行的行为。对于任意的初始状态盯= c r o ，代理都必须产生一系列中间状态q ，而其中 的每一个状态q 都是由状态q 一。通过行为s 得到。 契约同样可以要求代理执行n 个行为当中的一个，这个可以表示成选择行为 s u u t 。而其中代理究竟选择哪一个则是随意的。也就是说，任何一个行为都可能被 选择，但是同时代理也必须要选择一个执行。 刚才提到的两种结构，再加上以前说过的基本行为，就给我们提供了一个非常简单的契 约的定义： s ：= i s ；s zj su 黾。 这种语言中的每一个状态都描述了代理的一个契约。我们在此把操作限制在二元操作范 围，实际上，多元操作可以由二元操作得到。在上面的语言中。顺序和选择都满足结合律： ( s ；& ) ；墨= s ；( 是；岛) 并且( s u 是) u s = s u ( 是u 马) 。根据习惯，我们假定分号的优 先级要高于u 。 我们也可以观察这种契约语言能否具有我们所期待的一些性质。例如，我们希望： s k i p ；s = s s = s ；s l a p 因为不改变状态的s k i p 行为也不应该改变顺序执行的其他契约。另外，在选择语句中， 顺序应该是可以任意交换的。因此： 华东师范大学项士毕业论文可证编译器 s u s = s s z t j s 2 = 岛u s 下面是一个契约的例子。 x ：= 1 ；( x ：= x + y u s k i p ) ；y ：= x 一1 在这个例子中，代理者首先要把x 的值变为l ，然后，它可以有两种选择，或者把属性x 和属性y 的值相加赋给x 或者什么都不做，最后，再将属性y 的值变为x 一1 。这里我们可以 得出：状态空间至少有两个属性x 和y ( 它可能还具有其他属性，但是那些属性的值均不发生 变化) 。如果代理能够按照刚才所说来完成行为，那么我们就称它满足了契约。 3 1 3 代理之间的合作 考虑到下面两个代理a 和b ，他们分别独立工作于同一个状态空间。每一个代理都有自己 的愿望并且独立的作出抉择。如果它们想要合作，它们就需要一个契约来规定各自的行为。 一个典型的例子是其中的一个代理( 我们称作a ) 的行为作为客户，而另外一个代理b ，则作 为提供服务者。假设a 的契约s 如下： s = x 0 ；( r ；x ：= x + l u s 幻p ) 而t 是另外一个代理b 的契约 t = ( y 车1 u y 2 ) ；x 竽x + y 在s 中契约t 的出现就意味着代理a 要求b 帮助其执行t 这个契约。当然，我们可以将 两个状态s 和t 合成一个契约来规定上面的代理行为。因为连接到一起的契约是被两个不同 的代理所执行，所以我们要区分做出选择的是a 还是b ，连接的契约描述如下： s = x _ o ；( ( y _ 1 u b y # 2 ) ；x ：= x + y ；x = = x + l u 。s 七扫) 与上面两个契约不同的地方只在于将t 用实际的行为代替并且区分做出选择的代理。至 于s k i p 和赋值语句，因为无论哪个代理来做，都不会不一样，因此我们没有必要加以区分。 3 1 4 断言 断言是指在一个给定的状态下代理所必须满足的要求。我们用 g ) 来表示个断言。例 如， x + y = 0 ) ，该断言表示在状态空间中属性x 与y 的值必须为0 。一个带有断言的契约表 示如下： s = x ：= 1 ；( x ：= 工+ y ； x 1 u x ：= x + z ) ；y i - x 一1 这里契约要求在选择第一个赋值语句执行以后，属性x 的值必须大于1 。如果在代理执 行的过程中断言确实被满足。那么在状态保持的情况下，代理继续向后执行。相反的，如果 断言没有被满足，那么代理将破坏整个契约。 华东师范大学硕士毕业论文可证编译器 分析上面的例子，我们可以看到，如果当y 0 时，而代理又选择第条语句的话，那么 代理将破坏契约。而事实上，即使y 1 】u 工：= 工+ z ) ；y ：= 工一l 这里代理认定在选择第一个赋值语句后属性x 的值必定大于l 。如果这不是事实，那么 代理会从契约中解放出来。另外，这个代理也有可能选择后面的赋值从而执行完契约。 最后一点，和前文中一样，当我们连接两个代理a 和b 是，也必须区分究竟是哪个代理 的假设。 华东师范大学硕士毕业论文 可证编译器 3 2 契约的运用 我们利用代理去完成一些事情。也就是说，建立一些新的，更符合愿望的状态。我们通 过给出一个它们必须满足的条件来刻画这种状态( 也就是后置谓词) 。如果一个代理不能完成 指定的任务，那么就有可能借助于其他的代理。 我们可以认为契约经常是在一个我们想要完成的代理和个对