6程序的正確性

1、6. 程序的正確性前面介紹了兩種語義學， 即操作語義學和指稱語義學。 操作語義學方 法的特點是， 從程序的操作角度來說明語言的語義， 可以稱它是個抽 象機的方法；指稱語義方法的特點是，從語法單位的功能即“給什么 出來什么”的角度來說明語言的語義，可以稱它是個函數(shù)化的方法； 公理語義方法的特點是從變量間的邏輯關(guān)系來說明語言的語義， 可以 稱它是個邏輯化的方法。R. W. Floyd發(fā)表了給程序賦予意義一文，提出了一種描述程序意 義的邏輯方法，稱此方法為 Floyd 歸納斷言法。該方法的研究對象是 框圖程序。 Floyd 第一個揭示了程序與邏輯的關(guān)系，從而打開了邏輯 地研究程序性質(zhì)的大門。其中最為

2、重要的是所謂的循環(huán)不變式的問 題，對此 Z. Manna 做了非常深入的研究并發(fā)表了很多有價值的論文。后來，C. A. R. Hoare發(fā)表了計算機程序設(shè)計的公理基礎(chǔ)一文，第 一次用公理系統(tǒng)定義了程序設(shè)計語言的語義。 最有代表性的公理語義 系統(tǒng)是由Hoare和Wirth合作完成的Pascal語言的公理語義。我們知道， 即使一個程序的句法是完全正確的， 它也可能不按它的預(yù) 期行為做事。如何證明程序達到某種預(yù)期目的呢？這就是 “程序驗證” 的任務(wù) 一種普通的程序驗證的方法就是程序測試(program testing),就是讓程 序在關(guān)鍵性的輸入數(shù)據(jù)上運行， 這種方法只能使人更加相信程序是正 確的，

3、但無法保證程序沒有語義錯誤， 因為成功地通過一個子集的測 試僅僅是驗證程序正確的必要條件而不是充分條件。另一種方法就是程序證明(program verification)。公理化方法的優(yōu)點就是能用來證明程序的正確性。 它的主要思想是對給定語言構(gòu)造相應(yīng)的 公理系統(tǒng)。這個公理系統(tǒng)與傳統(tǒng)的公理系統(tǒng)有所不同，從形式上說， 區(qū)別在于它使用了如下形式的公式：P S Q其中 S 是語句， P 和 Q 是邏輯公式。我們稱 P 是前置條件 (Precondition),稱 Q為后置條件(Postcondition)，統(tǒng)稱上述公式為驗 證公式。 P、S 和 Q 中都包含一些程序變量,而 P 和 Q 是這些變量所

4、應(yīng)該滿足的關(guān)系式。顯然, 一個驗證公式成立與否,要依賴于程序變 量的狀態(tài)。如果任何時候驗證公式都成立,則稱驗證公式恒成立,并 記為? P S Q上述驗證公式成立的大致意思是：“如果執(zhí)行S前前置條件p成立并 且S的執(zhí)行終止，則能推出執(zhí)行 S后后置條件Q成立”例如：驗證 公式 x 0x:=x+2x10,在狀態(tài) =8/x 下,執(zhí)行語句 x:=x+2之前成立,同時該語句終止,并且執(zhí)行語句 x:=x+2 后后置條件 x 10成立。 但不難證明在狀態(tài) =5/x 下,盡管前置條件和語句的終止 性都成立，但執(zhí)行語句后其后置條件并不成立。 故上述驗證公式不是 恒成立。假設(shè)有一程序S,計算一 X值并把它放到變量y

5、中，其入口條件是x0。如果能證明？x0Sy= x，則也就證明了程序 S是正確的，即反應(yīng)了程序員的意圖，因此不需要用測試數(shù)據(jù)去一一測試。 但需要 注意的是程序正確的最基本條件是程序要終止，這是需要證明的對 象，而不能由我們自己來假設(shè)，但前面的驗證公式把該程序終止性作 為已知條件使用了，因此，上述證明是不完全的，故稱上述證明為部 分正確性的證明。6.1程序正確性的詳細說明程序驗證就是要證明滿足某設(shè)定的規(guī)范(specification)。規(guī)范是系統(tǒng)所 要滿足的需求的體現(xiàn)，它是以實現(xiàn)者易于理解的方式，表達所期望的 行為的一種精確而形式的陳述。下面是一些非形式化的規(guī)范：(1) 對于所有輸入值a, b N

