第3章_程序的正確性證明

1、第三章第三章 程序的正確性證明程序的正確性證明 主要內(nèi)容主要內(nèi)容程序的測試程序的測試Floyd-Hoare規(guī)則公理方法規(guī)則公理方法Dijkstra 最弱前置條件方法最弱前置條件方法程序的正確性程序的正確性所謂一段程序是正確的，是指這段程序能準(zhǔn)確無誤所謂一段程序是正確的，是指這段程序能準(zhǔn)確無誤地完成編寫者所期望賦予它的功能。地完成編寫者所期望賦予它的功能?；蛘哒f，對任何一組允許的輸入信息，程序執(zhí)行后能或者說，對任何一組允許的輸入信息，程序執(zhí)行后能得到一組和這組輸入信息相對應(yīng)的正確的輸出信息。得到一組和這組輸入信息相對應(yīng)的正確的輸出信息。通俗地說，通俗地說，“做了它該做的事，沒有做它不該做的做了它

2、該做的事，沒有做它不該做的事事”一段程序是錯(cuò)誤的，是指：一段程序是錯(cuò)誤的，是指：（1 1）程序完成的事情并不是程序員想要完成的事）程序完成的事情并不是程序員想要完成的事情；情；（2 2）程序員想要程序完成的事情，程序并沒有完）程序員想要程序完成的事情，程序并沒有完成。成。一般來說，程序中含有錯(cuò)誤是很難避免的。一般來說，程序中含有錯(cuò)誤是很難避免的。錯(cuò)誤可能有：錯(cuò)誤可能有：（1 1）設(shè)計(jì)時(shí)的錯(cuò)誤；）設(shè)計(jì)時(shí)的錯(cuò)誤；（2 2）程序編寫時(shí)的錯(cuò)誤；）程序編寫時(shí)的錯(cuò)誤；（3 3）運(yùn)行時(shí)的錯(cuò)誤等。）運(yùn)行時(shí)的錯(cuò)誤等。發(fā)現(xiàn)錯(cuò)誤或盡量減少錯(cuò)誤，是程序設(shè)計(jì)人員的努力發(fā)現(xiàn)錯(cuò)誤或盡量減少錯(cuò)誤，是程序設(shè)計(jì)人員的努力方向，更

3、是其職責(zé)。方向，更是其職責(zé)。如何保證程序的正確性如何保證程序的正確性要求要求1 1、從編程時(shí)就應(yīng)該盡量地避免和減少錯(cuò)誤的發(fā)生、從編程時(shí)就應(yīng)該盡量地避免和減少錯(cuò)誤的發(fā)生2 2、當(dāng)程序編好后要盡量找出錯(cuò)誤，糾正錯(cuò)誤、當(dāng)程序編好后要盡量找出錯(cuò)誤，糾正錯(cuò)誤避免錯(cuò)誤的方法避免錯(cuò)誤的方法 1 1、程序的結(jié)構(gòu)要簡單、程序的結(jié)構(gòu)要簡單 2 2、采用標(biāo)準(zhǔn)的軟件設(shè)計(jì)工具、標(biāo)準(zhǔn)的算法手冊以及有效、采用標(biāo)準(zhǔn)的軟件設(shè)計(jì)工具、標(biāo)準(zhǔn)的算法手冊以及有效的程序設(shè)計(jì)方法的程序設(shè)計(jì)方法發(fā)現(xiàn)錯(cuò)誤的方法發(fā)現(xiàn)錯(cuò)誤的方法 1 1、利用測試工具、利用測試工具: :跟蹤程序的運(yùn)行，用測試的辦法去查找跟蹤程序的運(yùn)行，用測試的辦法去查找并發(fā)現(xiàn)程序

4、錯(cuò)誤；并發(fā)現(xiàn)程序錯(cuò)誤； 2 2、利用程序的驗(yàn)證系統(tǒng)：證明程序的正確性。、利用程序的驗(yàn)證系統(tǒng)：證明程序的正確性。程序測試：給程序一組或幾組初始值進(jìn)行試運(yùn)行，程序測試：給程序一組或幾組初始值進(jìn)行試運(yùn)行，將運(yùn)行的結(jié)果與實(shí)現(xiàn)已知的結(jié)果比較，若兩則相將運(yùn)行的結(jié)果與實(shí)現(xiàn)已知的結(jié)果比較，若兩則相同，則認(rèn)為程序是正確的，若兩則不同，則說明程同，則認(rèn)為程序是正確的，若兩則不同，則說明程序有錯(cuò)誤。序有錯(cuò)誤。一、程序測試一、程序測試程序測試程序測試19831983年年IEEEIEEE提出的軟件工程術(shù)語中給軟件測試下的定提出的軟件工程術(shù)語中給軟件測試下的定義是：義是：“使用人工或者自動(dòng)手段來運(yùn)行或測定某個(gè)系使用人工或

5、者自動(dòng)手段來運(yùn)行或測定某個(gè)系統(tǒng)的過程，其目的在于檢驗(yàn)它是否滿足規(guī)定的需求或統(tǒng)的過程，其目的在于檢驗(yàn)它是否滿足規(guī)定的需求或是弄清預(yù)期結(jié)果與實(shí)際結(jié)果之間的差別。是弄清預(yù)期結(jié)果與實(shí)際結(jié)果之間的差別?！睖y試是程序的執(zhí)行過程，目的測試是程序的執(zhí)行過程，目的在于發(fā)現(xiàn)錯(cuò)誤在于發(fā)現(xiàn)錯(cuò)誤。一個(gè)好的測試用例在于能發(fā)現(xiàn)至今未發(fā)現(xiàn)的錯(cuò)誤；一個(gè)好的測試用例在于能發(fā)現(xiàn)至今未發(fā)現(xiàn)的錯(cuò)誤； 一個(gè)成功的測試是發(fā)現(xiàn)了至今未發(fā)現(xiàn)的錯(cuò)誤的測一個(gè)成功的測試是發(fā)現(xiàn)了至今未發(fā)現(xiàn)的錯(cuò)誤的測試。試。測試的原則1. 應(yīng)當(dāng) “盡早地和不斷地進(jìn)行軟件測試” 。2. 測試用例應(yīng)由測試輸入數(shù)據(jù)和對應(yīng)的預(yù)期輸出結(jié)果組成。3. 程序員應(yīng)避免檢查自己的程序。

