第5章軟件驗(yàn)證技術(shù)(5.9-5.10)

第5章軟件驗(yàn)證技術(shù)

(第5.9-5.10節(jié)）武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院主要內(nèi)容程序正確性證明調(diào)試武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院5.9程序正確性證明

測(cè)試可以幫助人們發(fā)現(xiàn)程序中的錯(cuò)誤，但它卻不能證明程序中沒有錯(cuò)誤。早在50年代，圖林（Turing）等人就開始注意并開展了程序正確性證明這方面的早期研究工作；60年代后半期，F(xiàn)loyd和Hoare等人提出了不變式斷言法和公理化方法，使得這一研究進(jìn)入了一個(gè)蓬勃發(fā)展的新階段；在此之后，出現(xiàn)了許多不同的程序正確性證明方法。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院5.9.1程序正確性定義

所謂一段程序是正確的，是指這段程序能準(zhǔn)確無誤地完成預(yù)定的功能?；蛘哒f，對(duì)任何一組允許的輸入，程序執(zhí)行后能得到一組相應(yīng)的正確的輸出。在研究程序正確性證明時(shí)，將一段程序的輸入和輸出應(yīng)滿足的條件的邏輯關(guān)系式分別稱為此段程序的輸入斷言（或初始斷言、前置斷言）和輸出斷言（或結(jié)果斷言、后置斷言），通常用謂詞φ(x)和ψ(x，z)表示，其中x和z分別表示輸入和輸出數(shù)據(jù)（可以是一個(gè)或一組變量）。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院例子unsignedpower(unsignedx,unsignedy){unsignedz;z=1;while(x!=0){z=z*y;x=x-1;}returnz;}則φ(x,y):x≥0,y＞0；ψ(x,y,z):z=yx。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院程序正確性三種類型程序的部分正確性程序的終止性程序的完全正確性武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院程序的部分正確性若每一個(gè)使得φ（x）為真且程序計(jì)算終止的輸入數(shù)據(jù)x，ψ（x，p（x））都為真，則稱程序p關(guān)于φ和ψ是部分正確的。這里p（x）表示與輸入數(shù)據(jù)x相對(duì)應(yīng)的程序p的輸出數(shù)據(jù)。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院程序的終止性若每一個(gè)使得φ（x）為真的輸入數(shù)據(jù)x，程序計(jì)算都終止，則稱程序P對(duì)φ是終止的。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院程序的完全正確性若每一個(gè)使得φ（x）為真的輸入數(shù)據(jù)x，程序計(jì)算都終止且ψ（x，P（x））為真，則稱程序P關(guān)于φ和ψ是完全正確的。顯然，一個(gè)程序是完全正確的等價(jià)于該程序是部分正確的同時(shí)又是終止的。轉(zhuǎn)到武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院程序正確性證明方法FLOYD的不變式斷言法（證明部分正確性）FLOYD良序集方法（證明終止性）Hoare的公理化方法（證明部分正確性）及其推廣（證明完全正確性）Dijstra的弱謂詞置換法（證明完全正確性）武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院5.9.2Floyd不變式斷言法

建立斷言

一個(gè)程序除了需要建立輸入/輸出斷言外，如程序中出現(xiàn)循環(huán)，還要建立相應(yīng)于該循環(huán)的不變式斷言，稱之為循環(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)行通過某通路時(shí)應(yīng)滿足的條件。證明檢驗(yàn)條件

證明上面給定的所有檢驗(yàn)條件，如果每一條通路的檢驗(yàn)條件都為真，則該程序是部分正確的。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院例子設(shè)x1，x2是正整數(shù)，求最大公約數(shù)Z=gcd（x1，x2），其流程圖如下圖所示。試證明它的部分正確性。

武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院建立斷言

輸入斷言φ（x）：x1＞0∧x2＞0輸出斷言ψ（x，z）：z=gcd（x1，x2）在斷點(diǎn)B建立不變式斷言P（x，y）：

x1＞0∧x2＞0∧y1＞0∧y2＞0∧gcd（y1，y2）=gcd（x1，x2）這里，約定所有變量均為整型，且x表示（x1，x2），y表示（y1，y2）。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院建立檢驗(yàn)條件

選擇B為斷點(diǎn)，則程序的執(zhí)行通路為：Path1：A→BPath2：B→D→BPath3：B→E→BPath4：B→G→C對(duì)每條通路可建立相應(yīng)的檢驗(yàn)條件。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院檢驗(yàn)條件表示設(shè)通路i的輸入/輸出斷言分別為φi（x,y）和ψi（x，y），而通過此通路的條件為Ri(x,y)，通過此通路后y的值變?yōu)閞i(x,y)，則應(yīng)有檢驗(yàn)條件：φi（x，y）∧Ri（x，y）ψi（x，ri（x，y））其中，y表示程序執(zhí)行中的一組中間變量，x是輸入量。符號(hào)表示蘊(yùn)涵邏輯關(guān)系。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院Path1檢驗(yàn)條件φ1（x，y）為φ（x）；R1（x，y）恒真，即無條件通過；ψ1（x，y）為P（x，y）；通過此通路后y的值取值x。故有：φ（x）P（x，x），即[x1＞0∧x2＞0][x1＞0∧x2＞0∧x1＞0∧x2＞0∧gcd（x1，x2）=gcd（x1，x2）]其它路徑的檢驗(yàn)條件（略）武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院證明檢驗(yàn)條件

