6程序的正确性

1、6. 程序的正确性前面介绍了两种语义学， 即操作语义学和指称语义学。 操作语义学方 法的特点是， 从程序的操作角度来说明语言的语义， 可以称它是个抽 象机的方法；指称语义方法的特点是，从语法单位的功能即“给什么 出来什么”的角度来说明语言的语义，可以称它是个函数化的方法； 公理语义方法的特点是从变量间的逻辑关系来说明语言的语义， 可以 称它是个逻辑化的方法。R. W. Floyd发表了给程序赋予意义一文，提出了一种描述程序意 义的逻辑方法，称此方法为 Floyd 归纳断言法。该方法的研究对象是 框图程序。 Floyd 第一个揭示了程序与逻辑的关系，从而打开了逻辑 地研究程序性质的大门。其中最为

2、重要的是所谓的循环不变式的问 题，对此 Z. Manna 做了非常深入的研究并发表了很多有价值的论文。后来，C. A. R. Hoare发表了计算机程序设计的公理基础一文，第 一次用公理系统定义了程序设计语言的语义。 最有代表性的公理语义 系统是由Hoare和Wirth合作完成的Pascal语言的公理语义。我们知道， 即使一个程序的句法是完全正确的， 它也可能不按它的预 期行为做事。如何证明程序达到某种预期目的呢？这就是 “程序验证” 的任务 一种普通的程序验证的方法就是程序测试(program testing),就是让程 序在关键性的输入数据上运行， 这种方法只能使人更加相信程序是正 确的，

3、但无法保证程序没有语义错误， 因为成功地通过一个子集的测 试仅仅是验证程序正确的必要条件而不是充分条件。另一种方法就是程序证明(program verification)。公理化方法的优点就是能用来证明程序的正确性。 它的主要思想是对给定语言构造相应的 公理系统。这个公理系统与传统的公理系统有所不同，从形式上说， 区别在于它使用了如下形式的公式：P S Q其中 S 是语句， P 和 Q 是逻辑公式。我们称 P 是前置条件 (Precondition),称 Q为后置条件(Postcondition)，统称上述公式为验 证公式。 P、S 和 Q 中都包含一些程序变量,而 P 和 Q 是这些变量所

4、应该满足的关系式。显然, 一个验证公式成立与否,要依赖于程序变 量的状态。如果任何时候验证公式都成立,则称验证公式恒成立,并 记为? P S Q上述验证公式成立的大致意思是：“如果执行S前前置条件p成立并 且S的执行终止，则能推出执行 S后后置条件Q成立”例如：验证 公式 x 0x:=x+2x10,在状态 =8/x 下,执行语句 x:=x+2之前成立,同时该语句终止,并且执行语句 x:=x+2 后后置条件 x 10成立。 但不难证明在状态 =5/x 下,尽管前置条件和语句的终止 性都成立，但执行语句后其后置条件并不成立。 故上述验证公式不是 恒成立。假设有一程序S,计算一 X值并把它放到变量y

5、中，其入口条件是x0。如果能证明？x0Sy= x，则也就证明了程序 S是正确的，即反应了程序员的意图，因此不需要用测试数据去一一测试。 但需要 注意的是程序正确的最基本条件是程序要终止，这是需要证明的对 象，而不能由我们自己来假设，但前面的验证公式把该程序终止性作 为已知条件使用了，因此，上述证明是不完全的，故称上述证明为部 分正确性的证明。6.1程序正确性的详细说明程序验证就是要证明满足某设定的规范(specification)。规范是系统所 要满足的需求的体现，它是以实现者易于理解的方式，表达所期望的 行为的一种精确而形式的陈述。下面是一些非形式化的规范：(1) 对于所有输入值a, b N

