軟件驗(yàn)證技術(shù)PPT課件

1、中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵主要內(nèi)容 程序正確性證明 調(diào)試第1頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵7.9 程序正確性證明 測(cè)試可以幫助人們發(fā)現(xiàn)程序中的錯(cuò)誤，但它卻不能證明程序中沒(méi)有錯(cuò)誤。 早在50年代，圖林（Turing）等人就開始注意并開展了程序正確性證明這方面的早期研究工作；60年代后半期，F(xiàn)loyd和Hoare等人提出了不變式斷言法和公理化方法，使得這一研究進(jìn)入了一個(gè)蓬勃發(fā)展的新階段；在此之后，出現(xiàn)了許多不同的程序正確性證明方法。 第2頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵7.9.1 程序正確性定義 所謂一段程序是正確的，是指這段程序能準(zhǔn)確無(wú)誤地完成預(yù)定的功

2、能?；蛘哒f(shuō)，對(duì)任何一組允許的輸入，程序執(zhí)行后能得到一組相應(yīng)的正確的輸出。 在研究程序正確性證明時(shí)，將一段程序的輸入和輸出應(yīng)滿足的條件的邏輯關(guān)系式分別稱為此段程序的輸入斷言（或初始斷言、前置斷言）和輸出斷言（或結(jié)果斷言、后置斷言），通常用謂詞(x)和(x，z)表示，其中x和z分別表示輸入和輸出數(shù)據(jù)（可以是一個(gè)或一組變量）。第3頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵例子 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,

3、y,z):z=yx。 第4頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵程序正確性三種類型 程序的部分正確性 程序的終止性 程序的完全正確性 第5頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵程序的部分正確性 若每一個(gè)使得（x）為真且程序計(jì)算終止的輸入數(shù)據(jù)x，（x，p（x）都為真，則稱程序p關(guān)于和是部分正確的。 這里p（x）表示與輸入數(shù)據(jù)x相對(duì)應(yīng)的程序p的輸出數(shù)據(jù)。第6頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵程序的終止性 若每一個(gè)使得（x）為真的輸入數(shù)據(jù)x，程序計(jì)算都終止，則稱程序P對(duì)是終止的。 第7頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵程序的完全正確性 若每一個(gè)使得（x

4、）為真的輸入數(shù)據(jù)x，程序計(jì)算都終止且（x，P（x）為真，則稱程序P關(guān)于和是完全正確的。 顯然，一個(gè)程序是完全正確的等價(jià)于該程序是部分正確的同時(shí)又是終止的。 第8頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵程序正確性證明方法 FLOYD的不變式斷言法（證明部分正確性） FLOYD良序集方法（證明終止性） Hoare的公理化方法（證明部分正確性）及其推廣（證明完全正確性） Dijstra的弱謂詞置換法（證明完全正確性） 第9頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵7.9.2 Floyd不變式斷言法 建立斷言 一個(gè)程序除了需要建立輸入/輸出斷言外，如程序中出現(xiàn)循環(huán)，還要建立相應(yīng)于該循環(huán)的

5、不變式斷言，稱之為循環(huán)不變式斷言。所謂循環(huán)不變式斷言，是在循環(huán)中選一個(gè)斷點(diǎn)，在斷點(diǎn)處建立一個(gè)適當(dāng)?shù)臄嘌?，使循環(huán)每次執(zhí)行到斷點(diǎn)時(shí)，斷言都為真。 建立檢驗(yàn)條件 所謂檢驗(yàn)條件就是程序運(yùn)行通過(guò)某通路時(shí)應(yīng)滿足的條件。 證明檢驗(yàn)條件 證明上面給定的所有檢驗(yàn)條件，如果每一條通路的檢驗(yàn)條件都為真，則該程序是部分正確的。第10頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵例子 設(shè)x1，x2是正整數(shù)，求最大公約數(shù)Z=gcd（x1，x2），其流程圖如下圖所示。試證明它的部分正確性。 第11頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵建立斷言 輸入斷言（x）：x10 x20 輸出斷言（x，z）：z=gcd（x1

6、，x2） 在斷點(diǎn)B建立不變式斷言P（x，y）： x10 x20y10y20gcd（y1，y2）=gcd（x1，x2）這里，約定所有變量均為整型，且x表示（x1，x2），y表示（y1，y2）。第12頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵建立檢驗(yàn)條件 選擇B為斷點(diǎn)，則程序的執(zhí)行通路為：Path1：ABPath2：BDBPath3：BEBPath4：BGC 對(duì)每條通路可建立相應(yīng)的檢驗(yàn)條件。第13頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵檢驗(yàn)條件表示設(shè)通路i的輸入/輸出斷言分別為i（x,y）和i（x，y），而通過(guò)此通路的條件為Ri(x,y)，通過(guò)此通路后y的值變?yōu)閞i(x,y)，則應(yīng)有