6、4. 在設(shè)計(jì)測試用例時(shí)，應(yīng)當(dāng)包括合理的輸入條件和不合理的輸入條件。5. 充分注意測試中的群集現(xiàn)象。即測試后程序中殘存的錯(cuò)誤數(shù)目與該程序中已發(fā)現(xiàn)的錯(cuò)誤數(shù)目成正比。6. 嚴(yán)格執(zhí)行測試計(jì)劃，排除測試的隨意性。7. 應(yīng)當(dāng)對每一個(gè)測試結(jié)果做全面檢查。8. 妥善保存測試計(jì)劃，測試用例，出錯(cuò)統(tǒng)計(jì)和最終分析報(bào)告，為維護(hù)提供方便。程序測試實(shí)質(zhì)上只是一種抽樣檢查程序測試實(shí)質(zhì)上只是一種抽樣檢查測試過程：測試過程： 選取測試數(shù)據(jù)選取測試數(shù)據(jù) 執(zhí)行程序執(zhí)行程序 輸入輸入測試數(shù)據(jù)測試數(shù)據(jù) 記錄執(zhí)行結(jié)果記錄執(zhí)行結(jié)果 手工核對結(jié)果手工核對結(jié)果 因此，測試只是一種查錯(cuò)的手段，它可以幫助人們因此，測試只是一種查錯(cuò)的手段，它可以幫

7、助人們?nèi)グl(fā)現(xiàn)程序中的錯(cuò)誤，但不能證明程序中沒有錯(cuò)去發(fā)現(xiàn)程序中的錯(cuò)誤，但不能證明程序中沒有錯(cuò)誤，即：誤，即：測試不能證明程序是正確的測試不能證明程序是正確的 程序測試的過程程序測試的過程軟件測試方法軟件測試方法軟件測試的方法和技術(shù)是多種多樣的。對于軟件測軟件測試的方法和技術(shù)是多種多樣的。對于軟件測試技術(shù)，根據(jù)不同角度，可以將測試方法分為不同試技術(shù)，根據(jù)不同角度，可以將測試方法分為不同種類。種類。（1）從是否需要執(zhí)行被測軟件的角度，可以分為）從是否需要執(zhí)行被測軟件的角度，可以分為靜靜態(tài)測試態(tài)測試和和動(dòng)態(tài)測試動(dòng)態(tài)測試；（2）從測試是否針對系統(tǒng)內(nèi)部結(jié)構(gòu)和具體實(shí)現(xiàn)算法）從測試是否針對系統(tǒng)內(nèi)部結(jié)構(gòu)和具體實(shí)

8、現(xiàn)算法的角度，可以分為的角度，可以分為白盒測試白盒測試和和黑盒測試黑盒測試；（3）從實(shí)際測試的前后過程來看，軟件測試是由一）從實(shí)際測試的前后過程來看，軟件測試是由一系列的不同測試組成，這些步驟可以分為：系列的不同測試組成，這些步驟可以分為：單元測單元測試試、組裝測試（集成測試）組裝測試（集成測試）、確認(rèn)測試確認(rèn)測試和和系統(tǒng)測系統(tǒng)測試試。兩種重要的軟件測試方法兩種重要的軟件測試方法 黑盒測試黑盒測試這種方法是把測試對象看做一個(gè)黑盒子，測試人員完這種方法是把測試對象看做一個(gè)黑盒子，測試人員完全不考慮程序內(nèi)部的邏輯結(jié)構(gòu)和內(nèi)部特性，只依據(jù)程全不考慮程序內(nèi)部的邏輯結(jié)構(gòu)和內(nèi)部特性，只依據(jù)程序的需求規(guī)格說明

9、書，檢查程序的功能是否符合它的序的需求規(guī)格說明書，檢查程序的功能是否符合它的功能說明。功能說明。黑盒測試又叫做黑盒測試又叫做功能測試功能測試或或數(shù)據(jù)驅(qū)動(dòng)測試數(shù)據(jù)驅(qū)動(dòng)測試。 白盒測試白盒測試此方法把測試對象看做一個(gè)透明的盒子，它允許測試此方法把測試對象看做一個(gè)透明的盒子，它允許測試人員利用程序內(nèi)部的邏輯結(jié)構(gòu)及有關(guān)信息，設(shè)計(jì)或選人員利用程序內(nèi)部的邏輯結(jié)構(gòu)及有關(guān)信息，設(shè)計(jì)或選擇測試用例，對程序所有邏輯路徑進(jìn)行測試。擇測試用例，對程序所有邏輯路徑進(jìn)行測試。通過在不同點(diǎn)檢查程序的狀態(tài)，確定實(shí)際的狀態(tài)是否通過在不同點(diǎn)檢查程序的狀態(tài)，確定實(shí)際的狀態(tài)是否與預(yù)期的狀態(tài)一致。因此白盒測試又稱為與預(yù)期的狀態(tài)一致。因