6、at,满足a, b>0，程序计算的是a和b 的最大公约数gcd(a, b)。(2) 对于所有输入值a, bNat，满足a, b>0，程序终止，输出值 是 gcd(a, b)。对于一计算最大公约数的递归程序 S,规范可写成：(2a, b Nat，若 a, b>o，贝S M(S)(a, b)有定义且M(S)(a, b)=gcd(a, b)。 显然规范( 2)等价于下面两个规范：(3) 对于所有输入值a, b Nat,满足a, b>o。若程序终止，则它终止的输出值是gcd(a, b)。和(4) 对于所有输入值a, b Nat，满足a, b>o，程序终止。对于递归程序S的

7、规范(2，与它等价的规范：(3a, bNat，若 a, b>o 且 M(S)(a, b)有定义，则M(S)(a, b)=gcd(a, b)。和(4a, bNat，若 a, b>0 则 M(S)(a, b)有定义。规范( 3)或( 3( 4)或( 4程序是否终止。这两种规范合起来就构成完全正确性的规范。定义 6.1 (有关谓词的正确性)令B是谓词逻辑的基，I是该基的一种解释。是相应的状态集合。令S 一 LiB是中的框图程序或L2B中的while-程序。M|(S)是程序的含 义。进一步令 :Bool 和 :Bool 是两个谓词，分别称为前置条件(precondition)和后置条件(p

8、ostcondition)。称程序S,( 1) 在解释 I 下，有关谓词(partially correctw. r. t predicates and )，如果对于所有状态，若 ( )=true 且 MI(S)( )(MI(S)( )=true。(2) 在解释I下，有关谓词终止(terminate)，如果对于所有状态，若 ( )=true 则 MI(S)( )有定义。(3) 在解释I下，有关谓词和 是完全正确的(totally correct)，如果对于所有状态，若（）=true 则 Mi（s）（）有定义且（Mi（S）（）二true定义6.2 （有关公式的正确性）令B, I和S如定义6.1所

9、述，p, q WFFb是两个公式，称程序S,在 解释|下，有关公式p和q是部分正确的，如果它关于谓词|（p）和|（q） 是部分正确的，类似可定义有关公式的完全正确性和终止性。例6.3（a）计算整数平方根的程序（例 3.2），它的完全正确性规范可陈述为：程序有关前置条件true和后置条件y/ xx<（yi+1）2是完全正确的。（b）令S是一计算最大公约数的框图程序或循环程序。规范（2）可重述为：程序有关前置条件 x=a y=b a>0b>0和后置条件x=gcd（a, b）是完全正确的。（c）某框图程序或循环程序关于前置条件true和后置条件false是部 分正确的 肝它的含义函

10、数处处没定义（everywhere undefined。（d） 某框图程序或循环程序关于前置条件true终止肝它的含义函数 是一个全函数（即处处有定义）。1. 注意某些规范，比如“一个程序关于true和true是部分正确的”， 根本没有什么意义，因为每个程序的终止状态都满足后置条件 true,使其为真。类似的例子见 ex6.1-1。2. 使P S Q成立的前置条件和后置条件可能有无穷多个，例如使px:=x+1x2成立的p有无穷多个，如x 1, x 2, x3,。其中最弱的条件是 x 1，这表示“要使 x 2 成立，执行前 S 起码要求 x 1 成立”。定义 6.4 (最弱前置条件和最强后置条件

11、， Weakest Precondition and Strongest Postcondition)(1) 令B, I, S和 如定义6.1所述。程序S和谓词 的最弱的自由 前置条件，记为wlp(S,)，定义为谓词： Bool，它满足( )=true iff MI(S)( )没有定义或者 MI(S)( )有定义且 (MI(S)( )=true。(2) 程序S和谓词 的最弱前置条件，记为wp(S,)，定义为谓词:Bool，它满足( )=true iff MI(S)( )有定义且 (MI (S) ( )=true 。(3) 程序S和谓词 的最强后置条件，记为sp( , S),定义为谓词:Bool

12、，它满足( )=true iff 存在一状态，使得 ( )=true 且MI(S)()= 。RMK.(1) (条件强弱的含义)设p, q是谓词，且有p q,则称p强于q, 称 q 弱于 p。 (2) wlp(S, )的定义中并不要求程序终止,所以它与“部分正确” 呼应； wp(S, )与“完全正确”呼应。下面的定理进一步说明了“最弱”和“最强”的含义。定理 6.5 令 B, I, S 和 如定义 6.1 或 6.4 所述。(1) 令 是S和 的最弱自由前置条件，那么(a)S关于 和 是部分正确的；和(b)对于谓词，若满足S关于 和 是部分正确 的，则对于所有状态，( )( )。(2) 对于“最

13、弱前置条件”和“完全正确”也有类似( 1)的结论。( 3) 令 是 和 S 的最强后置条件，那么 (a)S 关于 和 是部分正 确的，(b)对于谓词，若它满足S关于 和 是部分正确的， 则对于所有状态，( )( )。RMK.最强的条件(断言)是false ，而最弱的条件是true。条件true 是什么也没给出，而 false 则相当于无穷多个条件，以至于不 可满足。定理 (求最弱 (自由 )前置条件)(1) wlp(x:=e, q)=q xe(2) wlp(s1; s2, q)= wlp(s1, wlp(s2, q)(3) wlp(if(e, s1, s2), q)=(ewlp(s1, q)

14、( e wlp(s2, q)RMK. 注意这里并没有给出循环语句的最弱 (自由)前置条件的求法， 其原因是在用Hoare公理系统证明程序时，并不用最弱条件，而是用 循环不变式。定理 (求最强后置后件)1) sp(p, s1; s2)= sp(sp(p, s1), s2)(2)sp(p, x:=e)=x.(pxxxx=ex )(3) sp(p, if(e, s1, s2)= sp(pe, s1) sp(p e, s2)RMK. 以上介绍了求最弱前置条件( WP 方法)和最强后置条件的方法(SP方法)。在证明程序正确性时要用到它们。程序的入口处有输 入谓词p，就可以利用SP方法，往下求别的点上的断

15、言。同理，利 用程序出口处的谓词q,可以往上求别的点上的断言。有了上述定理 后，要证明pSq，只需求wp(S, q)，并证明p强于wp(S, q);或者 求sp(p, S),并证明q强于sp(p, S)即可。因为公理系统有推论规则， 可以得到最终结论。引理：令(li,1)(In,n)是例3.2的一个计算序列，满足n1, ln=test。那么有n(x)= 1(x)( n(y1)2n(x)n(y2)=2n(y1)+12n(y3)=(n(y1)+1)2证明：(归纳基础)因n=1, ln=li二begin。于是li=test，这是不可能的。所以命题无 意义而为真。(归纳步) 假设对于 j=1, , n

16、 命题成立。往证对于 n+1 ，命题也成立。假设ln+1二test。根据ln的值，可分成两种情况:(1) In二begin。因此 n=1, n+i(x)二n(x)=i(x),n+i(yi)=O,n+1(y2)=1,n+1(y3)=1 。容易验证结论成立。(2) ln=upd。那么n+1=ny 3/I(y2+y3)(n)进一步 ln-1=loop,n-1 y1/I(y1+1)(n-1)y2/I(y2+2)(n-1)(1)(2)In-2=test,有，(3)(4)n-1n+1(x)=n+1(y1)=n+1(y2)=n+1(y3)=n-2, 且 I(y3n(y1)=n(y2)=x)(n-2)=truen(x)=n-1(x)=n-2(x)n-1(y1)+1=n-1(y2)+2=n-2(y1)+1n-2 (y2)+2n(y2)+n(y3)n-2(y3)于是n+1(x)=n-2(x)=1(x)(n+1(y1)2=(n-2(y1)+1)2根据