6、at,滿足a, b>0，程序計算的是a和b 的最大公約數(shù)gcd(a, b)。(2) 對于所有輸入值a, bNat，滿足a, b>0，程序終止，輸出值 是 gcd(a, b)。對于一計算最大公約數(shù)的遞歸程序 S,規(guī)范可寫成：(2a, b Nat，若 a, b>o，貝S M(S)(a, b)有定義且M(S)(a, b)=gcd(a, b)。 顯然規(guī)范( 2)等價于下面兩個規(guī)范：(3) 對于所有輸入值a, b Nat,滿足a, b>o。若程序終止，則它終止的輸出值是gcd(a, b)。和(4) 對于所有輸入值a, b Nat，滿足a, b>o，程序終止。對于遞歸程序S的

7、規(guī)范(2，與它等價的規(guī)范：(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)有定義。規(guī)范( 3)或( 3( 4)或( 4程序是否終止。這兩種規(guī)范合起來就構(gòu)成完全正確性的規(guī)范。定義 6.1 (有關(guān)謂詞的正確性)令B是謂詞邏輯的基，I是該基的一種解釋。是相應(yīng)的狀態(tài)集合。令S 一 LiB是中的框圖程序或L2B中的while-程序。M|(S)是程序的含 義。進一步令 :Bool 和 :Bool 是兩個謂詞，分別稱為前置條件(precondition)和后置條件(p

8、ostcondition)。稱程序S,( 1) 在解釋 I 下，有關(guān)謂詞(partially correctw. r. t predicates and )，如果對于所有狀態(tài)，若 ( )=true 且 MI(S)( )(MI(S)( )=true。(2) 在解釋I下，有關(guān)謂詞終止(terminate)，如果對于所有狀態(tài)，若 ( )=true 則 MI(S)( )有定義。(3) 在解釋I下，有關(guān)謂詞和 是完全正確的(totally correct)，如果對于所有狀態(tài)，若（）=true 則 Mi（s）（）有定義且（Mi（S）（）二true定義6.2 （有關(guān)公式的正確性）令B, I和S如定義6.1所

9、述，p, q WFFb是兩個公式，稱程序S,在 解釋|下，有關(guān)公式p和q是部分正確的，如果它關(guān)于謂詞|（p）和|（q） 是部分正確的，類似可定義有關(guān)公式的完全正確性和終止性。例6.3（a）計算整數(shù)平方根的程序（例 3.2），它的完全正確性規(guī)范可陳述為：程序有關(guān)前置條件true和后置條件y/ xx<（yi+1）2是完全正確的。（b）令S是一計算最大公約數(shù)的框圖程序或循環(huán)程序。規(guī)范（2）可重述為：程序有關(guān)前置條件 x=a y=b a>0b>0和后置條件x=gcd（a, b）是完全正確的。（c）某框圖程序或循環(huán)程序關(guān)于前置條件true和后置條件false是部 分正確的 肝它的含義函

10、數(shù)處處沒定義（everywhere undefined。（d） 某框圖程序或循環(huán)程序關(guān)于前置條件true終止肝它的含義函數(shù) 是一個全函數(shù)（即處處有定義）。1. 注意某些規(guī)范，比如“一個程序關(guān)于true和true是部分正確的”， 根本沒有什么意義，因為每個程序的終止狀態(tài)都滿足后置條件 true,使其為真。類似的例子見 ex6.1-1。2. 使P S Q成立的前置條件和后置條件可能有無窮多個，例如使px:=x+1x2成立的p有無窮多個，如x 1, x 2, x3,。其中最弱的條件是 x 1，這表示“要使 x 2 成立，執(zhí)行前 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 存在一狀態(tài)，使得 ( )=true 且MI(S)()= 。RMK.(1) (條件強弱的含義)設(shè)p, q是謂詞，且有p q,則稱p強于q, 稱 q 弱于 p。 (2) wlp(S, )的定義中并不要求程序終止,所以它與“部分正確” 呼應(yīng)； wp(S, )與“完全正確”呼應(yīng)。下面的定理進一步說明了“最弱”和“最強”的含義。定理 6.5 令 B, I, S 和 如定義 6.1 或 6.4 所述。(1) 令 是S和 的最弱自由前置條件，那么(a)S關(guān)于 和 是部分正確的；和(b)對于謂詞，若滿足S關(guān)于 和 是部分正確 的，則對于所有狀態(tài)，( )( )。(2) 對于“最

13、弱前置條件”和“完全正確”也有類似( 1)的結(jié)論。( 3) 令 是 和 S 的最強后置條件，那么 (a)S 關(guān)于 和 是部分正 確的，(b)對于謂詞，若它滿足S關(guān)于 和 是部分正確的， 則對于所有狀態(tài)，( )( )。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. 注意這里并沒有給出循環(huán)語句的最弱 (自由)前置條件的求法， 其原因是在用Hoare公理系統(tǒng)證明程序時，并不用最弱條件，而是用 循環(huán)不變式。定理 (求最強后置后件)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)即可。因為公理系統(tǒng)有推論規(guī)則， 可以得到最終結(jié)論。引理：令(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證明：(歸納基礎(chǔ))因n=1, ln=li二begin。于是li=test，這是不可能的。所以命題無 意義而為真。(歸納步) 假設(shè)對于 j=1, , n

16、 命題成立。往證對于 n+1 ，命題也成立。假設(shè)ln+1二test。根據(jù)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 。容易驗證結(jié)論成立。(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根據(jù)