結(jié)構(gòu)化程序的正確性證明

1、結(jié)構(gòu)化程序的正確性證明第1頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二本課的內(nèi)容1.重復(fù)遞歸引理2.正確性定理3.結(jié)構(gòu)化程序正確性證明的代數(shù)方法4.循環(huán)不變式產(chǎn)生的方法第2頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二結(jié)構(gòu)化程序正確性證明思路任何結(jié)構(gòu)化程序都可以用序列、條件和循環(huán)3種結(jié)構(gòu)表示，其中循環(huán)的正確性最為復(fù)雜，若能夠用序列和條件結(jié)構(gòu)來表示循環(huán)，則可以使正確性證明得以簡(jiǎn)化。第3頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二重復(fù)遞歸引理基本概念：基于程序函數(shù)的程序正確性概念。 假設(shè)已知一個(gè)程序P和一個(gè)預(yù)期函數(shù)f，若有f=P 則稱程序P正確地實(shí)現(xiàn)了函數(shù)f，或說

2、程序P是正確的。第二章中程序函數(shù)的定義第4頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二重復(fù)遞歸引理重復(fù)遞歸引理內(nèi)容引理1 while-do的正確性定理引理2 do-until的正確性定理引理3 do-while-do的正確性定理第5頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二重復(fù)遞歸引理引理1已知預(yù)期函數(shù)f和循環(huán)程序P while p do g 則f=P的充要條件是：對(duì)所有xD（f）， 程序P終止，且f=if p then g;f第6頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二重復(fù)遞歸引理引理1證明：必要性 f= P=while p do g = f=if

3、p then g;f P=while p do g=if p then g; while p do g =if p then g;f 充分性 f=if p then g;f = f= while p do g if p then g;f =if p then g;if p then g;f = if p then g;if p then g;(if p then g) = if p then g;if p then g;I = while p do g 第7頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二重復(fù)遞歸引理引理2和引理3引理2 已知函數(shù)f和循環(huán)程序P：do g until p

4、 ，則 f=P的充要條件是：對(duì)所有xD（f），程序P終止，且 f=g;if p then f 引理3 已知函數(shù)f和循環(huán)程序P：do1 g while p do2 h ,則 f=P的充要條件是：對(duì)所有xD（f），程序P終止，且 f=g;if p then h;f 重復(fù)遞歸引理告訴我們，循環(huán)程序的驗(yàn)證可以通過將循環(huán)化為遞歸的方法，將程序轉(zhuǎn)化為由選擇以及序列組成的無循環(huán)程序進(jìn)行驗(yàn)證！ 第8頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二正確性定理已知預(yù)期函數(shù)f和基本程序P，則f=P的充要條件是： xD(f)，程序P終止，且對(duì)于不同的基本程序，函數(shù)f分別滿足下列關(guān)系：情形a，對(duì)于序列，p=g;

5、h,有f=(x,y)|y=hg(x)情形b，對(duì)于if-then程序，if p then g，有 f=(x,y)|p(x) y=g(x) | p(x) y=x情形c，對(duì)于if-then-else，if p then g else h，有 f=(x,y)|p(x) y=g(x)| p(x) y=h(x)情形d，對(duì)while-do程序，while p do g，有 f=(x,y)|p(x) y=fg(x)| p(x) y=x情形e，對(duì)于do-until程序，do g until p od,有 f=(x,y)|pg(x) y=g(x)| pg(x) y=fg(x)情形f，對(duì)于do-while-do程序

6、，do1 g while p do2 h od，有 f=(x,y)|pg(x) y= fhg(x)| pg(x) y=g(x)第9頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二正確性定理證明情形a,b,c由程序函數(shù)直接可得情形d,由下式可得（根據(jù)引理1）： 對(duì)while-do程序,while p do g ，有 while p do g = if p then g;f = (x,y)|p(x) y=f g(x)| p(x) y=x = f 情形e,f由引理2，3可證第10頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二結(jié)構(gòu)化程序正確性證明的代數(shù)方法給定一個(gè)程序P的預(yù)期程序函數(shù)

7、f，若xD（f），程序P是終止的，且通過正確性定理求解程序P的程序函數(shù)f，若與預(yù)期函數(shù)f相等，則得證。證明步驟： 1：程序P是終止的； 2：f和程序P的定義域相同； 3：通過正確性定理求解程序P的程序函數(shù)f，與預(yù)期函數(shù)f相等。對(duì)于相對(duì)簡(jiǎn)單直觀的程序，可以直接使用代數(shù)方法計(jì)算程序函數(shù)。對(duì)于復(fù)雜的序列和條件程序、循環(huán)程序的證明，可以采取跟蹤表方法求解程序函數(shù)。第11頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二代數(shù)方法跟蹤表1.已知程序P：x:=x+y;y:=x-y;x:=x-y;求它的程序函數(shù)。 假設(shè)變量x,y的初值是x0,y0 ，執(zhí)行第一個(gè)賦值語句后變量值為x1,y1 ，則可以建立賦