10、此白盒測試又稱為結(jié)構(gòu)測試結(jié)構(gòu)測試或或邏輯驅(qū)動(dòng)測試邏輯驅(qū)動(dòng)測試。黑盒測試方法是在程序接口上進(jìn)行測試，主要是為了發(fā)現(xiàn)以下黑盒測試方法是在程序接口上進(jìn)行測試，主要是為了發(fā)現(xiàn)以下錯(cuò)誤錯(cuò)誤: : 是否有不正確或遺漏了的功能是否有不正確或遺漏了的功能? ? 在接口上，輸入能否正確地接受在接口上，輸入能否正確地接受? ? 能否輸出正確的結(jié)果能否輸出正確的結(jié)果? ? 是否有數(shù)據(jù)結(jié)構(gòu)錯(cuò)誤或外部信息是否有數(shù)據(jù)結(jié)構(gòu)錯(cuò)誤或外部信息( (例如數(shù)據(jù)文件例如數(shù)據(jù)文件) )訪問錯(cuò)訪問錯(cuò)誤誤? ? 性能上是否能夠滿足要求性能上是否能夠滿足要求? ? 是否有初始化或終止性錯(cuò)誤是否有初始化或終止性錯(cuò)誤? ?用黑盒測試發(fā)現(xiàn)程序中的錯(cuò)

11、誤，必須在所有可能的輸入條件和用黑盒測試發(fā)現(xiàn)程序中的錯(cuò)誤，必須在所有可能的輸入條件和輸出條件中確定測試數(shù)據(jù)，來檢查程序是否都能產(chǎn)生正確的輸輸出條件中確定測試數(shù)據(jù)，來檢查程序是否都能產(chǎn)生正確的輸出。出。但這是不可能的。但這是不可能的。假設(shè)一個(gè)程序假設(shè)一個(gè)程序P P有輸入量有輸入量X X和和Y Y及輸出量及輸出量Z Z。在字長為。在字長為3232位的計(jì)位的計(jì)算機(jī)上運(yùn)行。若算機(jī)上運(yùn)行。若X X、Y Y取整數(shù)，按黑盒方法進(jìn)行窮舉測試：取整數(shù)，按黑盒方法進(jìn)行窮舉測試：可能采用的測試數(shù)據(jù)組：可能采用的測試數(shù)據(jù)組： 2 232322 232322 26464 如果測試一組數(shù)據(jù)需要如果測試一組數(shù)據(jù)需要1 1毫

12、秒，一年工作毫秒，一年工作3653652424小時(shí)，小時(shí)，完成所有測試需完成所有測試需5 5億年。億年。軟件人員使用白盒測試方法，主要想對程序模塊進(jìn)行軟件人員使用白盒測試方法，主要想對程序模塊進(jìn)行如下的檢查：如下的檢查：對程序模塊的所有獨(dú)立的執(zhí)行路徑至少測試一對程序模塊的所有獨(dú)立的執(zhí)行路徑至少測試一次；次；對所有的邏輯判定，取對所有的邏輯判定，取“真真”與取與取“假假”的兩種的兩種情況都至少測試一次；情況都至少測試一次；在循環(huán)的邊界和運(yùn)行界限內(nèi)執(zhí)行循環(huán)體；在循環(huán)的邊界和運(yùn)行界限內(nèi)執(zhí)行循環(huán)體；測試內(nèi)部數(shù)據(jù)結(jié)構(gòu)的有效性；測試內(nèi)部數(shù)據(jù)結(jié)構(gòu)的有效性；對一個(gè)具有多重選擇和循環(huán)嵌套的程序，不同的路徑數(shù)目可

13、能是天文數(shù)字。給出一個(gè)小程序的流程圖，它包括了一個(gè)執(zhí)行20次的循環(huán)。包含的不同執(zhí)行路徑數(shù)達(dá)520條，對每一條路徑進(jìn)行測試需要1毫秒，假定一年工作365 24小時(shí)，要想把所有路徑測試完，需3170年。即使能完成這樣即使能完成這樣的測試，也不意的測試，也不意味差程序沒有錯(cuò)味差程序沒有錯(cuò)誤。如：誤。如：x=x+z,錯(cuò)誤寫成錯(cuò)誤寫成x=x-z,且且當(dāng)當(dāng)z=0時(shí)，這種錯(cuò)時(shí)，這種錯(cuò)誤仍然難以發(fā)誤仍然難以發(fā)現(xiàn)現(xiàn) 。測試常常是不充分的，它只能測試常常是不充分的，它只能發(fā)現(xiàn)某些錯(cuò)誤存在，而不能證發(fā)現(xiàn)某些錯(cuò)誤存在，而不能證明錯(cuò)誤的不存在明錯(cuò)誤的不存在 。黑盒測試黑盒測試 等價(jià)類劃分 邊界值分析 錯(cuò)誤推測法 因果圖

14、例子例子 某個(gè)某個(gè)TRIANGLETRIANGLE程序，用程序，用3 3個(gè)整數(shù)表示一個(gè)三角個(gè)整數(shù)表示一個(gè)三角形的形的3 3條邊長。當(dāng)輸入條邊長。當(dāng)輸入3 3個(gè)整數(shù)后，該程序輸出一個(gè)整數(shù)后，該程序輸出一個(gè)結(jié)果，指出這三角形是等腰，等邊，還是不等個(gè)結(jié)果，指出這三角形是等腰，等邊，還是不等邊三角形。邊三角形。這個(gè)例子只知程序的功能，而不知內(nèi)部的邏輯與結(jié)這個(gè)例子只知程序的功能，而不知內(nèi)部的邏輯與結(jié)構(gòu)。在選擇數(shù)據(jù)組來測試程序時(shí)，我們可以憑經(jīng)構(gòu)。在選擇數(shù)據(jù)組來測試程序時(shí)，我們可以憑經(jīng)驗(yàn)，考慮如下情況：驗(yàn)，考慮如下情況：1 1）合理構(gòu)成等腰三角形）合理構(gòu)成等腰三角形2 2）合理構(gòu)成等邊三角形）合理構(gòu)成等邊三

