第四部分 弱谓词变换方法 2010

程序设计形式语义学南京理工大学计算机系张琨二○○四年八月二日南京理工大学计算机系2010.11主讲：张琨2.5程序正确性证明－Dijkstra的弱谓词变换方法及强验证方法Dijkstra于1967年提出了弱谓词变换方法，该方法采用的是反向推理，即从Q出发，S执行之后它的前置条件至少应该含有的条件。这种前置条件，称为最弱前置条件，也就是在S执行之后，Q成立时，前置条件应该附加的最小限制。这种方法称为弱谓词变换法。2.5程序正确性证明－Dijkstra的弱谓词变换方法及强验证方法定义2.9关于Q的最弱前置条件，记为WP(S,Q)它是一个满足最弱限制的语句，为了使S成功地终止，且S执行完后Q为真，此语句必须为真。程序证明转化为执行下面两个计算步骤：找出WP(S,Q)证明P⊃WP(S,Q)分析前面的例子：k≠0{y:=x/k}x=y*k2.5计算WP：语言的语义首先讨论语句的功能描述，即语句的语义说明，然后分别讨论各语句的最弱前置条件的计算。为讨论一般语句的WP(S,Q)的计算，首先定义一个标准记号R(x)。定义2.9：假定R是一谓词或一程序片段，记号R(X)表明R可以包含（在程序片段的情况下，可以修改）X中的变量，同样R(Z)解释为在整个R中，用Z中的表达式置换X对应的变量所得的结果。2.5计算WP：语言的语义1.空语句空语句什么也不做，所以，空语句之前的条件在空语句之后当然成立，因此，有：WP(SKIP,Q)≡Q其中，SKIP表示空语句2.5计算WP：语言的语义2.语句序列假定有语句序列S1;S2。如果在S1、S2执行后，其后置条件Q为真，Q自然也是S2的后置条件，对于S2，则有WP(S2,Q)。由于S1在S2之前，这意味着WP(S2,Q)是S1的后置条件，且在S1终止执行之后为真，于是，对于S1的最弱前置条件应该是WP(S1,WP(S2,Q))，因此，有公式：WP(S1;S2,Q)≡WP(S1,WP(S2,Q))WP(S1;S2;…;Sk,Q)≡WP(S1,WP(S2,…,WP(Sk,Q)…))2.5计算WP：语言的语义3.IF语句IFCTHENS1ELSES2的WP为：WP(IFCTHENS1ELSES2,Q)≡(CWP(S1,Q))∧(～CWP(S2,Q))IFCTHENS的WP为：WP(IFCTHENSELSESKIP,Q)≡(CWP(S,Q))∧(～CWP(SKIP,Q))≡(CWP(S,Q))∧(～CQ)2.5计算WP：语言的语义4.赋值语句x:=E的最弱前置条件是：WP(x:=E,Q(x))≡Q(E)Q(E)是Q(x)用E置换x而得。例1，若有{x:=y+3}x0WP(x:=y+3,x0)≡y+30例2，若有{x:=x+1}x≤n+1WP(x:=x+1,x≤n+1)≡x+1≤n+1但是，一般而言，总是假定E是有定义的，则正确的表示应该是：WP(x:=E,Q(x))≡E有定义∧Q(E)举例WP(S1;S2;…;Sk,Q)≡WP(S1,WP(S2,…,WP(Sk,Q)…))已知序列程序S如下，求WP(S,Q)x:=x+y;y:=x-y;x:=x-y,Q为x=b∧y=aWP(S,Q)≡WP(x:=x+y;y:=x-y;x:=x-y,x=b∧y=a)≡WP(x:=x+y;y:=x-y,WP(x:=x-y,x=b∧y=a))≡WP(x:=x+y;y:=x-y,x-y=b∧y=a)≡WP(x:=x+y,WP(y:=x-y,x-y=b∧y=a))≡WP(x:=x+y,x-(x-y)=b∧x-y=a)≡WP(x:=x+y,y=b∧x-y=a)≡y=b∧(x+y)-y=a≡y=b∧x=a2.5计算WP：语言的语义证明举例1.假定x是一个整型变量，证明x≠0{IFx0THENx:=-xELSEx:=x-1}x≥02.假定x是一个整型变量，证明xn∧P=2x{x:=x+1;P:=P*2}x≤n∧P=2x1.假定x是一个整型变量，证明x≠0{IFx0THENx:=-xELSEx:=x-1}x≥0(1)构造WPWP(IFx0THENx:=-xELSEx:=x-1,x≥0)≡(x0)⊃WP(x:=-x,x≥0)∧(x≥0)⊃WP(x:=x-1,x≥0)≡(x0⊃-x≥0)∧(x≥0⊃x-1≥0)≡TRUE∧(x≥0⊃x≥1)≡x≠0(2)证明x≠0⊃WP(IFx0THENx:=-xELSEx:=x-1,x≥0)正确，此时化为证明x≠0⊃x≠0⊃显然正确。2.假定x是一个整型变量，证明xn∧P=2x{x:=x+1;P:=P*2}x≤n∧P=2x(1)构造WPWP(x:=x+1;P:=P*2,x≤n∧P=2x)≡WP(x:=x+1,WP(P:=P*2,x≤n∧P=2x))≡WP(x:=x+1,x≤n∧P*2=2x)≡x+1≤n∧P*2=2x+1(2)证明xn∧P=2x⊃x+1≤n∧P*2=2x+1这显然是正确的。练习1.WP(x:=2*x;IFx1THENx:=x+2,x5),x是整数2.当断言Q为y=10时，计算WP(x:=2*y;y:=x–4,Q)。2.5计算WP：语言的语义5.嵌入断言为了使程序易于理解，往往在程序的某些语句之间插入注解，用以指明什么应该为真，这种注释也有助于简化一个证明。如在语句S1，S2之间，插入注解ASSERTR，其功能描述语句表示为P{S1;ASSERTR;S2}A如果证明这个语句是有效的，则足以证明：P{S1}R,R{S2}Q由于Q是S2的后置条件，则它在S2执行后为真，也应该在S2执行之前为真，于是Q成了R的后置条件，于是有WP(ASSERTR,Q)≡R∧Q如果能证明RQ，则上式可简化为WP(ASSERTR,Q)≡R2.5计算WP：语言的语义6.WHILE语句WHILE语句的循环条件虽然是事先设置的，但由于其循环次数可能是不确定的，可能导致出现循环不终止的情形。因此WHILE语句可能展开成一个任意常的语句序列，以致于它的最弱前置条件可能是无穷的。为避免这种情况，最有效的办法是找出WHILE语句最弱前置条件的一般项公式，使无限公式转变成有限情况的计算。2.5计算WP：语言的语义6.WHILE语句分析WHILE语句循环终止时谓词的结构，WHILE语句为WHILEBDOS该语句后的谓词为Q。分析其循环终止情况为：1.S执行零次，则循环开始B不为真，跳过WHILE语句后，应该有～B∧Q为真。2.S执行一次，则B开始为真，执行一次S后，又有～B∧Q为真，使循环终止。3.S执行两次，则B开始为真，执行一次S之后，B仍为真（B就成了第一个S的后置条件），执行第二次S，又有～B∧Q为真，使循环终止。2.5计算WP：语言的语义6.WHILE语句WHILE语句的最弱前置条件的表达式为：WP(WHILEBDOS,Q)≡H0∨H1∨H2∨…其中：H0=～B∧Q;Hi=B∧WP(S,Hi-1),i02.5计算WP：语言的语义举例说明：F是计算xn的循环的程序片段WHILEi≤nDOBEGINt:=t*x;i:=i+1END其后置谓词Q(t,i)，计算其WP(F,Q(t,i))2.5计算WP：语言的语义WP(F,Q(t,i))≡in∧Q(t,i)∨i≤n∧WP(t:=t*x;i:=i+1,in∧Q(t,i))∨i≤n∧WP(t:t*x;i:=i+1,i≤n∧WP(t:=t*x;i:=i+1,in∧Q(t,i)))∨…≡in∧Q(t,i)∨i≤n∧i+1n∧Q(t*x,i+1))∨i≤n∧i+1≤n∧i+2n∧Q(t*x2,i+2)))∨…≡in∧Q(t,i)∨i=n∧Q(t*x,i+1)∨i+1=n∧Q(t*x2,i+2)∨…≡Q(t*xj,i+j)对于使得i+jn的最小整数j≥0。即求最小整数j≥0，使得i+jn，循环终止。最弱前置条件小结证明P{S}Q分为以下两步：计算WP(S,Q)证明PWP(S,Q)列举各语句的最弱前置条件的计算公式：WP(SKIP,Q)≡QWP(S1;S2,Q)≡WP(S1,WP(S2,Q))WP(IFCTHENS1ELSES2,Q)≡(CWP(S1,Q))∧(～CWP(S2,Q))WP(IFCTHENSELSESKIP,Q)≡(CWP(S,Q))∧(～CQ)WP(ASSERTR,Q)≡R∧QWP(WHILEBDOS,Q)≡H0∨H1∨H2∨…H0=～B∧Q;H1=B∧WP(S,Hi-1),i0程序的正确性证明小结本节讨论了程序的表示与形式化证明。用SMALL语言表示程序中的控制与数据，表明不论使用哪种语言，尽管它们所表述的程序结构不同，但都等价于SMALL的语言表示。在程序证明部分，引入了程序部分正确性、终止性、完全正确性及最弱前置条件WP等多种程序正确性证明方法。程序的正确性证明小结通过上述程序正确性形式化证明方法的讨论，可得到如下启示：程序能像证明数学定义一样，证明其正确性；程序正确性证明方法提供了程序语义的形式化描述，不仅可用此证明程序的正确性，还为程序的形式推导奠定了理论基础。程序正确性证明的困难源于中间断言与验证条件的设置，其自动证明系统远远超过被证明的程序本身。因此，只有最重要的核心程序才考虑采用证明的方法，大量的软件系统，特别是大型软件系统通常靠测试方法验证其正确性与实用性。Dijkstra指出“测试只能证明程序有错，不能保证程序无错”。