7、檢驗(yàn)條件： i（x，y）Ri（x，y）i（x，ri（x，y） 其中，y表示程序執(zhí)行中的一組中間變量，x是輸入量。符號(hào)表示蘊(yùn)涵邏輯關(guān)系。第14頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵Path1檢驗(yàn)條件 1（x，y）為（x）；R1（x，y）恒真，即無(wú)條件通過(guò)； 1（x，y）為P（x，y）；通過(guò)此通路后y的值取值x。 故有：（x）P（x，x），即 x10 x20 x10 x20 x10 x20gcd（x1，x2）=gcd（x1，x2）其它路徑的檢驗(yàn)條件（略）第15頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵證明檢驗(yàn)條件 對(duì)任意正整數(shù)y1和y2有如下關(guān)系： 1若y1y2則gcd(y1,y2

8、)=gcd(y1-y2,y2)； 2若y2y1則gcd(y1,y2)=gcd(y1,y2-y1)； 3若y1=y2則gcd(y1,y2)=y1=y2。 對(duì)于Path1，其檢驗(yàn)條件顯然是成立的； 其它（略）第16頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵7.9.3 Floyd良序集方法 如果一個(gè)非空集合W關(guān)于二元關(guān)系-是良序的，則集合W應(yīng)滿足：W為具有關(guān)系-的偏序集。 即關(guān)系-滿足下列性質(zhì)： 1傳遞性，即對(duì)一切a，b，cW，如果a-b，b-c則有a-c。 2反對(duì)稱性，即對(duì)一切a，bW，如果a-b，則有b-a。 3反自反性，即對(duì)一切aW，a - a1 - a2 - 其中a0，a1，a2,.W

9、。 第17頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵證明步驟 設(shè)程序P的輸入斷言為（x），良序集法證明P關(guān)于（x）是終止的證明步驟 （1）選取一個(gè)點(diǎn)集合截?cái)喑绦虻母鱾€(gè)循環(huán)部分，在每一個(gè)截?cái)帱c(diǎn)i處建立一個(gè)中間斷言qi（x，y）。 （2）選取一個(gè)良序集（W，- Ej（x，r（x，y）顯然，如果所有的終止條件成立，則程序P一定終止。第18頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵例子 對(duì)任一給定的自然數(shù)X，計(jì)算Z= （即Z等于x的平方根取整）的程序流程圖如圖所示。 X第19頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵截?cái)喑绦虻难h(huán)部分 該程序只有一個(gè)循環(huán)，在B點(diǎn)將循環(huán)斷開，并建立斷點(diǎn)

10、斷言：q（x，y）：y30 y2x第20頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵選取良序集 選取良序集為（N，0，故有x-y2X-（y2+y3）且均屬于集合（N，）中。至此，也就證明了該程序的終止性。第24頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵7.9.4 程序正確性證明的局限性 經(jīng)驗(yàn)表明，程序證明實(shí)現(xiàn)的困難在于尋找程序的循環(huán)結(jié)構(gòu)所蘊(yùn)涵的循環(huán)不變式。 只有當(dāng)程序“做什么”的說(shuō)明能以簡(jiǎn)單的函數(shù)給出時(shí)，才能使用程序正確性證明技術(shù)。而大型問(wèn)題就難以給出這種說(shuō)明。因此，在實(shí)際應(yīng)用中還存在一些問(wèn)題。 所依賴的數(shù)學(xué)基礎(chǔ)太強(qiáng)，用起來(lái)不夠自然，數(shù)學(xué)素質(zhì)不強(qiáng)的人很難接受。另外，證明本身也不能保證

