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

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

2、該做的事，沒(méi)有做它不該做的事事”一段程序是錯(cuò)誤的，是指：一段程序是錯(cuò)誤的，是指：（1 1）程序完成的事情并不是程序員想要完成的事）程序完成的事情并不是程序員想要完成的事情；情；（2 2）程序員想要程序完成的事情，程序并沒(méi)有完）程序員想要程序完成的事情，程序并沒(méi)有完成。成。一般來(lái)說(shuō)，程序中含有錯(cuò)誤是很難避免的。一般來(lái)說(shuō)，程序中含有錯(cuò)誤是很難避免的。錯(cuò)誤可能有：錯(cuò)誤可能有：（1 1）設(shè)計(jì)時(shí)的錯(cuò)誤；）設(shè)計(jì)時(shí)的錯(cuò)誤；（2 2）程序編寫(xiě)時(shí)的錯(cuò)誤；）程序編寫(xiě)時(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ǎn)單、程序的結(jié)構(gòu)要簡(jiǎn)單 2 2、采用標(biāo)準(zhǔn)的軟件設(shè)計(jì)工具、標(biāo)準(zhǔn)的算法手冊(cè)以及有效、采用標(biāo)準(zhǔn)的軟件設(shè)計(jì)工具、標(biāo)準(zhǔn)的算法手冊(cè)以及有效的程序設(shè)計(jì)方法的程序設(shè)計(jì)方法發(fā)現(xiàn)錯(cuò)誤的方法發(fā)現(xiàn)錯(cuò)誤的方法 1 1、利用測(cè)試工具、利用測(cè)試工具: :跟蹤程序的運(yùn)行，用測(cè)試的辦法去查找跟蹤程序的運(yùn)行，用測(cè)試的辦法去查找并發(fā)現(xiàn)程序

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

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

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

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

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

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

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

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

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

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

14、例子例子 某個(gè)某個(gè)TRIANGLETRIANGLE程序，用程序，用3 3個(gè)整數(shù)表示一個(gè)三角個(gè)整數(shù)表示一個(gè)三角形的形的3 3條邊長(zhǎng)。當(dāng)輸入條邊長(zhǎ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ù)組來(lái)測(cè)試程序時(shí)，我們可以憑經(jīng)構(gòu)。在選擇數(shù)據(jù)組來(lái)測(cè)試程序時(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)生的情況來(lái)測(cè)試的方法顯然是黑盒子列出各種產(chǎn)生的情況來(lái)測(cè)試的方法顯然是黑盒子方法。它不關(guān)心盒子內(nèi)程序的具體邏輯，只是根方法。它不關(guān)心盒子內(nèi)程序的具體邏輯，只是根據(jù)程序功能來(lái)設(shè)計(jì)測(cè)試用例據(jù)程序功能來(lái)設(shè)計(jì)測(cè)試用例等價(jià)類劃分等價(jià)類劃分 有效等價(jià)類：是指對(duì)于程序的規(guī)格說(shuō)明來(lái)說(shuō)，是合理的，有效等價(jià)類：是指對(duì)于程序的規(guī)格說(shuō)明來(lái)說(shuō)，是合理的，有意義的輸入數(shù)據(jù)構(gòu)成的集合。有意義的輸入數(shù)據(jù)構(gòu)成的集合。 無(wú)效等價(jià)類：是指對(duì)于程序的規(guī)格說(shuō)明來(lái)說(shuō)，是不合理無(wú)效等價(jià)類：是指對(duì)于程序的規(guī)格說(shuō)明來(lái)說(shuō)，是不合理的，無(wú)意義的輸入數(shù)據(jù)構(gòu)成的集合。的，無(wú)意義的輸入數(shù)

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

18、用例，可以查出更多的錯(cuò)誤。比如，在做三角形計(jì)算時(shí)，要輸入三角形的三個(gè)邊長(zhǎng)：比如，在做三角形計(jì)算時(shí)，要輸入三角形的三個(gè)邊長(zhǎng)：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ò)寫(xiě)成大于等于號(hào)錯(cuò)寫(xiě)成大于等于號(hào)“”，那就不能構(gòu)成三角形。問(wèn)題恰出現(xiàn)在，那就不能構(gòu)成三角形。問(wèn)題恰出現(xiàn)在容易被疏忽的邊界附近。容易被疏忽的邊界附近。使用邊界值分析方法設(shè)計(jì)測(cè)試用例，首先應(yīng)確定邊界情況。使用邊界值分析方法設(shè)計(jì)測(cè)試用例，首先應(yīng)確定邊界情

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

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