15、角形3 3）合理構(gòu)成不等邊三角形）合理構(gòu)成不等邊三角形4 4）等腰三角形的三種排列）等腰三角形的三種排列5 5）三個(gè)正數(shù)，其中兩個(gè)數(shù)之和等于第三個(gè)數(shù)）三個(gè)正數(shù)，其中兩個(gè)數(shù)之和等于第三個(gè)數(shù)6 6）兩邊之和等于第三邊的三種排列）兩邊之和等于第三邊的三種排列7 7）三個(gè)正數(shù)，其中兩個(gè)數(shù)之和小于第三個(gè)數(shù)）三個(gè)正數(shù)，其中兩個(gè)數(shù)之和小于第三個(gè)數(shù)8 8）兩邊之和小于第三邊的三種排列）兩邊之和小于第三邊的三種排列9）輸入三個(gè)數(shù)，其中含有）輸入三個(gè)數(shù)，其中含有010）輸入三個(gè)數(shù)，其中含有負(fù)數(shù)）輸入三個(gè)數(shù)，其中含有負(fù)數(shù)11）輸入三個(gè)數(shù)，其中含有非整數(shù)值）輸入三個(gè)數(shù)，其中含有非整數(shù)值12）輸入三個(gè)均為）輸入三個(gè)均為

16、0的數(shù)的數(shù)13）輸入三個(gè)均為非法字符）輸入三個(gè)均為非法字符列出各種產(chǎn)生的情況來測試的方法顯然是黑盒子列出各種產(chǎn)生的情況來測試的方法顯然是黑盒子方法。它不關(guān)心盒子內(nèi)程序的具體邏輯，只是根方法。它不關(guān)心盒子內(nèi)程序的具體邏輯，只是根據(jù)程序功能來設(shè)計(jì)測試用例據(jù)程序功能來設(shè)計(jì)測試用例等價(jià)類劃分等價(jià)類劃分 有效等價(jià)類：是指對于程序的規(guī)格說明來說，是合理的，有效等價(jià)類：是指對于程序的規(guī)格說明來說，是合理的，有意義的輸入數(shù)據(jù)構(gòu)成的集合。有意義的輸入數(shù)據(jù)構(gòu)成的集合。 無效等價(jià)類：是指對于程序的規(guī)格說明來說，是不合理無效等價(jià)類：是指對于程序的規(guī)格說明來說，是不合理的，無意義的輸入數(shù)據(jù)構(gòu)成的集合。的，無意義的輸入數(shù)

17、據(jù)構(gòu)成的集合。 例如，在程序的規(guī)格說明中，對輸入條件有一句話：例如，在程序的規(guī)格說明中，對輸入條件有一句話： “ 項(xiàng)數(shù)可以從項(xiàng)數(shù)可以從1到到999 ” ，則，則有效等價(jià)類是有效等價(jià)類是“1項(xiàng)數(shù)項(xiàng)數(shù)999”兩個(gè)無效等價(jià)類是兩個(gè)無效等價(jià)類是“項(xiàng)數(shù)項(xiàng)數(shù)1”或或“項(xiàng)數(shù)項(xiàng)數(shù)999”。在數(shù)軸上表示成在數(shù)軸上表示成: 邊界值分析邊界值分析人們從長期的測試工作經(jīng)驗(yàn)得知，人們從長期的測試工作經(jīng)驗(yàn)得知，大量的錯(cuò)誤是發(fā)生在輸大量的錯(cuò)誤是發(fā)生在輸入或輸出范圍的邊界上，而不是在輸入范圍的內(nèi)部入或輸出范圍的邊界上，而不是在輸入范圍的內(nèi)部。因此。因此針對各種邊界情況設(shè)計(jì)測試用例，可以查出更多的錯(cuò)誤。針對各種邊界情況設(shè)計(jì)測試

18、用例，可以查出更多的錯(cuò)誤。比如，在做三角形計(jì)算時(shí)，要輸入三角形的三個(gè)邊長：比如，在做三角形計(jì)算時(shí)，要輸入三角形的三個(gè)邊長：A、B和和C。 我們應(yīng)注意到這三個(gè)數(shù)值應(yīng)當(dāng)滿足我們應(yīng)注意到這三個(gè)數(shù)值應(yīng)當(dāng)滿足 A0、B0、C0、 ABC、ACB、BCA，才能才能構(gòu)成三角形。但如果把六個(gè)不等式中的任何一個(gè)大于號(hào)構(gòu)成三角形。但如果把六個(gè)不等式中的任何一個(gè)大于號(hào)“”錯(cuò)寫成大于等于號(hào)錯(cuò)寫成大于等于號(hào)“”，那就不能構(gòu)成三角形。問題恰出現(xiàn)在，那就不能構(gòu)成三角形。問題恰出現(xiàn)在容易被疏忽的邊界附近。容易被疏忽的邊界附近。使用邊界值分析方法設(shè)計(jì)測試用例，首先應(yīng)確定邊界情況。使用邊界值分析方法設(shè)計(jì)測試用例，首先應(yīng)確定邊界情

19、況。應(yīng)當(dāng)應(yīng)當(dāng)選取正好等于，剛剛大于，或剛剛小于邊界的值做為測試數(shù)據(jù)選取正好等于，剛剛大于，或剛剛小于邊界的值做為測試數(shù)據(jù)，而不是選取等價(jià)類中的典型值或任意值做為測試數(shù)據(jù)。而不是選取等價(jià)類中的典型值或任意值做為測試數(shù)據(jù)。錯(cuò)誤推測法錯(cuò)誤推測法因果圖因果圖如果在測試時(shí)必須考慮如果在測試時(shí)必須考慮輸入條件的各種組合輸入條件的各種組合，可使用，可使用一種適合于描述對于多種條件的組合，相應(yīng)產(chǎn)生多個(gè)動(dòng)一種適合于描述對于多種條件的組合，相應(yīng)產(chǎn)生多個(gè)動(dòng)作的形式來設(shè)計(jì)測試用例，這就需要利用因果圖。作的形式來設(shè)計(jì)測試用例，這就需要利用因果圖。把輸入條件視為把輸入條件視為“因因”，把輸出條件視為，把輸出條件視為“果果

