第5章軟件驗證技術(5.9-5.10)

第5章軟件驗證技術

(第5.9-5.10節(jié)）武漢紡織大學數(shù)學與計算機學院主要內容程序正確性證明調試武漢紡織大學數(shù)學與計算機學院5.9程序正確性證明

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

所謂一段程序是正確的，是指這段程序能準確無誤地完成預定的功能?；蛘哒f，對任何一組允許的輸入，程序執(zhí)行后能得到一組相應的正確的輸出。在研究程序正確性證明時，將一段程序的輸入和輸出應滿足的條件的邏輯關系式分別稱為此段程序的輸入斷言（或初始斷言、前置斷言）和輸出斷言（或結果斷言、后置斷言），通常用謂詞φ(x)和ψ(x，z)表示，其中x和z分別表示輸入和輸出數(shù)據(jù)（可以是一個或一組變量）。武漢紡織大學數(shù)學與計算機學院例子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。武漢紡織大學數(shù)學與計算機學院程序正確性三種類型程序的部分正確性程序的終止性程序的完全正確性武漢紡織大學數(shù)學與計算機學院程序的部分正確性若每一個使得φ（x）為真且程序計算終止的輸入數(shù)據(jù)x，ψ（x，p（x））都為真，則稱程序p關于φ和ψ是部分正確的。這里p（x）表示與輸入數(shù)據(jù)x相對應的程序p的輸出數(shù)據(jù)。武漢紡織大學數(shù)學與計算機學院程序的終止性若每一個使得φ（x）為真的輸入數(shù)據(jù)x，程序計算都終止，則稱程序P對φ是終止的。武漢紡織大學數(shù)學與計算機學院程序的完全正確性若每一個使得φ（x）為真的輸入數(shù)據(jù)x，程序計算都終止且ψ（x，P（x））為真，則稱程序P關于φ和ψ是完全正確的。顯然，一個程序是完全正確的等價于該程序是部分正確的同時又是終止的。轉到武漢紡織大學數(shù)學與計算機學院程序正確性證明方法FLOYD的不變式斷言法（證明部分正確性）FLOYD良序集方法（證明終止性）Hoare的公理化方法（證明部分正確性）及其推廣（證明完全正確性）Dijstra的弱謂詞置換法（證明完全正確性）武漢紡織大學數(shù)學與計算機學院5.9.2Floyd不變式斷言法

建立斷言

一個程序除了需要建立輸入/輸出斷言外，如程序中出現(xiàn)循環(huán)，還要建立相應于該循環(huán)的不變式斷言，稱之為循環(huán)不變式斷言。所謂循環(huán)不變式斷言，是在循環(huán)中選一個斷點，在斷點處建立一個適當?shù)臄嘌?，使循環(huán)每次執(zhí)行到斷點時，斷言都為真。建立檢驗條件

所謂檢驗條件就是程序運行通過某通路時應滿足的條件。證明檢驗條件

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

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

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

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

選擇B為斷點，則程序的執(zhí)行通路為：Path1：A→BPath2：B→D→BPath3：B→E→BPath4：B→G→C對每條通路可建立相應的檢驗條件。武漢紡織大學數(shù)學與計算機學院檢驗條件表示設通路i的輸入/輸出斷言分別為φi（x,y）和ψi（x，y），而通過此通路的條件為Ri(x,y)，通過此通路后y的值變?yōu)閞i(x,y)，則應有檢驗條件：φi（x，y）∧Ri（x，y）ψi（x，ri（x，y））其中，y表示程序執(zhí)行中的一組中間變量，x是輸入量。符號表示蘊涵邏輯關系。武漢紡織大學數(shù)學與計算機學院Path1檢驗條件φ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）]其它路徑的檢驗條件（略）武漢紡織大學數(shù)學與計算機學院證明檢驗條件

對任意正整數(shù)y1和y2有如下關系：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。

對于Path1，其檢驗條件顯然是成立的；

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

如果一個非空集合W關于二元關系-<是良序的，則集合W應滿足：①W為具有關系-<的偏序集。即關系-<滿足下列性質：1°傳遞性，即對一切a，b，c∈W，如果a-<b，b-<c則有a-<c。2°反對稱性，即對一切a，b∈W，如果a-<b，則有b-<a。3°反自反性，即對一切a∈W，a-<a。②W的每一非空子集都有一個“最小”元素。即不存在由W中的元素構成的無限遞減序列：a0>-a1>-a2>-……其中a0，a1，a2,...∈W。武漢紡織大學數(shù)學與計算機學院證明步驟

設程序P的輸入斷言為φ（x），良序集法證明P關于φ（x）是終止的證明步驟

（1）選取一個點集合截斷程序的各個循環(huán)部分，在每一個截斷點i處建立一個中間斷言qi（x，y）。（2）選取一個良序集（W，-<），在每一個截斷點i處定義一個終止表達式Ei（x，y）。（3）證明所選取的斷言是“良斷言”。即對每一個從程序入口到斷點j的通路α有：φ（x）∧Rα（x，y）qj（x，rα（x，y））成立；而對每一個由斷點i到斷點j的通路α有：qi（x，y）∧Rα（x，y）qj（x，rα（x，y））成立。這里Rα和rα分別表示通過通路α的條件及通過通路α以后變量y的值。另外，在這兩個蘊涵式中省略了全稱量詞xy，以下兩步亦如此。（4）證明終止表達式是“良函數(shù)”。即對每個斷點i有：qi（x，y）Ei（x，y）∈W（5）證明終止條件成立。即對于每一條從斷點i到斷點j，且是某個循環(huán)的一部分的通路α有：qi（x，y）∧Rα（x，y）[Ei（x，y）>-Ej（x，rα（x，y））]顯然，如果所有的終止條件成立，則程序P一定終止。武漢紡織大學數(shù)學與計算機學院例子對任一給定的自然數(shù)X，計算Z=[]（即Z等于x的平方根取整）的程序流程圖如圖所示。

武漢紡織大學數(shù)學與計算機學院截斷程序的循環(huán)部分

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

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

1°對通路A→B（從程序入口點A到截斷點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]顯然,此蘊涵式成立；其它（略）武漢紡織大學數(shù)學與計算機學院證明終止表達式是良函數(shù)

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

即對于斷點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)]由蘊涵式的前項有:y2≤x且y2+y3≤x故x-y2≥0即x-y2∈Nx-(y2+y3)≥0即x-(y2+y3)∈N同時y3>0，故有x-y2〉X-（y2+y3）且均屬于集合（N，〈）中。至此，也就證明了該程序的終止性。武漢紡織大學數(shù)學與計算機學院5.9.4程序正確性證明的局限性

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

試

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

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

武漢紡織大學數(shù)學與計算機學院5.10.2調試的策略之一：猜測法

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

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