21、入條件的等價(jià)類)，哪些是結(jié)果 (即輸出條件)，并給每個(gè)原因和結(jié)果賦予一個(gè)標(biāo)識(shí)符。(2) 分析軟件規(guī)格說(shuō)明描述中的語(yǔ)義，找出原因與結(jié)果之間，原因與原因之間對(duì)應(yīng)的是什么關(guān)系? 根據(jù)這些關(guān)系，畫(huà)出因果圖。(3) 由于語(yǔ)法或環(huán)境限制，有些原因與原因之間，原因與結(jié)果之間的組合情況不可能出現(xiàn)。為表明這些特殊情況，在因果圖上用一些記號(hào)標(biāo)明約束或限制條件。(4) 把因果圖轉(zhuǎn)換成判定表。(5) 把判定表的每一列作為依據(jù)，設(shè)計(jì)測(cè)試用例。實(shí)例實(shí)例在因果圖中出現(xiàn)的基本符號(hào)通常在因果圖中用Ci表示原因，用Ei表示結(jié)果，各結(jié)點(diǎn)表示狀態(tài)，可取值“0”或“1”?！?”表示某狀態(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ī)軟件測(cè)試用例的設(shè)計(jì)。其規(guī)格說(shuō)明如下：若投入5角錢或1元錢的硬幣，押下橙汁或啤酒的按鈕，則相應(yīng)的飲料就送出來(lái)。若售貨機(jī)沒(méi)有零錢找，則一個(gè)顯示零錢找完的紅燈亮，這時(shí)再投入1元硬幣并押下按鈕后，飲料不送出來(lái)而且1元硬幣也退出來(lái)；若有零錢找，則顯示零錢找完的紅燈滅，在送出飲料的同時(shí)退還5角硬幣?！睂?shí)例實(shí)例(1) 分析這一段說(shuō)明，列出原因和結(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) 畫(huà)出因果圖。所有原因結(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í)例程序測(cè)試的黑盒子方法常憑程序測(cè)試的黑盒子方法常憑經(jīng)驗(yàn)經(jīng)驗(yàn)進(jìn)行，在設(shè)計(jì)進(jìn)行，在設(shè)計(jì)測(cè)試用例時(shí)可以綜合使用上述

24、各種方法。在設(shè)測(cè)試用例時(shí)可以綜合使用上述各種方法。在設(shè)計(jì)測(cè)試數(shù)據(jù)時(shí)，我們應(yīng)該考慮認(rèn)為最易出錯(cuò)和計(jì)測(cè)試數(shù)據(jù)時(shí)，我們應(yīng)該考慮認(rèn)為最易出錯(cuò)和最易忽略的地方，進(jìn)行重點(diǎn)測(cè)試。最易忽略的地方，進(jìn)行重點(diǎn)測(cè)試。白盒測(cè)試白盒測(cè)試 邏輯覆蓋： 語(yǔ)句覆蓋 判定覆蓋 條件覆蓋 判定條件覆蓋 條件組合覆蓋 路徑覆蓋循環(huán)覆蓋基本路徑測(cè)試?yán)永釉嚋y(cè)試下面這一程序試測(cè)試下面這一程序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ì)測(cè)試用例，其任務(wù)是我們可用白盒子方法設(shè)計(jì)測(cè)試用例，其任務(wù)是盡盡可能多地執(zhí)行各種語(yǔ)句可能多地執(zhí)行各種語(yǔ)句，以及調(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)一般的語(yǔ)句個(gè)計(jì)算框，可發(fā)現(xiàn)一般的語(yǔ)句的錯(cuò)誤的錯(cuò)誤這組數(shù)據(jù)可使語(yǔ)句都能執(zhí)行一次這組

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

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

28、到路徑abd;第一個(gè)計(jì)第一個(gè)計(jì)算框執(zhí)行結(jié)果是否影響條件的執(zhí)行也尚未算框執(zhí)行結(jié)果是否影響條件的執(zhí)行也尚未測(cè)試到。測(cè)試到。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ù)來(lái)看，它從這組數(shù)據(jù)來(lái)看，它注意了注意了4 4個(gè)條件個(gè)條件A1,B=0,A=2A1,B=0,A=2和和X1X1的覆蓋。我們稱這種注重的覆蓋。我們稱這種注重判斷的覆蓋為判斷的覆蓋為“條件覆蓋條件覆蓋”。執(zhí)行足夠多的測(cè)試用例，使得被測(cè)程序中執(zhí)行足夠多的測(cè)試用例，

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

30、件覆蓋的綜合，但不能保證檢查出邏輯表達(dá)式的全部錯(cuò)誤。邏輯表達(dá)式的全部錯(cuò)誤。 對(duì)于上例中對(duì)于上例中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è)測(cè)試用例能同時(shí)滿足判定、條件兩個(gè)測(cè)試用例能同時(shí)滿足判定、條件覆蓋覆蓋 以上這些數(shù)據(jù)雖然均達(dá)到一些測(cè)試目的，且各有側(cè)重，但是以上這些數(shù)據(jù)雖然均達(dá)到一些測(cè)試目的，且各有側(cè)重，但是都是不充分的。都是不充分的。如從條件出發(fā)，用組合的辦法使如從條件出發(fā)，用組合的辦法使各個(gè)條件都能執(zhí)行到各個(gè)條件都能執(zhí)行到，則我，則我們可以寫(xiě)出以下們可以寫(xiě)出以下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) 求如圖所示條件語(yǔ)句的前提與結(jié)論求如圖所示條件語(yǔ)句的前提與結(jié)論P(yáng):true則，則，trueif A0 THEN B:=A else B:=-AB=06 6、循環(huán)語(yǔ)句、循環(huán)語(yǔ)句 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)語(yǔ)句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 則證明分析過(guò)程每步成立 (3) 不需證明終止性，因?yàn)镕OR語(yǔ)句一定會(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è)語(yǔ)句，是一個(gè)語(yǔ)句，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)開(kāi)始從其中任一狀態(tài)開(kāi)始執(zhí)行必將在有限的時(shí)間內(nèi)終止于滿足執(zhí)行必將在有限的時(shí)間內(nèi)終止于滿足R R的狀態(tài)的狀態(tài)”。 稱稱 wp( “S”,R) 是語(yǔ)句是語(yǔ)句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)是找不到的，因此對(duì)應(yīng)的狀態(tài)集為空。因此對(duì)應(yīng)的狀態(tài)集為空。 2、合取分配律：wp(“S”,Q) wp(“S”,R)=wp(“S”, Q R) 表示從某一狀態(tài)開(kāi)始執(zhí)行表示從某一狀態(tài)開(kā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)過(guò)的路徑相同，所得的結(jié)果也相同。wp (“S”,Q) wp (“S”,R)=wp (“S”, Q R) n不確定程序：從某一個(gè)狀態(tài)出發(fā)，程序的任何兩次執(zhí)行可能得到的結(jié)果都不同，有時(shí)即便所得的結(jié)果相同，可能經(jīng)過(guò)的路徑也不同。wp (“S”,Q) wp (“S”,R) wp (“S”, Q R) 例：拋硬幣具有不確定性 wp(“拋硬幣”，正面)=F wp(“拋硬幣”，反面)=Fwp(“拋硬幣”，正面 反面)=T （三）求解最弱前置謂詞的規(guī)則（三）求解最弱前置謂詞的規(guī)則 1、skip、abort、復(fù)合語(yǔ)句wp(“skip”,R)=R (相當(dāng)于空語(yǔ)句)wp(

41、“abort”,R)=F (執(zhí)行過(guò)程中夭折的語(yǔ)句)wp(“S1,S2”,R)= wp(“S1”, wp(“S2”,R)（相當(dāng)于順序復(fù)合語(yǔ)句）例如wp(“skip;skip”,R)=wp(“skip”,wp(“skip”,R)=R2、 賦值語(yǔ)句(1) 單個(gè)簡(jiǎn)單變量的賦值語(yǔ)句(2) 多個(gè)簡(jiǎn)單變量的賦值語(yǔ)句(3) 單個(gè)數(shù)組元素的賦值（1）單個(gè)簡(jiǎn)單變量的賦值語(yǔ)句 S:=I:=E其語(yǔ)義為： 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無(wú)定義時(shí)，其結(jié)果也無(wú)定義。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ù)組元素的賦值語(yǔ)句單個(gè)數(shù)組元素的賦值語(yǔ)句對(duì)一個(gè)數(shù)組元素的賦值語(yǔ)句 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這樣，語(yǔ)句bi:=E等價(jià)于b:=(b;i:E)若略去domain(E)與domain(i)等因素，數(shù)組的賦值語(yǔ)句語(yǔ)義是wp(“bi:=E”,R)=Rb(b;i: