1、中南大學 信息科學(xn x k xu)與工程學院 任勝兵主要(zhyo)內容 程序正確性證明(zhngmng) 調試第1頁/共34頁第一頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵7.9 程序正確性證明(zhngmng) 測試可以幫助人們發現程序中的錯誤，但它卻不能證明程序中沒有錯誤。 早在50年代，圖林（Turing）等人就開始注意并開展了程序正確性證明這方面的早期研究工作；60年代后半期，Floyd和Hoare等人提出了不變式斷言法和公理化方法，使得這一研究進入(jnr)了一個蓬勃發展的新階段；在此之后，出現了許多不同的程序正確性證明方法。 第2頁/共34頁第

2、二頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵7.9.1 程序正確性定義(dngy) 所謂一段程序是正確的，是指這段程序能準確無誤地完成預定的功能。或者說，對任何一組允許的輸入，程序執行后能得到一組相應的正確的輸出(shch)。 在研究程序正確性證明時，將一段程序的輸入和輸出(shch)應滿足的條件的邏輯關系式分別稱為此段程序的輸入斷言（或初始斷言、前置斷言）和輸出(shch)斷言（或結果斷言、后置斷言），通常用謂詞(x)和(x，z)表示，其中x和z分別表示輸入和輸出(shch)數據（可以是一個或一組變量）。第3頁/共34頁第三頁，共34頁。中南大學 信息科學(xn

3、 x k xu)與工程學院 任勝兵例子(l zi) unsigned power(unsigned x,unsigned y) unsigned z; z=1; while (x!=0) z=z*y; x=x-1; return z; 則 (x,y):x0, y0；(x,y,z):z=yx。 第4頁/共34頁第四頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵程序正確性三種(sn zhn)類型 程序(chngx)的部分正確性 程序(chngx)的終止性 程序(chngx)的完全正確性 第5頁/共34頁第五頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院

4、任勝兵程序(chngx)的部分正確性 若每一個使得（x）為真且程序計算終止的輸入數據x，（x，p（x）都為真，則稱程序p關于和是部分正確的。 這里(zhl)p（x）表示與輸入數據x相對應的程序p的輸出數據。第6頁/共34頁第六頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵程序(chngx)的終止性 若每一個(y )使得（x）為真的輸入數據x，程序計算都終止，則稱程序P對是終止的。 第7頁/共34頁第七頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵程序(chngx)的完全正確性 若每一個使得（x）為真的輸入數據x，程序計算都終止且（x，P（x）

5、為真，則稱程序P關于和是完全正確的。 顯然(xinrn)，一個程序是完全正確的等價于該程序是部分正確的同時又是終止的。 第8頁/共34頁第八頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵程序正確性證明(zhngmng)方法 FLOYD的不變式斷言法（證明部分正確性） FLOYD良序集方法（證明終止性） Hoare的公理化方法（證明部分正確性）及其推廣(tugung)（證明完全正確性） Dijstra的弱謂詞置換法（證明完全正確性） 第9頁/共34頁第九頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵7.9.2 Floyd不變式斷言(dunyn)

6、法 建立斷言 一個程序除了需要建立輸入/輸出斷言外，如程序中出現循環，還要建立相應于該循環的不變式斷言，稱之為循環不變式斷言。所謂循環不變式斷言，是在循環中選一個斷點，在斷點處建立一個適當的斷言，使循環每次執行到斷點時，斷言都為真。 建立檢驗條件 所謂檢驗條件就是程序運行通過某通路時應滿足的條件。 證明檢驗條件 證明上面給定(i dn)的所有檢驗條件，如果每一條通路的檢驗條件都為真，則該程序是部分正確的。第10頁/共34頁第十頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵例子(l zi) 設x1，x2是正整數，求最大公約數Z=gcd（x1，x2），其流程圖如下(rxi

7、)圖所示。試證明它的部分正確性。 第11頁/共34頁第十一頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵建立(jinl)(jinl)斷言 輸入斷言（x）：x10 x20 輸出斷言（x，z）：z=gcd（x1，x2） 在斷點(dun din)B建立不變式斷言P（x，y）： x10 x20y10y20gcd（y1，y2）=gcd（x1，x2）這里，約定所有變量均為整型，且x表示（x1，x2），y表示（y1，y2）。第12頁/共34頁第十二頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵建立檢驗(jinyn)(jinyn)條件 選擇B為斷點，則程序(

8、chngx)的執行通路為： Path1：AB Path2：BDB Path3：BEB Path4：BGC 對每條通路可建立相應的檢驗條件。第13頁/共34頁第十三頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵檢驗條件(tiojin)(tiojin)表示設通路i的輸入/輸出(shch)斷言分別為i（x,y）和i（x，y），而通過此通路的條件為Ri(x,y)，通過此通路后y的值變為ri(x,y)，則應有檢驗條件： i（x，y）Ri（x，y）i（x，ri（x，y） 其中，y表示程序執行中的一組中間變量，x是輸入量。符號表示蘊涵邏輯關系。第14頁/共34頁第十四頁，共34頁。

9、中南大學 信息科學(xn x k xu)與工程學院 任勝兵Path1檢驗(jinyn)條件 1（x，y）為（x）；R1（x，y）恒真，即無條件通過(tnggu)； 1（x，y）為P（x，y）；通過(tnggu)此通路后y的值取值x。 故有：（x）P（x，x），即 x10 x20 x10 x20 x10 x20gcd（x1，x2）=gcd（x1，x2）其它路徑的檢驗條件（略）第15頁/共34頁第十五頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵證明檢驗(jinyn)(jinyn)條件 對任意正整數y1和y2有如下(rxi)關系： 1若y1y2則gcd(y1,y2)=gc

10、d(y1-y2,y2)； 2若y2y1則gcd(y1,y2)=gcd(y1,y2-y1)； 3若y1=y2則gcd(y1,y2)=y1=y2。 對于Path1，其檢驗條件顯然是成立的； 其它（略）第16頁/共34頁第十六頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵7.9.3 Floyd良序集方法(fngf) 如果一個非空集合W關于二元關系-是良序的，則集合W應滿足：W為具有關系-的偏序集。 即關系-滿足下列性質： 1傳遞性，即對一切a，b，cW，如果a-b，b-c則有a-c。 2反對稱性，即對一切a，bW，如果a-b，則有b-a。 3反自反性，即對一切aW，a -

11、a1 - a2 - 其中a0，a1，a2,.W。 第17頁/共34頁第十七頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵證明(zhngmng)(zhngmng)步驟 設程序P的輸入斷言為（x），良序集法證明P關于（x）是終止的證明步驟 （1）選取一個點集合截斷程序的各個循環部分，在每一個截斷點i處建立一個中間斷言qi（x，y）。 （2）選取一個良序集（W，- Ej（x，r（x，y）顯然，如果所有的終止條件成立，則程序P一定終止。第18頁/共34頁第十八頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵例子(l zi) 對任一給定(i dn)的自然

12、數X，計算Z= （即Z等于x的平方根取整）的程序流程圖如圖所示。 X第19頁/共34頁第十九頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵截斷程序的循環(xnhun)(xnhun)部分 該程序(chngx)只有一個循環，在B點將循環斷開，并建立斷點斷言：q（x，y）：y30 y2x第20頁/共34頁第二十頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵選取(xunq)(xunq)良序集 選取(xunq)良序集為（N，0，故有x-y2X-（y2+y3）且均屬于集合（N，）中。至此，也就證明了該程序的終止性。第24頁/共34頁第二十四頁，共34頁。

13、中南大學 信息科學(xn x k xu)與工程學院 任勝兵7.9.4 程序正確性證明(zhngmng)的局限性 經驗表明，程序證明實現的困難在于尋找程序的循環結構所蘊涵的循環不變式。 只有當程序“做什么”的說明能以簡單的函數(hnsh)給出時，才能使用程序正確性證明技術。而大型問題就難以給出這種說明。因此，在實際應用中還存在一些問題。 所依賴的數學基礎太強，用起來不夠自然，數學素質不強的人很難接受。另外，證明本身也不能保證無錯。第25頁/共34頁第二十五頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵7.10 調 試 q調試，又稱糾錯或排錯，是程序測試后開始的工作，主要

14、任務是依據測試發現的錯誤跡象(jxing)確定錯誤位置和原因，并加以改正。q調試活動由兩部分組成：q 確定程序中可疑錯誤的確切性質和位置。q 對程序（設計，編碼）進行修改，排除這個錯誤。q調試是通過現象，找出原因的一個思維分析的過程。第26頁/共34頁第二十六頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵7.10.1 調試(dio sh)的步驟 n從錯誤的外部表現形式入手，確定程序中出錯位置；n研究有關部分的程序，找出錯誤的內在原因；n修改設計和代碼，以排除這個錯誤；n重復進行暴露了這個錯誤的原始測試或某些有關測試，以確認該錯誤是否被排除；是否引進了新的錯誤。n如果所

15、做的修正無效，則撤消(chxio)這次改動，重復上述過程，直到找到一個有效的解決辦法為止。第27頁/共34頁第二十七頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵調試(dio sh)難點 錯誤的癥狀和引起錯誤的原因可能相隔(xingg)很遠，尤其是在高度耦合的程序結構中； 錯誤癥狀可能在另一錯誤被糾正后消失或暫時性的消失； 錯誤癥狀可能實際并不是由錯誤引起的（如舍入誤差）； 錯誤癥狀可能是由不易跟蹤的人工操作引起的； 錯誤癥狀可能是和時間相關的，而不是處理問題； 很難再現產生錯誤癥狀的輸入條件； 錯誤癥狀可能時有時無（如在軟硬件結合的嵌入式系統中常常遇到）； 錯誤癥狀

16、可能是由于把任務分布在若干不同處理器上運行而造成。 第28頁/共34頁第二十八頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵7.10.2 調試(dio sh)的策略之一：猜測法 該方法通過分析錯誤癥狀，根據以往經驗，輔助使用已有的計算機工具，猜測錯誤的原因并進行定位。可以通過“在程序中插入打印語句”、“使用注釋或GOTO語句運行(ynxng)部分程序”或“調試工具”等來實現該方法。第29頁/共34頁第二十九頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵跟蹤(gnzng)(gnzng)法 n先分析錯誤征兆，確定最先發現“癥狀”的位置(wi zh

17、i)。然后，人工沿程序的控制流程，向回追蹤源程序代碼，直到找到錯誤根源或確定錯誤產生的范圍。n跟蹤法對于小程序很有效，往往能把錯誤范圍縮小到程序中的一小段代碼；仔細分析這段代碼不難確定出錯的準確位置(wi zhi)。但對于大程序，由于回溯的路徑數目較多，回溯會變得很困難。第30頁/共34頁第三十頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵演繹法無剩余列舉可能的原因排除不會發生的原因細析余下的原因證明假設糾正錯誤收集更多的測試結果有剩余不能能 演繹法排錯是測試人員首先根據已有的測試用例，設想及枚舉出所有可能出錯的原因做為假設；然后再用原始測試數據或新的測試，從中逐個排除不可能正確(zhngqu)的假設；最后，再用測試數據驗證余下的假設確是出錯的原因。第31頁/共34頁第三十一頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵歸納法 歸納法排錯的基本思想是：從一些線索（錯誤征兆）著手(zhushu)，通過分析它們之間的關系來找出錯誤。收集有關數據組織數據研究數據間的關系提出假設證明假設糾正錯誤能不能能不能第32頁/共34頁第三十二頁，共34頁。中南大學 信息科學(xn x k xu)與工程學院 任勝兵7.10.3 調試(