11、無(wú)錯(cuò)。第25頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵7.10 調(diào) 試 q調(diào)試，又稱糾錯(cuò)或排錯(cuò)，是程序測(cè)試后開始的工作，主要任務(wù)是依據(jù)測(cè)試發(fā)現(xiàn)的錯(cuò)誤跡象確定錯(cuò)誤位置和原因，并加以改正。q調(diào)試活動(dòng)由兩部分組成： 確定程序中可疑錯(cuò)誤的確切性質(zhì)和位置。 對(duì)程序（設(shè)計(jì)，編碼）進(jìn)行修改，排除這個(gè)錯(cuò)誤。q調(diào)試是通過(guò)現(xiàn)象，找出原因的一個(gè)思維分析的過(guò)程。第26頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵7.10.1 調(diào)試的步驟 n從錯(cuò)誤的外部表現(xiàn)形式入手，確定程序中出錯(cuò)位置；n研究有關(guān)部分的程序，找出錯(cuò)誤的內(nèi)在原因；n修改設(shè)計(jì)和代碼，以排除這個(gè)錯(cuò)誤；n重復(fù)進(jìn)行暴露了這個(gè)錯(cuò)誤的原始測(cè)試或某些有關(guān)測(cè)試，

12、以確認(rèn)該錯(cuò)誤是否被排除；是否引進(jìn)了新的錯(cuò)誤。n如果所做的修正無(wú)效，則撤消這次改動(dòng)，重復(fù)上述過(guò)程，直到找到一個(gè)有效的解決辦法為止。第27頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵調(diào)試難點(diǎn) 錯(cuò)誤的癥狀和引起錯(cuò)誤的原因可能相隔很遠(yuǎn)，尤其是在高度耦合的程序結(jié)構(gòu)中； 錯(cuò)誤癥狀可能在另一錯(cuò)誤被糾正后消失或暫時(shí)性的消失； 錯(cuò)誤癥狀可能實(shí)際并不是由錯(cuò)誤引起的（如舍入誤差）； 錯(cuò)誤癥狀可能是由不易跟蹤的人工操作引起的； 錯(cuò)誤癥狀可能是和時(shí)間相關(guān)的，而不是處理問(wèn)題； 很難再現(xiàn)產(chǎn)生錯(cuò)誤癥狀的輸入條件； 錯(cuò)誤癥狀可能時(shí)有時(shí)無(wú)（如在軟硬件結(jié)合的嵌入式系統(tǒng)中常常遇到）； 錯(cuò)誤癥狀可能是由于把任務(wù)分布在若干不同處理器

13、上運(yùn)行而造成。 第28頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵7.10.2 調(diào)試的策略之一：猜測(cè)法 該方法通過(guò)分析錯(cuò)誤癥狀，根據(jù)以往經(jīng)驗(yàn)，輔助使用已有的計(jì)算機(jī)工具，猜測(cè)錯(cuò)誤的原因并進(jìn)行定位。可以通過(guò)“在程序中插入打印語(yǔ)句”、“使用注釋或GOTO語(yǔ)句運(yùn)行部分程序”或“調(diào)試工具”等來(lái)實(shí)現(xiàn)該方法。第29頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵跟蹤法 n先分析錯(cuò)誤征兆，確定最先發(fā)現(xiàn)“癥狀”的位置。然后，人工沿程序的控制流程，向回追蹤源程序代碼，直到找到錯(cuò)誤根源或確定錯(cuò)誤產(chǎn)生的范圍。n跟蹤法對(duì)于小程序很有效，往往能把錯(cuò)誤范圍縮小到程序中的一小段代碼；仔細(xì)分析這段代碼不難確定出錯(cuò)的準(zhǔn)確位置

14、。但對(duì)于大程序，由于回溯的路徑數(shù)目較多，回溯會(huì)變得很困難。第30頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵演繹法無(wú)剩余列舉可能的原因排除不會(huì)發(fā)生的原因細(xì)析余下的原因證明假設(shè)糾正錯(cuò)誤收集更多的測(cè)試結(jié)果有剩余不能能 演繹法排錯(cuò)是測(cè)試人員首先根據(jù)已有的測(cè)試用例，設(shè)想及枚舉出所有可能出錯(cuò)的原因做為假設(shè)；然后再用原始測(cè)試數(shù)據(jù)或新的測(cè)試，從中逐個(gè)排除不可能正確的假設(shè)；最后，再用測(cè)試數(shù)據(jù)驗(yàn)證余下的假設(shè)確是出錯(cuò)的原因。第31頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵歸納法 歸納法排錯(cuò)的基本思想是：從一些線索（錯(cuò)誤征兆）著手，通過(guò)分析它們之間的關(guān)系來(lái)找出錯(cuò)誤。收集有關(guān)數(shù)據(jù)組織數(shù)據(jù)研究數(shù)據(jù)間的關(guān)系提出假設(shè)證明假設(shè)糾正錯(cuò)誤能不能能不能第32頁(yè)/共34頁(yè)中南大學(xué) 信息科學(xué)與工程學(xué)院 任勝兵7.10.3 調(diào)試的原則 綜合起來(lái)