對(duì)任意正整數(shù)y1和y2有如下關(guān)系：1°若y1>y2則gcd(y1,y2)=gcd(y1-y2,y2)；2°若y2>y1則gcd(y1,y2)=gcd(y1,y2-y1)；3°若y1=y2則gcd(y1,y2)=y1=y2。

對(duì)于Path1，其檢驗(yàn)條件顯然是成立的；

其它（略）武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院5.9.3Floyd良序集方法

如果一個(gè)非空集合W關(guān)于二元關(guān)系-<是良序的，則集合W應(yīng)滿足：①W為具有關(guān)系-<的偏序集。即關(guān)系-<滿足下列性質(zhì)：1°傳遞性，即對(duì)一切a，b，c∈W，如果a-<b，b-<c則有a-<c。2°反對(duì)稱性，即對(duì)一切a，b∈W，如果a-<b，則有b-<a。3°反自反性，即對(duì)一切a∈W，a-<a。②W的每一非空子集都有一個(gè)“最小”元素。即不存在由W中的元素構(gòu)成的無限遞減序列：a0>-a1>-a2>-……其中a0，a1，a2,...∈W。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(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，-<），在每一個(gè)截?cái)帱c(diǎn)i處定義一個(gè)終止表達(dá)式Ei（x，y）。（3）證明所選取的斷言是“良斷言”。即對(duì)每一個(gè)從程序入口到斷點(diǎn)j的通路α有：φ（x）∧Rα（x，y）qj（x，rα（x，y））成立；而對(duì)每一個(gè)由斷點(diǎn)i到斷點(diǎn)j的通路α有：qi（x，y）∧Rα（x，y）qj（x，rα（x，y））成立。這里Rα和rα分別表示通過通路α的條件及通過通路α以后變量y的值。另外，在這兩個(gè)蘊(yùn)涵式中省略了全稱量詞xy，以下兩步亦如此。（4）證明終止表達(dá)式是“良函數(shù)”。即對(duì)每個(gè)斷點(diǎn)i有：qi（x，y）Ei（x，y）∈W（5）證明終止條件成立。即對(duì)于每一條從斷點(diǎn)i到斷點(diǎn)j，且是某個(gè)循環(huán)的一部分的通路α有：qi（x，y）∧Rα（x，y）[Ei（x，y）>-Ej（x，rα（x，y））]顯然，如果所有的終止條件成立，則程序P一定終止。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院例子對(duì)任一給定的自然數(shù)X，計(jì)算Z=[]（即Z等于x的平方根取整）的程序流程圖如圖所示。

武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院截?cái)喑绦虻难h(huán)部分

該程序只有一個(gè)循環(huán)，在B點(diǎn)將循環(huán)斷開，并建立斷點(diǎn)斷言：q（x，y）：y3＞0∧y2≤x武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院選取良序集

選取良序集為（N，<），N為自然數(shù)集合。定義B點(diǎn)的終止表達(dá)式為：E（x，y）：x-y2武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院證明所選取的斷言是“良斷言”

1°對(duì)通路A→B（從程序入口點(diǎn)A到截?cái)帱c(diǎn)B）有：φ（x）∧RA→B（x，y）q（x，rA→B（x，y））顯然RA→B（x，y）恒為真，即走A→B的條件恒真；rA→B（x，y）為（0，0，1），即y的值通過A→B后變?yōu)?0,0,1)。y表示（y1,y2,y3）。故有φ（x）q（x，0，0，1）即x≥0[1＞0∧0≤x]顯然,此蘊(yùn)涵式成立；其它（略）武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院證明終止表達(dá)式是良函數(shù)

即證明：q（x，y）E（x，y）∈N即[y3＞0∧y2≤x]x-y2≥0x-y2∈N此蘊(yùn)涵式顯然也成立。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院證明終止條件成立

即對(duì)于斷點(diǎn)B到斷B的通路（B→C→D→B）有：q（x，y）∧RB→C→D→B（x，y）[E（x，y）＞E（x，rB→C→D→B（x，y））]即：[y3＞0∧y2≤x∧y2+y3≤x][x-y2＞x-(y2+y3)]由蘊(yùn)涵式的前項(xiàng)有:y2≤x且y2+y3≤x故x-y2≥0即x-y2∈Nx-(y2+y3)≥0即x-(y2+y3)∈N同時(shí)y3>0，故有x-y2〉X-（y2+y3）且均屬于集合（N，〈）中。至此，也就證明了該程序的終止性。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院5.9.4程序正確性證明的局限性

經(jīng)驗(yàn)表明，程序證明實(shí)現(xiàn)的困難在于尋找程序的循環(huán)結(jié)構(gòu)所蘊(yùn)涵的循環(huán)不變式。只有當(dāng)程序“做什么”的說明能以簡(jiǎn)單的函數(shù)給出時(shí)，才能使用程序正確性證明技術(shù)。而大型問題就難以給出這種說明。因此，在實(shí)際應(yīng)用中還存在一些問題。所依賴的數(shù)學(xué)基礎(chǔ)太強(qiáng)，用起來不夠自然，數(shù)學(xué)素質(zhì)不強(qiáng)的人很難接受。另外，證明本身也不能保證無錯(cuò)。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院補(bǔ)充：集成測(cè)試文檔集成測(cè)試文檔即測(cè)試說明書（testspecifications）應(yīng)給出集成的總體規(guī)劃和某些特殊測(cè)試的描述。它將作為軟件配置的一部分提交給用戶。測(cè)試說明書的主要內(nèi)容提綱如下：武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院測(cè)試說明書的主要內(nèi)容提綱1）測(cè)試范圍2）測(cè)試計(jì)劃A．測(cè)試的各個(gè)階段和劃分模塊群情況B．進(jìn)度安排C．開銷軟件（驅(qū)動(dòng)和樁模塊）D．環(huán)境和資源武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院3）各個(gè)模塊群測(cè)試過程的描述，包括：A．集成的順序①用途②被測(cè)模式B．模塊群中各模塊單元測(cè)試的情況①模塊的測(cè)試描述②開銷軟件描述③期望的結(jié)果武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院C．測(cè)試環(huán)境①特殊工具和技術(shù)②開銷軟件的描述D．測(cè)試用例E．模塊群的期望結(jié)果等4）實(shí)際測(cè)試結(jié)果5）參考文獻(xiàn)6）附錄。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院5.10調(diào)

試

調(diào)試，又稱糾錯(cuò)或排錯(cuò)，是程序測(cè)試后開始的工作，主要任務(wù)是依據(jù)測(cè)試發(fā)現(xiàn)的錯(cuò)誤跡象確定錯(cuò)誤位置和原因，并加以改正。調(diào)試活動(dòng)由兩部分組成：①確定程序中可疑錯(cuò)誤的確切性質(zhì)和位置。②對(duì)程序（設(shè)計(jì)，編碼）進(jìn)行修改，排除這個(gè)錯(cuò)誤。調(diào)試是通過現(xiàn)象，找出原因的一個(gè)思維分析的過程。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院執(zhí)行測(cè)試用例測(cè)試用例結(jié)果評(píng)估附加測(cè)試被懷疑的原因已識(shí)別的原因糾正回歸測(cè)試測(cè)試過程武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院5.10.1調(diào)試的步驟

從錯(cuò)誤的外部表現(xiàn)形式入手，確定程序中出錯(cuò)位置；研究有關(guān)部分的程序，找出錯(cuò)誤的內(nèi)在原因；修改設(shè)計(jì)和代碼，以排除這個(gè)錯(cuò)誤；重復(fù)進(jìn)行暴露了這個(gè)錯(cuò)誤的原始測(cè)試或某些有關(guān)測(cè)試，以確認(rèn)該錯(cuò)誤是否被排除；是否引進(jìn)了新的錯(cuò)誤。如果所做的修正無效，則撤消這次改動(dòng)，重復(fù)上述過程，直到找到一個(gè)有效的解決辦法為止。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院調(diào)試難點(diǎn)錯(cuò)誤的癥狀和引起錯(cuò)誤的原因可能相隔很遠(yuǎn)，尤其是在高度耦合的程序結(jié)構(gòu)中；錯(cuò)誤癥狀可能在另一錯(cuò)誤被糾正后消失或暫時(shí)性的消失；錯(cuò)誤癥狀可能實(shí)際并不是由錯(cuò)誤引起的（如舍入誤差）；錯(cuò)誤癥狀可能是由不易跟蹤的人工操作引起的；錯(cuò)誤癥狀可能是和時(shí)間相關(guān)的，而不是處理問題；很難再現(xiàn)產(chǎn)生錯(cuò)誤癥狀的輸入條件；錯(cuò)誤癥狀可能時(shí)有時(shí)無（如在軟硬件結(jié)合的嵌入式系統(tǒng)中常常遇到）；錯(cuò)誤癥狀可能是由于把任務(wù)分布在若干不同處理器上運(yùn)行而造成。

武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院5.10.2調(diào)試的策略之一：猜測(cè)法

該方法通過分析錯(cuò)誤癥狀，根據(jù)以往經(jīng)驗(yàn)，輔助使用已有的計(jì)算機(jī)工具，猜測(cè)錯(cuò)誤的原因并進(jìn)行定位。可以通過“在程序中插入打印語句”、“使用注釋或GOTO語句運(yùn)行部分程序”或“調(diào)試工具”等來實(shí)現(xiàn)該方法。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院跟蹤法

先分析錯(cuò)誤征兆，確定最先發(fā)現(xiàn)“癥狀”的位置。然后，人工沿程序的控制流程，向回追蹤源程序代碼，直到找到錯(cuò)誤根源或確定錯(cuò)誤產(chǎn)生的范圍。跟蹤法對(duì)于小程序很有效，往往能把錯(cuò)誤范圍縮小到程序中的一小段代碼；仔細(xì)分析這段代碼不難確定出錯(cuò)的準(zhǔn)確位置。但對(duì)于大程序，由于回溯的路徑數(shù)目較多，回溯會(huì)變得很困難。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院演繹法演繹法排錯(cuò)是測(cè)試人員首先根據(jù)已有的測(cè)試用例，設(shè)想及枚舉出所有可能出錯(cuò)的原因做為假設(shè)；然后再用原始測(cè)試數(shù)據(jù)或新的測(cè)試，從中逐個(gè)排除不可能正確的假設(shè)；最后，再用測(cè)試數(shù)據(jù)驗(yàn)證余下的假設(shè)確是出錯(cuò)的原因。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院列舉可能的原因排除不正確的假設(shè)精化余下的假設(shè)證明假設(shè)收集更多數(shù)據(jù)糾正錯(cuò)誤有剩余能不能無剩余演繹法：普通特殊從假設(shè)中逐步排除、精化，從而導(dǎo)出錯(cuò)誤根源。武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院列舉所有可能出錯(cuò)原因的假設(shè)：把所有可能的錯(cuò)誤原因列成表。進(jìn)而可以組織、分析現(xiàn)有數(shù)據(jù)。利用已有的測(cè)試數(shù)據(jù)，排除不正確的假設(shè)：仔細(xì)分析已有的數(shù)據(jù)，尋找矛盾，力求排除前一步列出所有原因。如果所有原因都被排除了，則需要補(bǔ)充一些數(shù)據(jù)(測(cè)試用例)，以建立新的假設(shè)。改進(jìn)余下的假設(shè)：利用已知的線索，進(jìn)一步改進(jìn)余下的假設(shè)，使之更具體化，以便可以精確地確定出錯(cuò)位置。證明余下的假設(shè)武漢紡織大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院歸納法歸納法排錯(cuò)的基本思想是：從一些線索（錯(cuò)誤征兆）著手，通過分析它們之間的