20、”，將，將黑盒看成是從因到果的網(wǎng)絡(luò)圖，采用邏輯圖的形式來表黑盒看成是從因到果的網(wǎng)絡(luò)圖，采用邏輯圖的形式來表達(dá)功能說明書中輸入條件的各種組合與輸出的關(guān)系。根達(dá)功能說明書中輸入條件的各種組合與輸出的關(guān)系。根據(jù)這種關(guān)系可選擇高效的測試用例。據(jù)這種關(guān)系可選擇高效的測試用例。因果圖是一種形式化語言，是一種組合邏輯網(wǎng)絡(luò)圖。因果圖是一種形式化語言，是一種組合邏輯網(wǎng)絡(luò)圖。因果圖方法最終生成的就是判定表。它適合于檢查程因果圖方法最終生成的就是判定表。它適合于檢查程序輸入條件的各種組合情況。序輸入條件的各種組合情況。實(shí)例實(shí)例用因果圖生成測試用例的基本步驟(1) 分析軟件規(guī)格說明描述中，哪些是原因 (即輸入條件或輸

21、入條件的等價(jià)類)，哪些是結(jié)果 (即輸出條件)，并給每個(gè)原因和結(jié)果賦予一個(gè)標(biāo)識(shí)符。(2) 分析軟件規(guī)格說明描述中的語義，找出原因與結(jié)果之間，原因與原因之間對應(yīng)的是什么關(guān)系? 根據(jù)這些關(guān)系，畫出因果圖。(3) 由于語法或環(huán)境限制，有些原因與原因之間，原因與結(jié)果之間的組合情況不可能出現(xiàn)。為表明這些特殊情況，在因果圖上用一些記號(hào)標(biāo)明約束或限制條件。(4) 把因果圖轉(zhuǎn)換成判定表。(5) 把判定表的每一列作為依據(jù)，設(shè)計(jì)測試用例。實(shí)例實(shí)例在因果圖中出現(xiàn)的基本符號(hào)通常在因果圖中用Ci表示原因，用Ei表示結(jié)果，各結(jié)點(diǎn)表示狀態(tài)，可取值“0”或“1”。“0”表示某狀態(tài)不出現(xiàn)，“1”表示某狀態(tài)出現(xiàn)。主要的原因和結(jié)果之

22、間的關(guān)系有：實(shí)例實(shí)例表示約束條件的符號(hào)為了表示原因與原因之間，結(jié)果與結(jié)果之間可能存在的約束條件，在因果圖中可以附加一些表示約束條件的符號(hào)。實(shí)例實(shí)例例如，有一個(gè)處理單價(jià)為5角錢的飲料的自動(dòng)售貨機(jī)軟件測試用例的設(shè)計(jì)。其規(guī)格說明如下：若投入5角錢或1元錢的硬幣，押下橙汁或啤酒的按鈕，則相應(yīng)的飲料就送出來。若售貨機(jī)沒有零錢找，則一個(gè)顯示零錢找完的紅燈亮，這時(shí)再投入1元硬幣并押下按鈕后，飲料不送出來而且1元硬幣也退出來；若有零錢找，則顯示零錢找完的紅燈滅，在送出飲料的同時(shí)退還5角硬幣?！睂?shí)例實(shí)例(1) 分析這一段說明，列出原因和結(jié)果原因: 1. 售貨機(jī)有零錢找2. 投入1元硬幣3. 投入5角硬幣4. 押

23、下橙汁按鈕5. 押下啤酒按鈕建立中間結(jié)點(diǎn)，表示處理中間狀態(tài)11. 投入1元硬幣且押下飲料按鈕12. 押下橙汁或啤酒的按鈕13. 應(yīng)當(dāng)找5角零錢并且售貨機(jī)有零錢找14. 錢已付清實(shí)例實(shí)例結(jié)果： 21. 售貨機(jī)零錢找完燈亮22. 退還1元硬幣23. 退還5角硬幣24. 送出橙汁飲料25. 送出啤酒飲料(2) 畫出因果圖。所有原因結(jié)點(diǎn)列在左邊，所有結(jié)果結(jié)點(diǎn)列在右邊。(3) 由于 2 與 3 ，4 與 5 不能同時(shí)發(fā)生，分別加上約束條件E。(4) 因果圖實(shí)例實(shí)例實(shí)例實(shí)例(5) 轉(zhuǎn)換成判定表實(shí)例實(shí)例程序測試的黑盒子方法常憑程序測試的黑盒子方法常憑經(jīng)驗(yàn)經(jīng)驗(yàn)進(jìn)行，在設(shè)計(jì)進(jìn)行，在設(shè)計(jì)測試用例時(shí)可以綜合使用上述

24、各種方法。在設(shè)測試用例時(shí)可以綜合使用上述各種方法。在設(shè)計(jì)測試數(shù)據(jù)時(shí)，我們應(yīng)該考慮認(rèn)為最易出錯(cuò)和計(jì)測試數(shù)據(jù)時(shí)，我們應(yīng)該考慮認(rèn)為最易出錯(cuò)和最易忽略的地方，進(jìn)行重點(diǎn)測試。最易忽略的地方，進(jìn)行重點(diǎn)測試。白盒測試白盒測試 邏輯覆蓋： 語句覆蓋 判定覆蓋 條件覆蓋 判定條件覆蓋 條件組合覆蓋 路徑覆蓋循環(huán)覆蓋基本路徑測試?yán)永釉嚋y試下面這一程序試測試下面這一程序Procedure P(varProcedure P(var A,B:REAL) A,B:REAL)beginbegin if(A if(A1)and(B=0)then X:=X/A;1)and(B=0)then X:=X/A; if(A if(

25、A=2)or (X1)then X:=X+1;=2)or (X1)then X:=X+1;endend在執(zhí)行這個(gè)程序時(shí)，有各種不同的路徑，如： a b d a b e d a c b d a c b e d我們可用白盒子方法設(shè)計(jì)測試用例，其任務(wù)是我們可用白盒子方法設(shè)計(jì)測試用例，其任務(wù)是盡盡可能多地執(zhí)行各種語句可能多地執(zhí)行各種語句，以及調(diào)試到各種路徑。，以及調(diào)試到各種路徑。如選擇如選擇 A = 2 ,B = 0 ,X = 3則可執(zhí)行路徑則可執(zhí)行路徑 a c b e d此時(shí)能覆蓋到全部此時(shí)能覆蓋到全部2個(gè)計(jì)算框，可發(fā)現(xiàn)一般的語句個(gè)計(jì)算框，可發(fā)現(xiàn)一般的語句的錯(cuò)誤的錯(cuò)誤這組數(shù)據(jù)可使語句都能執(zhí)行一次這組

26、數(shù)據(jù)可使語句都能執(zhí)行一次我們通常把這種我們通常把這種注重語句注重語句的覆蓋叫的覆蓋叫“語句覆蓋語句覆蓋”執(zhí)行足夠多的測試用例，使得被測程序中每個(gè)可執(zhí)行足夠多的測試用例，使得被測程序中每個(gè)可執(zhí)行語句至少被執(zhí)行一次執(zhí)行語句至少被執(zhí)行一次這種覆蓋肯定是不充分的，如：第這種覆蓋肯定是不充分的，如：第一個(gè)判斷中一個(gè)判斷中and誤寫為誤寫為or，第二個(gè)判，第二個(gè)判斷中斷中X1誤寫為誤寫為X0，則無法暴露出，則無法暴露出程序的錯(cuò)誤。程序的錯(cuò)誤。語句覆蓋是最弱的邏輯覆蓋準(zhǔn)則語句覆蓋是最弱的邏輯覆蓋準(zhǔn)則 。如選擇如選擇A = 3,B = 0,X = 1A = 2,B = 1,X = 3則可執(zhí)行的路徑為則可執(zhí)行的

27、路徑為 a c b d a b e d從所走路徑來看，上面這組數(shù)據(jù)要全面一些，它不僅通從所走路徑來看，上面這組數(shù)據(jù)要全面一些，它不僅通過全部兩個(gè)計(jì)算框，而且第一個(gè)判別框的兩邊都執(zhí)行過過全部兩個(gè)計(jì)算框，而且第一個(gè)判別框的兩邊都執(zhí)行過一次。一次。我們通常把這種我們通常把這種注重選擇測試注重選擇測試的覆蓋叫做的覆蓋叫做“判定覆判定覆蓋蓋”，又稱為，又稱為“分支覆蓋分支覆蓋”。執(zhí)行足夠多的測試用例，使得被測程序中每個(gè)語句至少執(zhí)行足夠多的測試用例，使得被測程序中每個(gè)語句至少被執(zhí)行一次，且每個(gè)判斷的真假分支至少執(zhí)行一次被執(zhí)行一次，且每個(gè)判斷的真假分支至少執(zhí)行一次n但這組數(shù)據(jù)仍未檢查到路徑但這組數(shù)據(jù)仍未檢查

28、到路徑abd;第一個(gè)計(jì)第一個(gè)計(jì)算框執(zhí)行結(jié)果是否影響條件的執(zhí)行也尚未算框執(zhí)行結(jié)果是否影響條件的執(zhí)行也尚未測試到。測試到。n它仍不充分它仍不充分如選擇如選擇A=2,B=0,X=4A=2,B=0,X=4A=1,B=1,X=1A=1,B=1,X=1則可執(zhí)行的路徑為則可執(zhí)行的路徑為 a c b e da c b e d a b d a b d從這組數(shù)據(jù)來看，它從這組數(shù)據(jù)來看，它注意了注意了4 4個(gè)條件個(gè)條件A1,B=0,A=2A1,B=0,A=2和和X1X1的覆蓋。我們稱這種注重的覆蓋。我們稱這種注重判斷的覆蓋為判斷的覆蓋為“條件覆蓋條件覆蓋”。執(zhí)行足夠多的測試用例，使得被測程序中執(zhí)行足夠多的測試用例，

29、使得被測程序中每個(gè)判定的每個(gè)條件的可能值每個(gè)判定的每個(gè)條件的可能值至少執(zhí)行一至少執(zhí)行一次次n雖然覆蓋有所改善，但對第一個(gè)判斷為雖然覆蓋有所改善，但對第一個(gè)判斷為真，第二個(gè)為假這一路徑真，第二個(gè)為假這一路徑acbd未測試到。未測試到。n它仍不充分它仍不充分 判定判定/ /條件覆蓋條件覆蓋執(zhí)行足夠多的測試用例，使得被測程序中的判定的執(zhí)行足夠多的測試用例，使得被測程序中的判定的每個(gè)條件的所有可能取值至少執(zhí)行一次，同時(shí)每個(gè)每個(gè)條件的所有可能取值至少執(zhí)行一次，同時(shí)每個(gè)判定本身的所有可能判定結(jié)果至少執(zhí)行一次。判定本身的所有可能判定結(jié)果至少執(zhí)行一次。是判定覆蓋與條件覆蓋的綜合，但不能保證檢查出是判定覆蓋與條

30、件覆蓋的綜合，但不能保證檢查出邏輯表達(dá)式的全部錯(cuò)誤。邏輯表達(dá)式的全部錯(cuò)誤。 對于上例中對于上例中A1A1時(shí)檢查時(shí)檢查B=0B=0，而，而 A=1A=1時(shí)，時(shí)，B0B0卻卻不去驗(yàn)證了。不去驗(yàn)證了。A=2 B=0 X=4 ; A=3,B=1,X=1兩個(gè)測試用例能同時(shí)滿足判定、條件兩個(gè)測試用例能同時(shí)滿足判定、條件覆蓋覆蓋 以上這些數(shù)據(jù)雖然均達(dá)到一些測試目的，且各有側(cè)重，但是以上這些數(shù)據(jù)雖然均達(dá)到一些測試目的，且各有側(cè)重，但是都是不充分的。都是不充分的。如從條件出發(fā)，用組合的辦法使如從條件出發(fā)，用組合的辦法使各個(gè)條件都能執(zhí)行到各個(gè)條件都能執(zhí)行到，則我，則我們可以寫出以下們可以寫出以下8種條件組合：種條

31、件組合：1)A1,B=02)A1,B0;(是不等號(hào)是不等號(hào))3)A=1,B=04)A=1,B05)A=2,X16)A=2,X=17)A2,X18)A2,X0B:=AB0 B=0P A=0例例4： 計(jì)算計(jì)算X=MAX(A,B)X=MAX(A,B)的程序?yàn)榈某绦驗(yàn)閕f A=B then X:=A else X:=Bif A=B then X:=A else X:=B 試驗(yàn)證其正確性。試驗(yàn)證其正確性。 證明：證明：P:trueP A=BX:=AX=A X=BP AA 而而 X=A X=B X=MAX(A,B) X=B XA X=MAX(A,B) 故故P:true if A=B then X:=A e

32、lse X:=B. X=MAX(A,B) 求如圖所示條件語句的前提與結(jié)論求如圖所示條件語句的前提與結(jié)論P(yáng):true則，則，trueif A0 THEN B:=A else B:=-AB=06 6、循環(huán)語句、循環(huán)語句 BSdoBwhileSB;QSdoBwhilePQBSBP稱為稱為循環(huán)不變式循環(huán)不變式：一個(gè)在每次循環(huán)的前后均為真的謂詞。 終止性終止性： t t0 0(0T=t(0T=t0 0S0S0 Tt T0 5. T=t0 S T0 y0Q:=0;R:=x;while R=y do begin R:=R-y;Q:=Q+1 endQ:x=R+Q*y 0=R=0其中循環(huán)不變式為：:x=R+Q*

33、y R0 Q=0 界函數(shù)T:R 證明：(1) P=x0 y0 Q:=0;R:=x; P1=x0 y0 Q=0 R=x(2)(2)循環(huán)語句1. P1 =x=R+Q*y R0 Q=0，顯然成立2. B R:=R-y; Q:=Q+1 B x=R+Q*y R0 Q=0 R=y R:=R-y x=R+y+Q*y R 0-y Q=0 R =y-y x=R+(Q+1)*y R-y Q=0 R=0 Q:=Q+1 x=R+Q*y R-y Q=0 R=0 3. B Q x=R+Q*y R0 Q=0 Ry Q:x=R+Q*y 0=R=04. B T=0 x=R+Q*y R0 Q=0 R=y R=05. T=t0 R

34、:=R-y; Q:=Q+1Tt0 R=t0 R:=R-y; R=t0-y Q:=Q+1R=t0-y t0 T0 Q=01. P 2. B S3. B Q4. B T0 5. T=t0 S T06. T=t0 S T0 y0z:=0;u:=x;repeat z:=z+y; u:=u-1;until u=0R:z=x*y: x*y=z+u*y u0Q: x*y=z+u*y u=0證明：1. P z:=0;u:=x;P P z:=0;x0 y0 z=0u:=x; x0 y0 z=0 u=x P x0 y0 z=0 u=x2.P repeat z:=z+y; u:=u-1;until u=0 R 1)

35、 P 顯然， x0 y0 z=0 u=x x*y=z+u*y u0成立。2) z:=z+y; u:=u-1;Q x*y=z+u*y u0z:=z+y; x*y=z-y +u*y u0 u:=u-1; x*y=z+y +(u-1)*y u-1 x*y=z +u*y u-1 Q3)Q B x*y=z+u*y u=0 u0 x*y=z+u*y u04)Q B Rx*y=z+u*y u=0 u=0 x*y=z u=0 x*y=z R5) B T0 B x*y=z+u*y u0 u0因?yàn)門=u0,所以 B T0成立6)T=t0 z:=z+y; u:=u-1;Tt0 u=t0 z:=z+y; u=t0u:

36、=u-1; u=t0-1t0 u=t0 u t0+1 z:=z+y; u-1 t0u:=u-1;u0 Q: x*y=z+u*y u=01. P 2. SQ3. Q B 4. Q B R5. B T06. T=t0 S TB P=Q (2) A=B 則證明分析過程每步成立 (3) 不需證明終止性，因?yàn)镕OR語句一定會(huì)終止的。 給定數(shù)組X,Y begin s:=0; P: 給定數(shù)組X,Y s=0 for I=1 to N do S:=S+XI*YI endNjjYjX1*Q:S= 證明：(1) N1 P: 給定數(shù)組X,Y s=0 Q:S= 所以，N=1a) P I=1SQ(1) S=0 I=1 S

37、:=S+XI*YIS= b) Q(pred(I)SQ(I), Q(I-1)SQ(I) S= S:=S+XI*YI S= +XI*YI S= C) Q(B)=Q, Q(B) Q要證Q(B)=Q(N)=Q,即I=N, Q(N)= =QNjjYjX1*0)*:1 :(jYjXNjj11*jjYjX11*IjjYjX11*IjjYjXIjjYjX1*NjjYjX1*定義定義：假定：假定S是一個(gè)語句，是一個(gè)語句，R是一個(gè)謂詞，它描述是一個(gè)謂詞，它描述S執(zhí)執(zhí)行后所確定的某種關(guān)系。從行后所確定的某種關(guān)系。從S和和R定義另外一個(gè)謂定義另外一個(gè)謂詞，記為詞，記為 wp(“S”,R),它表示：它表示： “所有這樣

38、的狀態(tài)的集合，所有這樣的狀態(tài)的集合，S S從其中任一狀態(tài)開始從其中任一狀態(tài)開始執(zhí)行必將在有限的時(shí)間內(nèi)終止于滿足執(zhí)行必將在有限的時(shí)間內(nèi)終止于滿足R R的狀態(tài)的狀態(tài)”。 稱稱 wp( “S”,R) 是語句是語句S關(guān)于關(guān)于R的最弱前置謂詞的最弱前置謂詞 - S - 終止終止 wp (“S”,R) R 一些狀態(tài)集合一些狀態(tài)集合 后置條件后置條件三、三、DijkstraDijkstra最弱前置條件方法最弱前置條件方法 （二）（二） 最弱前置謂詞的幾個(gè)性質(zhì)公理最弱前置謂詞的幾個(gè)性質(zhì)公理 1、排奇律：wp (“S”, F)=F 要從某個(gè)狀態(tài)集的任何一個(gè)狀態(tài)出發(fā)執(zhí)行要從某個(gè)狀態(tài)集的任何一個(gè)狀態(tài)出發(fā)執(zhí)行S后必定

39、會(huì)終后必定會(huì)終止，終止時(shí)滿足止，終止時(shí)滿足F，即使，即使F為真，這樣的狀態(tài)是找不到的，為真，這樣的狀態(tài)是找不到的，因此對應(yīng)的狀態(tài)集為空。因此對應(yīng)的狀態(tài)集為空。 2、合取分配律：wp(“S”,Q) wp(“S”,R)=wp(“S”, Q R) 表示從某一狀態(tài)開始執(zhí)行表示從某一狀態(tài)開始執(zhí)行S S，能終止，且分別滿足和，能終止，且分別滿足和的狀態(tài)，那它當(dāng)然也能終止，且滿足的狀態(tài)，那它當(dāng)然也能終止，且滿足的狀態(tài)，反之亦的狀態(tài)，反之亦然然。 3、單調(diào)律：如果Q R，則wp(“S”,Q) wp(“S”,R) 4、折取分配律：wp (“S”,Q) wp (“S”,R) wp (“S”, Q R) n確定程序

40、：從某一個(gè)狀態(tài)出發(fā)，程序不管執(zhí)行多少次，所經(jīng)過的路徑相同，所得的結(jié)果也相同。wp (“S”,Q) wp (“S”,R)=wp (“S”, Q R) n不確定程序：從某一個(gè)狀態(tài)出發(fā)，程序的任何兩次執(zhí)行可能得到的結(jié)果都不同，有時(shí)即便所得的結(jié)果相同，可能經(jīng)過的路徑也不同。wp (“S”,Q) wp (“S”,R) wp (“S”, Q R) 例：拋硬幣具有不確定性 wp(“拋硬幣”，正面)=F wp(“拋硬幣”，反面)=Fwp(“拋硬幣”，正面 反面)=T （三）求解最弱前置謂詞的規(guī)則（三）求解最弱前置謂詞的規(guī)則 1、skip、abort、復(fù)合語句wp(“skip”,R)=R (相當(dāng)于空語句)wp(

41、“abort”,R)=F (執(zhí)行過程中夭折的語句)wp(“S1,S2”,R)= wp(“S1”, wp(“S2”,R)（相當(dāng)于順序復(fù)合語句）例如wp(“skip;skip”,R)=wp(“skip”,wp(“skip”,R)=R2、 賦值語句(1) 單個(gè)簡單變量的賦值語句(2) 多個(gè)簡單變量的賦值語句(3) 單個(gè)數(shù)組元素的賦值（1）單個(gè)簡單變量的賦值語句 S:=I:=E其語義為： wp(“I:=E”,R)=domain(E) canddomain(E) 表示能獲得正常表達(dá)式E結(jié)果條件。 當(dāng)條件顯然時(shí)，可略去此項(xiàng)。 表示表達(dá)式E去替換R中所有自由出現(xiàn)的變量I。B1 cand B2 表示從左到右的

42、次序計(jì)算，B1為F時(shí)，則不必計(jì)算B2,其結(jié)果全為F。B1為T時(shí)，則其結(jié)果為B2的結(jié)果。B1無定義時(shí)，其結(jié)果也無定義。IERIER1.wp(“x:=x+1”,x0)=(x+10)=x-12.wp(“x:=5”,x=5)=5=5=T 3.wp(“x:=5”,x5)=55=F 4.wp(“x:=AB”,P(x)=(B0) cand P(AB) 5.wp(“x:=x *x”, x4=10) =(x*x)4=10)=x8=106.設(shè)數(shù)組B的下標(biāo)域?yàn)?：100，則: wp(“x:=BI”,x=BI)=(0=I=100) cand BI=BI =0=I0s=(j:0=j0s+bi= (j:0=j=0 s=

43、(j:0=ji:bj)10.Ta:=a+1;b:=xa=b wp(“a:=a+1;b:=x”,a=b)=wp(“a:=a+1”,a=x) =a+1=x11. wp(“a:=a+1;b:=x(a,b)”,a=b) = wp(“a:=a+1”,a=x(a,b)=a+1=x(a+1,b)練練 習(xí)習(xí)(3)(3)單個(gè)數(shù)組元素的賦值語句單個(gè)數(shù)組元素的賦值語句對一個(gè)數(shù)組元素的賦值語句 S:=bi:=E其中b是數(shù)組名，i是b的下標(biāo)表達(dá)式我們用（b;i:E)表示一個(gè)數(shù)組函數(shù)，定義為： (b; i: E)j= E 當(dāng) i=j bj 當(dāng)ij這樣，語句bi:=E等價(jià)于b:=(b;i:E)若略去domain(E)與domain(i)等因素，數(shù)組的賦值語句語義是wp(“bi:=E”,R)=Rb(b;i: