




版權(quán)說(shuō)明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權(quán),請(qǐng)進(jìn)行舉報(bào)或認(rèn)領(lǐng)
文檔簡(jiǎn)介
1、第6章 結(jié)構(gòu)化程序的正確性證明,本課的內(nèi)容,1.重復(fù)遞歸引理 2.正確性定理 3.結(jié)構(gòu)化程序正確性證明的代數(shù)方法 4.循環(huán)不變式產(chǎn)生的方法,結(jié)構(gòu)化程序正確性證明思路,任何結(jié)構(gòu)化程序都可以用序列、條件和循環(huán)3種結(jié)構(gòu)表示,其中循環(huán)的正確性最為復(fù)雜,若能夠用序列和條件結(jié)構(gòu)來(lái)表示循環(huán),則可以使正確性證明得以簡(jiǎn)化。,重復(fù)遞歸引理,基本概念:基于程序函數(shù)的程序正確性概念。 假設(shè)已知一個(gè)程序P和一個(gè)預(yù)期函數(shù)f,若有 f=P 則稱程序P正確地實(shí)現(xiàn)了函數(shù)f,或說(shuō)程序P是正確的。,第二章中程序函數(shù)的定義,重復(fù)遞歸引理,重復(fù)遞歸引理內(nèi)容 引理1 while-do的正確性定理 引理2 do-until的正確性定理 引
2、理3 do-while-do的正確性定理,重復(fù)遞歸引理引理1,已知預(yù)期函數(shù)f和循環(huán)程序P while p do g 則f=P的充要條件是:對(duì)所有xD(f), 程序P終止,且f=if p then g;f,重復(fù)遞歸引理引理1,證明: 必要性 f= P=while p do g = f=if 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 th
3、en g;if p then g;(if p then g) = if p then g;if p then g;I = while p do g ,重復(fù)遞歸引理引理2和引理3,引理2 已知函數(shù)f和循環(huán)程序P:do g until p ,則 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)證可以通過(guò)將循環(huán)化為遞歸的方法,將程序轉(zhuǎn)化為由選擇以及序列組成的無(wú)循
4、環(huán)程序進(jìn)行驗(yàn)證!,正確性定理,已知預(yù)期函數(shù)f和基本程序P,則f=P的充要條件是: xD(f),程序P終止,且對(duì)于不同的基本程序,函數(shù)f分別滿足下列關(guān)系: 情形a,對(duì)于序列,p=g;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)
5、 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程序,do1 g while p do2 h od,有 f=(x,y)|pg(x) y= fhg(x)| pg(x) y=g(x),正確性定理證明,情形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
6、由引理2,3可證,結(jié)構(gòu)化程序正確性證明的代數(shù)方法,給定一個(gè)程序P的預(yù)期程序函數(shù)f,若xD(f),程序P是終止的,且通過(guò)正確性定理求解程序P的程序函數(shù)f,若與預(yù)期函數(shù)f相等,則得證。 證明步驟: 1:程序P是終止的; 2:f和程序P的定義域相同; 3:通過(guò)正確性定理求解程序P的程序函數(shù)f,與預(yù)期函數(shù)f相等。 對(duì)于相對(duì)簡(jiǎn)單直觀的程序,可以直接使用代數(shù)方法計(jì)算程序函數(shù)。 對(duì)于復(fù)雜的序列和條件程序、循環(huán)程序的證明,可以采取跟蹤表方法求解程序函數(shù)。,代數(shù)方法跟蹤表,1.已知程序P:x:=x+y;y:=x-y;x:=x-y;求它的程序函數(shù)。 假設(shè)變量x,y的初值是x0,y0 ,執(zhí)行第一個(gè)賦值語(yǔ)句后變量值為
7、x1,y1 ,則可以建立賦值表如下:,分析跟蹤表可知: x3=x2-y2=x1-(x1-y1)=y1=y0 y3=y2=x1- y1=x0+y0-y0=x0 通過(guò)跟蹤表法,可知程序P的程序函數(shù)為(x,y),(y,x),代數(shù)方法跟蹤表,2.序列程序 y:=a y:=x*y+b y:=x*y+c y:= x*y+d 跟蹤表為:,代數(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)+
8、d) 即 y=ax3+bx2+cx+d,分離規(guī)則,條件語(yǔ)句 if p then g else h 可用條件規(guī)則表示出來(lái) (pg | ph)。 為了證明條件語(yǔ)句的正確性,就需要比較預(yù)期函數(shù)f和條件規(guī)則是否相等。,復(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) r22 p1,p2是分離的,即p1 p2為假。 如果一個(gè)條件規(guī)則的所有謂詞都是分離的,稱它為分離規(guī)則。,將條件規(guī)則化為分離規(guī)則,在化簡(jiǎn)和比較條件規(guī)則時(shí),分離
9、規(guī)則比一般的條件規(guī)則使用更方便一些。 一般的復(fù)合規(guī)則不一定能展開(kāi),但分離的復(fù)合規(guī)則總可以展開(kāi)。 一般的條件規(guī)則的前后順序是不能交換的,而分離規(guī)則的順序是可以交換的。 討論程序的正確性時(shí),總是首先將條件規(guī)則化為分離規(guī)則。,將條件規(guī)則化為分離規(guī)則,對(duì)于任意的條件規(guī)則 (p1 r1 | p2 r2 | p3 r3 | ) 化為分離規(guī)則 (p1r1 |p1p2r2|p1p2p3r3 | ),條件語(yǔ)句的正確性證明,假設(shè)某一條語(yǔ)句的程序函數(shù)是分離規(guī)則: (p1r1|p2r2|p3r3) 預(yù)期函數(shù)是f,由于f可以是賦值的形式,例如y:=f(x)的形式給出時(shí),為了證明條件語(yǔ)句的正確性,需證明以下兩點(diǎn): (1)
10、 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),條件語(yǔ)句的正確性證明,另外,當(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ī)則中的謂詞成對(duì)合取后,相應(yīng)的結(jié)果是相同的: p1(x) q1 (x) r1(x) = s1 (x)
11、p1(x) q2 (x) r1(x) = s2(x) p3(x) q1 (x) r3 (x) = s1 (x) p3(x) q2 (x) r3 (x) = s2(x),例子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) = (x:=-x) x0 (x:=x+2*abs(x)=(x:=x+2*(-x)=(x:=-x) 得證,例子2,已知預(yù)期函數(shù)f是(x,y
12、,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,例子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
13、*x+y,a),與預(yù)期函數(shù)相等,因此得證。,循環(huán)不變式產(chǎn)生的方法,對(duì)于程序部分正確性證明的不變式斷言法,這一方法的關(guān)鍵是建立一個(gè)正確的不變式斷言,對(duì)一般程序來(lái)說(shuō),不變式斷言的建立主要依靠程序員對(duì)程序的理解,尚無(wú)系統(tǒng)的方法。 但對(duì)結(jié)構(gòu)化程序來(lái)說(shuō),如果已知它的程序函數(shù),則可以根據(jù)不變式狀態(tài)定理,來(lái)確定它的一個(gè)循環(huán)不變式。,循環(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) 成立,即
14、f(x) = f(x0) ,則執(zhí)行循環(huán)后q(x)也成立,即證明 p(x)q(x) = qg(x) 由p(x)為真,及正確性定理 f=(x,y)|p(x)y=fg(x)|p(x)y=x可知 即 p(x) = (f(x)=fg(x),循環(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),循環(huán)不變式產(chǎn)生的方法,同理可知如下定理: 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),循環(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,循環(huán)不變式產(chǎn)生的方法例2,求程序P: while ab do a,
溫馨提示
- 1. 本站所有資源如無(wú)特殊說(shuō)明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請(qǐng)下載最新的WinRAR軟件解壓。
- 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請(qǐng)聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
- 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁(yè)內(nèi)容里面會(huì)有圖紙預(yù)覽,若沒(méi)有圖紙預(yù)覽就沒(méi)有圖紙。
- 4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
- 5. 人人文庫(kù)網(wǎng)僅提供信息存儲(chǔ)空間,僅對(duì)用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對(duì)用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對(duì)任何下載內(nèi)容負(fù)責(zé)。
- 6. 下載文件中如有侵權(quán)或不適當(dāng)內(nèi)容,請(qǐng)與我們聯(lián)系,我們立即糾正。
- 7. 本站不保證下載資源的準(zhǔn)確性、安全性和完整性, 同時(shí)也不承擔(dān)用戶因使用這些下載資源對(duì)自己和他人造成任何形式的傷害或損失。
最新文檔
- 大五人格與教育政策執(zhí)行力的關(guān)系研究
- 智慧城市防災(zāi)減災(zāi)教育領(lǐng)域的創(chuàng)新與實(shí)踐
- 智慧城市安全防護(hù)新篇章視頻監(jiān)控與大數(shù)據(jù)的融合應(yīng)用
- 教育機(jī)器人在職業(yè)培訓(xùn)中的應(yīng)用和價(jià)值分析
- 教育數(shù)據(jù)分析提升課程設(shè)計(jì)的有效途徑
- 技術(shù)在商業(yè)競(jìng)爭(zhēng)中的關(guān)鍵作用
- 醫(yī)療創(chuàng)新重塑健康管理與醫(yī)療服務(wù)
- 抖音商戶直播價(jià)格策略審批登記制度
- 公交優(yōu)先策略對(duì)2025年城市交通擁堵治理的影響分析報(bào)告
- 公眾參與視角下環(huán)境影響評(píng)價(jià)信息公開(kāi)策略研究報(bào)告
- 2025年7月新疆維吾爾自治區(qū)學(xué)業(yè)水平合格性考試歷史試題(含答案)
- 農(nóng)村農(nóng)資采購(gòu)與供應(yīng)長(zhǎng)期合作協(xié)議
- 反假幣培訓(xùn)課件
- 2025至2030中國(guó)電壓暫降治理行業(yè)產(chǎn)業(yè)運(yùn)行態(tài)勢(shì)及投資規(guī)劃深度研究報(bào)告
- 遼寧省2024年7月普通高中學(xué)業(yè)水平合格性考試化學(xué)試卷(含答案)
- 煤炭造價(jià)知識(shí)培訓(xùn)
- 2025屆遼寧省大連市高新區(qū)英語(yǔ)七年級(jí)第二學(xué)期期末學(xué)業(yè)質(zhì)量監(jiān)測(cè)模擬試題含答案
- 中山大學(xué)強(qiáng)基校測(cè)面試題
- 愛(ài)回收培訓(xùn)課件
- 2025年湖南省中考化學(xué)真題(解析版)
- aopa無(wú)人機(jī)培訓(xùn)管理制度
評(píng)論
0/150
提交評(píng)論