8、值表如下：語句xy1x:=x+yx1=x0+y0y1=y02y:=x-yx2=x1y2=x1-y13x:=x-yx3=x2-y2y3=y2分析跟蹤表可知：x3=x2-y2=x1-(x1-y1)=y1=y0 y3=y2=x1- y1=x0+y0-y0=x0通過跟蹤表法，可知程序P的程序函數(shù)為(x,y),(y,x)第12頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二代數(shù)方法跟蹤表2.序列程序 y:=a y:=x*y+by:=x*y+cy:= x*y+d跟蹤表為：語句xy1y:=ax1=x0y1=a2y:=x*y+bx2=x1y2:=x1*y1+b3y:=x*y+cx3=x2y3:=x2*

9、y2+c4y:= x*y+dx4=x3y4:=x3*y3+d第13頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二代數(shù)方法跟蹤表所以，x4=x3= x2=x1=x0 y4= x3*y3+d =x2*(x2*y2+c)+d = x1*(x1*(x1*y1+b)+c)+d = x0*(x0*(x0*a+b)+c)+d相應(yīng)的程序函數(shù)為：(x,y=x, x*(x*(x*a+b)+c)+d)即y=ax3+bx2+cx+d第14頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二分離規(guī)則條件語句 if p then g else h 可用條件規(guī)則表示出來 (pg | ph)。為了證明條件語句的

10、正確性，就需要比較預(yù)期函數(shù)f和條件規(guī)則是否相等。第15頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二復(fù)合條件規(guī)則的化簡(jiǎn) (p1 (q11 r11 | q12 r12 ) | p2 (q21 r21 | q22 r22 ) )(p1 q11) r11 | (p1 q12) r12 | (p2 q21) r21 | (p2 q22) r22p1,p2是分離的，即p1 p2為假。如果一個(gè)條件規(guī)則的所有謂詞都是分離的，稱它為分離規(guī)則。第16頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二將條件規(guī)則化為分離規(guī)則在化簡(jiǎn)和比較條件規(guī)則時(shí)，分離規(guī)則比一般的條件規(guī)則使用更方便一些。一般的復(fù)合規(guī)

11、則不一定能展開，但分離的復(fù)合規(guī)則總可以展開。一般的條件規(guī)則的前后順序是不能交換的，而分離規(guī)則的順序是可以交換的。討論程序的正確性時(shí)，總是首先將條件規(guī)則化為分離規(guī)則。第17頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二將條件規(guī)則化為分離規(guī)則對(duì)于任意的條件規(guī)則（p1 r1 | p2 r2 | p3 r3 | ）化為分離規(guī)則（p1r1 |p1p2r2|p1p2p3r3 | ）第18頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二條件語句的正確性證明假設(shè)某一條語句的程序函數(shù)是分離規(guī)則： （p1r1|p2r2|p3r3） 預(yù)期函數(shù)是f，由于f可以是賦值的形式，例如y:=f(x)的形式給

12、出時(shí)，為了證明條件語句的正確性，需證明以下兩點(diǎn)：(1) f(x)的定義域和分離規(guī)則式的定義域是相同的；(2) 利用分離規(guī)則的謂詞將f(x)的定義域分解，并有以下關(guān)系成立：p1(x)r1(x)=f(x)p2(x)r2(x)=f(x)p3(x)r3(x)=f(x)第19頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二條件語句的正確性證明另外，當(dāng)f是以條件規(guī)則的形式給出時(shí)，例如，是下列的分離規(guī)則 (q1 s1 | q2 s2 )這時(shí)，要證明它和分離規(guī)則式相同，需要證明：(1)兩個(gè)分離規(guī)則的定義域是相同的，即p1(x)Vp2(x)Vp3(x) = q1(x)V q2(x)(2) 兩個(gè)分離規(guī)則中

