事物的正確答案不止一個130-人教版

1精選課件ppt1精選課件ppt本章內(nèi)容軟件驗證的框架部分正確性證明完全正確性證明演算2精選課件ppt本章內(nèi)容軟件驗證的框架2精選課件ppt程序驗證概略模型檢測主要適合驗證能夠用有限狀態(tài)進行模型化的系統(tǒng)。不能處理運行于單個處理器的順序程序等具有無限狀態(tài)空間的系統(tǒng)程序驗證基于證明：使用一種證明演算構(gòu)造系統(tǒng)滿足所需性質(zhì)的一個證明半自動面向性質(zhì)應用領域：順序變換程序（不存在并發(fā)問題）軟件開發(fā)前后都可以適用3精選課件ppt程序驗證概略模型檢測主要適合驗證能夠用有限狀態(tài)進行模型化的系軟件驗證的一種框架將應用領域中需求的非形式描述R轉(zhuǎn)化成某種符號邏輯中“等價的”公式Φ；在編程環(huán)境中，編寫一個能實現(xiàn)Φ的程序P；證明程序P滿足公式Φ；4精選課件ppt軟件驗證的一種框架將應用領域中需求的非形式描述R轉(zhuǎn)化成某種符一種核心程序設計語言包含：整數(shù)值和布爾變量的賦值If，while語句順序合成不包含：對象過程，線程遞歸數(shù)據(jù)結(jié)構(gòu)5精選課件ppt一種核心程序設計語言包含：5精選課件ppt語法論域整數(shù)表達式布爾表達式命令6精選課件ppt語法論域整數(shù)表達式6精選課件ppt整數(shù)表達式的語法E::=n|x|(-E)|(E+E)|(E-E)|(E*E)n:{…,-2,-1,0,1,2,…}x:任意變量例：5，x，4+(x-3),x+(x*(y-(5+z)))7精選課件ppt整數(shù)表達式的語法E::=n|x|(-E)|(E+E)|(E布爾表達式的語法B::=true|false|(!B)|(B&B)|(B||B)|(E<E)E1==E2:(E1<E2)&!(E2<E1)8精選課件ppt布爾表達式的語法B::=true|false|(!命令的語法C::=x=E|C;C|ifB{C}else{C}|whileB{C}x=E: 當前狀態(tài)下計算整數(shù)表達式E的值，然后用該計算的結(jié)果復寫儲存在x中的當前值C;C： 命令C1和C2的順序合成。開始在當前儲存狀態(tài)下執(zhí)行C1。若執(zhí)行終止，則在執(zhí)行C1的結(jié)果后的儲存狀態(tài)下執(zhí)行C2，否則C1的執(zhí)行不終止，運行C1,C2也不終止。ifB{C}else{C} 在當前存儲狀態(tài)下計算布爾表達式B。若結(jié)果為真，則執(zhí)行C1；若B計算為假，則執(zhí)行C2。9精選課件ppt命令的語法C::=x=E|C;C|ifB{C}e命令的語法whileB{C}1.在當前存儲狀態(tài)下計算布爾表達式B的值2.若B計算為假，則命令終止3.否則執(zhí)行C。若該執(zhí)行終止，則用已更新的存儲狀態(tài)下重新計算的B值再次從步驟(1)開始10精選課件ppt命令的語法whileB{C}10精選課件ppt例計算x的階乘的程序Fac1 y=1; z=0; while(z!=x){ z=z+1; y=y*z; }11精選課件ppt例計算x的階乘的程序Fac111精選課件ppt霍爾三元組計算數(shù)y，其平方小于輸入x?！鷜×y<xx為負數(shù)時，需求變?yōu)椋喝糨斎離是正數(shù)，計算一個平方小于x的數(shù)。 (|x>0|P(|y.y<x|)霍爾三元組： (|Φ|P|Ψ|)若程序P在一個滿足Φ的狀態(tài)下運行，則執(zhí)行P的結(jié)果狀態(tài)滿足Ψ。Φ：P的前置條件；Ψ：P的后置條件12精選課件ppt霍爾三元組計算數(shù)y，其平方小于輸入x。12精選課件ppt霍爾三元組核心程序的存儲或狀態(tài)是將每個變量x指派為一個整數(shù)l(x)的函數(shù)l；對帶有函數(shù)符號(負號),-，+，*以及二元謂詞符號<和=的謂詞邏輯公式Φ，狀態(tài)l滿足Φ(l|=Φ)，當且僅當M|=Φ成立；要求|Φ|和|Ψ|中的量詞只約束未出現(xiàn)在程序P中的變量。13精選課件ppt霍爾三元組核心程序的存儲或狀態(tài)是將每個變量x指派為一個整數(shù)l例對滿足l(x)=-2,l(y)=5,l(z)=-1的任意狀態(tài)l，關(guān)系L|=?(x+y)<z成立L|=y-x*z<z不成立L|=u(y<u→y*z(u*z)不成立14精選課件ppt例對滿足l(x)=-2,l(y)=5,l(z)=-1的任意狀(|x>0)|P(|y.y<x|)并不能規(guī)范唯一的程序P例y=0while(y*y<x){ y=y+1;}y=y-115精選課件ppt(|x>0)|P(|y.y<x|)15精選課件ppt部分正確性如果對滿足Φ的所有狀態(tài)，只要P實際終止。執(zhí)行P后的結(jié)果狀態(tài)就滿足后置條件Ψ，我們說三元組(|Φ|P|Ψ|)在部分正確意義下滿足。此時，關(guān)系|=par(|Φ|P|Ψ|)成立。|=par：部分正確性的滿足關(guān)系任何不終止的程序都滿足其規(guī)范例：whiletrue{x=0;}16精選課件ppt部分正確性如果對滿足Φ的所有狀態(tài)，只要P實際終止。執(zhí)行P后的完全正確性我們說三元組(|Φ|P|Ψ|)在完全正確意義下滿足，如果前置條件Φ的所有狀態(tài)下執(zhí)行程序P，P肯定終止。而且結(jié)果狀態(tài)滿足后置條件Ψ。此時，關(guān)系|=tot(|Φ|P|Ψ|)成立。|=tot：完全正確性的滿足關(guān)系不終止的程序都不滿足其規(guī)范17精選課件ppt完全正確性我們說三元組(|Φ|P|Ψ|)在完全正確意義下滿足證明的規(guī)范類型的典型例子Succa=x+1;If(a-1==0){ y=1;}else{ y=a；}在部分性和完全性的意義下滿足規(guī)范(||Succ(|y=(x+1|)Fac1y=1; z=0; while(z!=x){ z=z+1; y=y*z;}|=tot(|x≧0|Fac1|Ψ|)成立|=tot(|

|Fac1|Ψ|)不可證|=par(|x≧0|Fac1|Ψ|)可證|=par(|

|Fac1|Ψ|)可證18精選課件ppt證明的規(guī)范類型的典型例子SuccFac118精選課件ppt定義若三元組(|Φ|P|Ψ|)的部分正確性可以用部分正確性演算所證明，稱|-par(|Φ|P|Ψ|)是有效的。若三元組(|Φ|P|Ψ|)的完全正確性可以用完全正確性演算所證明，稱|-tot(|Φ|P|Ψ|)是有效的。|-par是合理的：如果對所有Φ，P和Ψ，只要|-par(|Φ|P|Ψ|)是有效的，則|-par(|Φ|P|Ψ|)成立。|-tot是合理的：如果對所有Φ，P和Ψ，只要|-tot(|Φ|P|Ψ|)是有效的，則|-tot(|Φ|P|Ψ|)成立。|-par是完備的：如果對所有Φ，P和Ψ，只要||-par(|Φ|P|Ψ|)成立，則|-par(|Φ|P|Ψ|)是有效的。|-tot是合理的：如果對所有Φ，P和Ψ，只要||-tot(|Φ|P|Ψ|)成立，則|-tot(|Φ|P|Ψ|)是有效的。19精選課件ppt定義若三元組(|Φ|P|Ψ|)的部分正確性可以用部分正確性演邏輯變量對于霍爾三元組(|Φ|P|Ψ|)，其邏輯變量的集合是在Φ或Ψ中自由但不出現(xiàn)在P中的變量例Fac220精選課件ppt邏輯變量對于霍爾三元組(|Φ|P|Ψ|)，其邏輯變量的集合是例Fac2y=1;while(x!=0){y=y*x;x=x-1;}(|x≧0|)Fac2(|y=x!|)(|x=x0∧x≧0|)Fac2(|y=x!|)Sumz=0;while(x>0){z=z+x;x=x-1;}(|x=x0∧x≧0|)Sum(|z=x0(x0+1)/2|)21精選課件ppt例Fac2Sum21精選課件ppt部分正確性證明證明規(guī)則復合(|Φ|)C1(|η|) (|η|)C2(|Ψ|) (|Φ|)C1;C2(|Ψ|)

22精選課件ppt部分正確性證明證明規(guī)則22精選課件ppt賦值 (|Ψ[E/x]|)x=E(|Ψ|)例Ψ：x=6，E=5(|Ψ|)x=E(|Ψ[E/x]|)（不成立）在驗證過程中，反向應用公理比正向應用要好若知道Ψ希望找到使(|Φ|)x=E(|Ψ|)的Φ很容易。如果知道Φ希望找到使(|Φ|)x=E(|Ψ|)的Ψ不容易。使用反向公理，應用完全是機械的。23精選課件ppt賦值23精選課件ppt賦值的實例P是程序x=2(|2=2|)P(|x=2|)(|2=4|)P(|x=4|)(|2=y|)P(|x=y|)(|2>0|)P(|x>0|)24精選課件ppt賦值的實例P是程序x=224精選課件ppt賦值的實例P是x=x+1(|x+1=2|)P(|x=2|)(|x+1=y|)P(|x=y|)(|x+1+5=y|)P(|x+5=y|)(|x+1>0∧y>0|)P(|x>0∧y>0|)25精選課件ppt賦值的實例P是x=x+125精選課件pptIf語句(|Φ∧B|)C1(|Ψ|) (|Φ∧?B|)C2(|Ψ|) (|Φ|)ifB{C1}else{C2}(|Ψ|)26精選課件pptIf語句26精選課件pptWhile語句 (|Ψ∧B|)C(|Ψ|) (|Ψ|)whileB{C}(Ψ∧?B)Ψ:不變量27精選課件pptWhile語句 (|Ψ∧B|)C(|Ψ|)27精選課件蘊含 |-Φ→Φ’(|Φ|)C(|Ψ|)|-Ψ→Ψ’

(|Φ’|)C(|Ψ|)’

28精選課件ppt蘊含 |-Φ→Φ’(|Φ|)C(|Ψ|)|-Ψ用證明規(guī)則證明例

Fac1y=1;z=0;while(z!=x){ z=z+1; y=y*z;}29精選課件ppt用證明規(guī)則證明例

Fac129精選課件ppt證明布景將程序看成一個序列C1;C2;…;Cn。Ci都不是更小程序的復合。通過公式與代碼的交織給出|-par

(|Φ0|)C(|Ψn|)的一個證明：(|Φ0|)C1;(|Φ1|)C2;…;(|Φn|)(|Φ0|)C1;C2;…;Cn(|Ψ|)證明布景的構(gòu)造從后置條件Ψ開始，通過Cn將其上推，然后是Cn-1，直到最頂端出現(xiàn)一個公式Φ’。如果復合程序C1;C2;…;Cn-1執(zhí)行后終止。用蘊含規(guī)則檢驗Φ’是否能由已知的前置條件Φ得到。30精選課件ppt證明布景將程序看成一個序列C1;C2;…;Cn。Ci都不是更賦值的例證明|-par(|y=5|)x=y+1(|x=6|)是有效的 (|y=5|) (|y+1=6|)蘊含 x=y+1; (|x=6|)賦值31精選課件ppt賦值的例證明|-par(|y=5|)x=y+1(|x=6|)賦值的例|-par(|y<3|)y=y+1(|y<4|)是有效的 (|y<3|) (|y+1<4|) y=y+1; (|y<4|)32精選課件ppt賦值的例|-par(|y<3|)y=y+1(|y<4|)是有賦值的例對于賦值語句的順序合成z=x;z=z+y;u=z;證明|-par(||)P(|u=x+y|) (||) (x+y=y+x)z=x; (z+y=x+y)z=z+y; (|z=x+y|)u=z; (|u=x+y|) 33精選課件ppt賦值的例對于賦值語句的順序合成 (||)33精選課件p賦值的例 (|x+1=x+1|) x=x+1； (|x=x+1|)

(|x+2=y+1|) y=y+1000001； x=x+2; (|x=y+1|)

34精選課件ppt賦值的例 (|x+1=x+1|) (|x+2=y+1|)If語句計算最弱的Φ(|Φ|)ifB{C1}else{C2}(|Ψ|)通過C1將Ψ往上推，稱結(jié)果為Φ1.通過C1將Ψ往上推，稱結(jié)果為Φ2.令（B→Φ1)∧（?B→Φ2)35精選課件pptIf語句計算最弱的Φ35精選課件pptIf語句的例(|Φ1|C1(|Ψ|)(|Φ2|C2(|Ψ|)（B→Φ1)∧(?B→Φ2)ifB{C1}else{C2}(|Ψ|)

中間條件(a-1=0→1+x+1)∧(?(a-1=0)→a=x+1)Succa=x+1;If(a-1==0){ y=1;}else{ y=a；}Φ1:1=x+1Φ2:a=x+136精選課件pptIf語句的例(|Φ1|C1(|Ψ證明

(||) (|(x+1-1=0→1=x+1|)∧(?(x+1-1=0)→x+1=x+1)|) a=x+1； (|(a-1=0→1=x+1|)∧(?(a-1=0)→a=x+1)|) If(a-1==0){ (|1=x+1|) y=1; (|y=x+1|) }else (|a=x+1|) y=a; (|y=x+1|)} (|y=x+1|)37精選課件ppt證明 (||)37精選課件pptWhile語句 (|η∧B|)C(|η|) (|η|)whileB{C}(|η∧?B|)B為假，C不執(zhí)行。η的真值沒有變化B為真，則執(zhí)行C，在執(zhí)行完C后，η為真。-若現(xiàn)在B為假，停止于η∧?B。-若B為真，再執(zhí)行C，η重新確立。這個while語句終止，當且僅當在C執(zhí)行了有限次后，B為假，停止于η∧?B。38精選課件pptWhile語句 (|η∧B|)C(|η|)38精選課件While語句證明(|Φ|)whileB{C}(Ψ)|-Φ→η|-η∧?B→Ψ|-par(|η|)while(B){C}(|η∧?B|)關(guān)鍵是找出合適的不變量η。定義：while語句while(B){C}的不變量是使||-par(|η|)while(B){C}(|η∧?B|)成立的一個公式η；即對所有狀態(tài)l，若η和B在l下為真，且C從狀態(tài)l開始執(zhí)行并終止，則在結(jié)果狀態(tài)下η仍為真。39精選課件pptWhile語句證明(|Φ|)whileB{C}(Ψ)39精選例 y=1; z=0;l1： while(z!=x){ z=z+1; y=y*z;l2: }從一個x=6的狀態(tài)下執(zhí)行不變量:y=z!while語句的前置條件:y=1∧z=0后置條件：y=x!|-(y=1∧z=0)→(y=z!)|-(y=z!∧x=z)→(y=x!)有效

迭代次數(shù)Z在l1處的值y在l1處的值B在l1處的值001真111真222真336真4424真55120真66720假40精選課件ppt例 y=1; 迭代次數(shù)Z在l1處的值y在l1處的值B在l1處證明步驟猜測公式η，希望它是一個合適的不變量。嘗試證明|-η∧?B→Ψ和|-Φ→η是有效的。通過while語句的程序體C將η往上推。將出現(xiàn)的公式命名為η’。嘗試證明|-η∧B→η’是有效的。在while語句的上面寫出η。41精選課件ppt證明步驟猜測公式η，希望它是一個合適的不變量。41精選課件p證明例 (||) (|1=0!|)y=1; (|y=0!|)z=0; (|y=z!|)While(z!=x){ (|y=z!∧z≠x|) (|y·(z+1)=(z+1)!|)z=z=1； (|y·z=z!|)Y=y*z; (|y=z!|)} (|y=z!∧?(z≠x)|) (|y=x!|) y=1; z=0;l1： while(z!=x){ z=z+1; y=y*z;l2: }while語句的前置條件:y=1∧z=0后置條件：y=x!|-(y=1∧z=0)→(y=z!)|-(y=z!∧x=z)→(y=x!)有效42精選課件ppt證明例 (||) y=1;42精選課件ppt練習證明|-par(|x≧0|)Copy1(|x=y|),其中Copy2為：a=x y=0; while(a!=0){ y=y+1;a=a-1; }證明|-par(|y≧0|)Multil(|z=x*y|),其中Multil為：a=0; z=0; while(a!=y){ z=z+x;y=y-1; }43精選課件ppt練習證明證明43精選課件ppt案例研究：最小和截段設a[0],a[1],…,a[n-1]是數(shù)組a的整數(shù)值。a的裁段是一個連續(xù)的片段a[i],…,a[j],其中0≤i≤j<n.Si,j表示這個片段的和Si,j=a[i],a[i+1],…,a[j]。最小和截段是a的截段a[i],…,a[j]，使得該截段的和Si,j小于或等于a的任何其他截斷a[i’],…,a[j’]的和Si’,j’。例[-1,3,15,-6,4,-5]的最小裁段為[-6,4,-5],最小和為-7[1,-1,3,-1,1]的最小裁段為[1,-1]和[-1,1]，最小和為-744精選課件ppt案例研究：最小和截段設a[0],a[1],…,a[n-1]是最小和截段的算法列出給定數(shù)組的所有可能的截段遍歷這些截斷列表，計算每個截段的和45精選課件ppt最小和截段的算法列出給定數(shù)組的所有可能的截段45精選課件pp0(n)的算法k=1;t=a[0];s=a[0];while(k!=n){t=min(t+a[k],a[k]);s=min(s,t);k=k+1;}46精選課件ppt0(n)的算法k=1;46精選課件ppt需求規(guī)范S1：(||)Min_Sum(|?i,j(0≤i≤j<n→s≤Si,j)|)S2:(||)Min_Sum(|?i,j(0≤i≤j<n∧s=Si,j)|)47精選課件ppt需求規(guī)范S1：47精選課件ppt不變量Inv1(s,k)=?i,j(0≤i≤j<k→s≤Si,j)|)Inv2(t,k)=?i(0≤i<k→t≤Si,k-1)|)48精選課件ppt不變量Inv1(s,k)=?i,j(0≤i≤j<k→s≤證明(||)(|Inv1(a[0],1)∧Inv2(a[0],1)|)K=1;(|Inv1(a[0],k)∧Inv2(a[0],k)|)T=a[0];(|Inv1(a[0],k)∧Inv2(t,k)|)S=a[0];(|Inv1(s,k)∧Inv2(t,k)|)while(k!=n){

(|Inv1(s,k)∧Inv2(t,k)∧k≠n|)(|Inv1(min(s,min(t+a[k],a[k])),k+1)∧Inv2(min(t+a[k],a[k]),k+1)|)t=min(t+a[k],a[k]);(|Inv1(min(s,t),k+1)∧Inv2(t,k+1)|)s=min(s,t);(|Inv1(s,k+1)∧Inv2(t,k+1)|)k=k+1;(|Inv1(s,k)∧Inv2(t,k)|)}(|Inv1(s,k)∧Inv2(t,k)∧??(k=n)|)Inv1(s,n)|)49精選課件ppt證明(||)49精選課件ppt引理設s,t是任意整數(shù)，n是數(shù)組a的長度，而k是范圍在0<k<n中的數(shù)組的索引。則(|Inv1(s,k)∧Inv2(t,k)∧k≠n|)蘊含1.Inv1(min(s,min(t+a[k],a[k])),k+1)2.Inv2(min(t+a[k],a[k]),k+1)證明：1.任何滿足0≤i<k+1的i，將證明min(t+a[k],a[k])≤Si,k。若i<k,則Si,k=Si,k-1+a[k],故需證min(t+a[k],a[k])≤Si,k-1+a[k],t≤Si,k-1,所以兩邊加上a[k]就得到結(jié)果。否則，i=k