13、的謂詞成對(duì)合取后，相應(yīng)的結(jié)果是相同的：p1(x) q1 (x) r1(x) = s1 (x)p1(x) q2 (x) r1(x) = s2(x)p3(x) q1 (x) r3 (x) = s1 (x)p3(x) q2 (x) r3 (x) = s2(x)第20頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二例子1預(yù)期函數(shù) f=(x:=-x)程序P為 if x0 then x:=x-2*x else x:=x+2*abs(x)P=(x0 x:=x-2*x| x0 x:=x+2*abs(x)證明(1) f和P的定義域均為整數(shù)，相同。(2) P是一個(gè)分離規(guī)則，且x0 (x:=x-2*x) =

14、 (x:=-x)x0 (x:=x+2*abs(x)=(x:=x+2*(-x)=(x:=-x)得證第21頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二例子2 已知預(yù)期函數(shù)f是（x,y,a是整數(shù)，且x0） (x,y,a),(0,a*x+y,a) 程序P如下，其中x0： while x0 do x,y=x-1,y+a 證明程序P是正確的，即f=P 證明1：程序是終止的 證明2：定義域相同 證明3：f=(x,y)|p(x) y=fg(x) | p(x) y=x，其中，p(x)=(x0), p(x)=(x=0) 利用fg(x)的跟蹤表證明3第22頁，共30頁，2022年，5月20日，19點(diǎn)8分

15、，星期二例子2于是有： x2 =0 y2=a0*(x0-1)+y0+a0=a0* x0 +y0即當(dāng)x0時(shí) x,y,a :=0,a*x+y,a; 當(dāng)x=0時(shí) x,y,a :=0,y,a = 0,a*0+y,a因此可知，f (x,y,a),(0,a*x+y,a)，與預(yù)期函數(shù)相等，因此得證。語句xyx,y:=x-1,y+ax1 =x0-1y1 =y0+a0 x,y,a:=0,a*x+y,ax2 =0y2=a0* x1 + y1第23頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二循環(huán)不變式產(chǎn)生的方法 對(duì)于程序部分正確性證明的不變式斷言法，這一方法的關(guān)鍵是建立一個(gè)正確的不變式斷言，對(duì)一般程序來

16、說，不變式斷言的建立主要依靠程序員對(duì)程序的理解，尚無系統(tǒng)的方法。 但對(duì)結(jié)構(gòu)化程序來說，如果已知它的程序函數(shù)，則可以根據(jù)不變式狀態(tài)定理，來確定它的一個(gè)循環(huán)不變式。第24頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二循環(huán)不變式產(chǎn)生的方法不變式狀態(tài)定理：假設(shè)f=while p(x) do g(x) ， x0是初始值，則 循環(huán)不變式q(x)為：f(x) = f(x0)證明：1.在進(jìn)入循環(huán)時(shí)， f(x0) = f(x0)，因此q(x)成立。2.試證假設(shè)在每一次進(jìn)入循環(huán)前q(x) 成立，即f(x) = f(x0) ，則執(zhí)行循環(huán)后q(x)也成立，即證明 p(x)q(x) = qg(x)由p(x)為

17、真，及正確性定理 f=(x,y)|p(x)y=fg(x)|p(x)y=x可知 即 p(x) = (f(x)=fg(x)第25頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二循環(huán)不變式產(chǎn)生的方法又進(jìn)入循環(huán)前q(x) 成立，即q(x)=(f(x0)=f(x) p(x)q(x) = (f(x0)= fg(x)而(f(x0)= fg(x) (f g(x)=f(x0) (f(g(x) =f(x0) q(g(x) (歸納假設(shè)q(x)=(f(x)=f(x0) qg(x)p(x)q(x) = qg(x)第26頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二循環(huán)不變式產(chǎn)生的方法同理可知如下定理：

18、2 假設(shè) f(x)=do g(x) until p(x) ，則該循環(huán)不變式q(x)為 f(x)=fg(x0)3假設(shè) f(x)=do1 g(x) while p(x) do2 h(x) ，則該循環(huán)不變式q(x)為 f(x)=fhg(x0)第27頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二循環(huán)不變式產(chǎn)生的方法例1對(duì)于循環(huán)程序P：while v0 do u,v=u+1,v-1 ，其程序函數(shù)為(u,v),(u+v,0)，求其循環(huán)不變式。（設(shè)u、v0）對(duì)循環(huán)中所有變量，分別計(jì)算f(x)和f(x0)，列表如下：則循環(huán)不變式為f(x)=f(x0) = u+v= u0+v0 xf(x)f(x0)uu+vu0+v0 v00第28頁，共30頁，2022年，5月20日，19點(diǎn)8分，星期二循環(huán)不變式產(chǎn)生的方法例2求程序P： while ab do a,q:=a-b,q+1 的循環(huán)不變式該程序的程序函數(shù)為(a,b,q),(a-a/b*b,b