凈室軟件工程課件

第11章凈室軟件工程基本概念凈室策略功能規(guī)格說(shuō)明凈室設(shè)計(jì)凈室測(cè)試認(rèn)證第11章凈室軟件工程基本概念111.1基本概念凈室軟件工程(Cleanroomsoftwareengineering)是一種在軟件開(kāi)發(fā)過(guò)程中強(qiáng)調(diào)在軟件中建立正確性要求的方法。與傳統(tǒng)的分析、設(shè)計(jì)、編碼、測(cè)試和調(diào)試的周期觀點(diǎn)有所不同。11.1基本概念凈室軟件工程(Cleanroomsoft2凈室方法的觀點(diǎn)：

通過(guò)在第一次正確地書(shū)寫(xiě)代碼增量，并在測(cè)試前驗(yàn)證它們的正確性來(lái)避免成本很高的缺陷消除過(guò)程。它的過(guò)程模型是在代碼增量集成到系統(tǒng)的同時(shí)，進(jìn)行代碼增量的統(tǒng)計(jì)質(zhì)量驗(yàn)證。11.1基本概念凈室方法的觀點(diǎn)：11.1基本概念3與形式化方法技術(shù)一樣，凈室過(guò)程強(qiáng)調(diào)規(guī)格說(shuō)明和設(shè)計(jì)上的嚴(yán)格性，并且使用基于數(shù)學(xué)的正確性證明來(lái)對(duì)結(jié)果設(shè)計(jì)模型的每個(gè)元素進(jìn)行形式化驗(yàn)證。凈室方法不是先制造一個(gè)產(chǎn)品，然后再去消除缺陷，而是要求在規(guī)格說(shuō)明和設(shè)計(jì)中消除錯(cuò)誤，然后以“干凈”的方式進(jìn)行制造。凈室方法還對(duì)形式化方法進(jìn)行了擴(kuò)展，強(qiáng)調(diào)統(tǒng)計(jì)質(zhì)量控制技術(shù)，包括基于客戶對(duì)軟件的預(yù)期使用的測(cè)試。11.1基本概念與形式化方法技術(shù)一樣，凈室過(guò)程強(qiáng)調(diào)規(guī)格說(shuō)明和設(shè)計(jì)上的嚴(yán)格性4“第一次就將事情做正確”是軟件工程最重要的哲學(xué)。凈室軟件工程是這樣一個(gè)過(guò)程：它強(qiáng)調(diào)在程序構(gòu)造開(kāi)始前進(jìn)行正確性的數(shù)學(xué)驗(yàn)證，并且將軟件可靠性認(rèn)證作為軟件測(cè)試的一部分。其底線是極低的故障率，這是使用非形式化方法難于或不可能達(dá)到的。11.1基本概念“第一次就將事情做正確”是軟件工程最重要的哲學(xué)。11.1基520世紀(jì)80年代，Mills、Dyer、及Linger最先建議將凈室原理應(yīng)用于軟件工程。雖然在軟件開(kāi)發(fā)的早期，人們對(duì)其抱以很大的希望，但它并沒(méi)有得到廣泛的使用。

11.1基本概念20世紀(jì)80年代，Mills、Dyer、及Linger最先建6

Henderson提出了沒(méi)有得到廣泛使用的三個(gè)原因：1.凈室方法學(xué)太理論化、太數(shù)學(xué)化、太激進(jìn)，難于在實(shí)際的軟件開(kāi)發(fā)中使用。2.它提倡開(kāi)發(fā)者不需要進(jìn)行單元測(cè)試，而是進(jìn)行正確性驗(yàn)證和統(tǒng)計(jì)質(zhì)量控制，這些觀念與當(dāng)前大多數(shù)軟件開(kāi)發(fā)方式有很大的偏離。11.1基本概念Henderson提出了沒(méi)有得到廣泛使用的三個(gè)原因：1173.軟件開(kāi)發(fā)產(chǎn)業(yè)的成熟度不高。使用凈室過(guò)程需要在整個(gè)生命周期階段嚴(yán)格按照定義的過(guò)程進(jìn)行。由于大多數(shù)軟件企業(yè)的運(yùn)作還處于過(guò)程成熟度中的較低級(jí)別，軟件工程師還沒(méi)有準(zhǔn)備應(yīng)用凈室技術(shù)。11.1基本概念3.軟件開(kāi)發(fā)產(chǎn)業(yè)的成熟度不高。使用凈室過(guò)程需要在整個(gè)生命周期8“程序中出現(xiàn)錯(cuò)誤的唯一方式是作者將錯(cuò)誤引入進(jìn)去的。沒(méi)有其他方式……正確實(shí)踐的目標(biāo)是：設(shè)法避免引入錯(cuò)誤，如果引入了錯(cuò)誤，通過(guò)測(cè)試或任何其他運(yùn)行程序的方式來(lái)消除錯(cuò)誤。”

HarlanMills11.1基本概念11.1基本概念911.2凈室策略凈室方法使用增量過(guò)程模型。一個(gè)“軟件增量的流水線”由若干小的、獨(dú)立的軟件團(tuán)隊(duì)開(kāi)發(fā)。每當(dāng)一個(gè)軟件增量通過(guò)認(rèn)證，它就被集成到整體系統(tǒng)中。因此，系統(tǒng)的功能隨時(shí)間增加。11.2凈室策略凈室方法使用增量過(guò)程模型。10一旦將功能分配給系統(tǒng)的軟件元素，則可啟動(dòng)凈室增量的流水線。需要完成的任務(wù)如下：

(1)增量策劃。制定一個(gè)采用增量策略的項(xiàng)目計(jì)劃，確定每個(gè)增量的功能、預(yù)計(jì)規(guī)模、及凈室開(kāi)發(fā)進(jìn)度。(2)需求收集。為每個(gè)增量開(kāi)發(fā)更詳細(xì)的客戶級(jí)需求描述。

11.2凈室策略一旦將功能分配給系統(tǒng)的軟件元素，則可啟動(dòng)凈室增量的流水線。需11(3)盒結(jié)構(gòu)規(guī)格說(shuō)明。運(yùn)用盒結(jié)構(gòu)的規(guī)格說(shuō)明方法描述功能規(guī)格說(shuō)明。遵從操作分析原則，盒結(jié)構(gòu)“在每一個(gè)精化級(jí)別上使行為、數(shù)據(jù)及過(guò)程的創(chuàng)造性定義獨(dú)立”。(4)形式化設(shè)計(jì)。使用盒結(jié)構(gòu)方法，凈室設(shè)計(jì)是規(guī)格說(shuō)明的自然、無(wú)縫擴(kuò)展。對(duì)規(guī)格說(shuō)明(稱為黑盒)進(jìn)行迭代求精(在一個(gè)增量?jī)?nèi))類似于體系結(jié)構(gòu)設(shè)計(jì)和構(gòu)件級(jí)設(shè)計(jì)(分別稱為“狀態(tài)盒”和“清晰盒”)。

11.2凈室策略(3)盒結(jié)構(gòu)規(guī)格說(shuō)明。運(yùn)用盒結(jié)構(gòu)的規(guī)格說(shuō)明方法描述功能規(guī)格說(shuō)12(5)正確性驗(yàn)證。凈室團(tuán)隊(duì)對(duì)設(shè)計(jì)及代碼進(jìn)行一系列嚴(yán)格的正確性驗(yàn)證活動(dòng)。驗(yàn)證從最高層次的盒結(jié)構(gòu)(規(guī)格說(shuō)明)開(kāi)始，然后移向設(shè)計(jì)細(xì)節(jié)和代碼。正確性驗(yàn)證的第一層次通過(guò)應(yīng)用一組“正確性問(wèn)題”來(lái)進(jìn)行，如果這些沒(méi)有證明規(guī)格說(shuō)明是正確的，則使用更形式化的(數(shù)學(xué)的)驗(yàn)證方法。11.2凈室策略(5)正確性驗(yàn)證。凈室團(tuán)隊(duì)對(duì)設(shè)計(jì)及代碼進(jìn)行一系列嚴(yán)格的正確13(6)代碼生成、檢查和驗(yàn)證。以某種專門(mén)語(yǔ)言表示的盒結(jié)構(gòu)規(guī)格說(shuō)明被翻譯為適當(dāng)?shù)某绦蛟O(shè)計(jì)語(yǔ)言。然后，使用標(biāo)準(zhǔn)的走查或檢查技術(shù)來(lái)保證代碼和盒結(jié)構(gòu)的語(yǔ)義相符性，以及代碼的語(yǔ)法正確性。最后，對(duì)源代碼進(jìn)行正確性驗(yàn)證。

11.2凈室策略(6)代碼生成、檢查和驗(yàn)證。以某種專門(mén)語(yǔ)言表示的盒結(jié)構(gòu)規(guī)格說(shuō)14(7)統(tǒng)計(jì)測(cè)試規(guī)劃。分析軟件的預(yù)計(jì)使用情況，規(guī)劃并設(shè)計(jì)一組測(cè)試用例，以測(cè)試使用情況的“概率分布”。

11.2凈室策略(7)統(tǒng)計(jì)測(cè)試規(guī)劃。分析軟件的預(yù)計(jì)使用情況，規(guī)劃并設(shè)計(jì)一組測(cè)15(8)統(tǒng)計(jì)使用測(cè)試。對(duì)計(jì)算機(jī)軟件進(jìn)行窮舉測(cè)試是不可能的，因此，設(shè)計(jì)有限數(shù)量的測(cè)試用例總是必要的。統(tǒng)計(jì)使用技術(shù)執(zhí)行由統(tǒng)計(jì)樣本導(dǎo)出的一系列測(cè)試，這里的統(tǒng)計(jì)樣本是從來(lái)自目標(biāo)人群的所有用戶對(duì)程序的所有可能執(zhí)行中抽取的。11.2凈室策略(8)統(tǒng)計(jì)使用測(cè)試。11.2凈室策略16(9)認(rèn)證。一旦完成驗(yàn)證、檢查和使用測(cè)試(并且所有錯(cuò)誤被改正)，則對(duì)增量進(jìn)行集成前的認(rèn)證工作。

11.2凈室策略(9)認(rèn)證。一旦完成驗(yàn)證、檢查和使用測(cè)試(并且所有錯(cuò)誤被17凈室方法的特異之處

明確使用統(tǒng)計(jì)質(zhì)量控制。使用基于數(shù)學(xué)的正確性證明來(lái)驗(yàn)證設(shè)計(jì)規(guī)格說(shuō)明。實(shí)現(xiàn)了一些測(cè)試技術(shù)，這些測(cè)試技術(shù)最有可能揭示具有嚴(yán)重影響的錯(cuò)誤。

凈室方法的特異之處明確使用統(tǒng)計(jì)質(zhì)量控制。18凈室軟件工程和傳統(tǒng)軟件實(shí)踐的差別在于：它不再?gòu)?qiáng)調(diào)(有些人稱取消)單元測(cè)試和調(diào)試的作用，從而大量地減少(或取消)由軟件開(kāi)發(fā)者所承擔(dān)的測(cè)試工作量。在凈室軟件工程中，單元測(cè)試和調(diào)試被正確性驗(yàn)證和基于統(tǒng)計(jì)的測(cè)試所替代。凈室方法的特異之處

凈室軟件工程和傳統(tǒng)軟件實(shí)踐的差別在于：它不再?gòu)?qiáng)調(diào)(有些人稱取1911.3功能規(guī)格說(shuō)明不管選擇哪種分析方法，操作分析原理總是適用的。對(duì)數(shù)據(jù)、功能和行為建模，并對(duì)結(jié)果模型進(jìn)行分解,提供更進(jìn)一步的詳細(xì)信息?？傮w目標(biāo)是從捕獲問(wèn)題實(shí)質(zhì)的規(guī)格說(shuō)明(模型)移向提供重要實(shí)現(xiàn)細(xì)節(jié)的規(guī)格說(shuō)明。11.3功能規(guī)格說(shuō)明不管選擇哪種分析方法，操作分析原理總是20凈室軟件工程通過(guò)使用盒結(jié)構(gòu)規(guī)格說(shuō)明的方法來(lái)遵從操作分析原則。一個(gè)“盒”在某個(gè)細(xì)節(jié)層次上封裝系統(tǒng)(或系統(tǒng)的某些方面)。通過(guò)逐步求精的過(guò)程，盒被精化為層次?！懊總€(gè)盒規(guī)格說(shuō)明的信息內(nèi)容足以定義其精化，不需要依賴任何其他盒的實(shí)現(xiàn)”。這使得分析員能夠按層次劃分一個(gè)系統(tǒng)——從頂層的基本表示到底層實(shí)現(xiàn)的特定細(xì)節(jié)。11.3功能規(guī)格說(shuō)明凈室軟件工程通過(guò)使用盒結(jié)構(gòu)規(guī)格說(shuō)明的方法來(lái)遵從操作分析原則。21有三種類型的盒：黑盒，狀態(tài)盒，清晰盒

黑盒。黑盒刻畫(huà)系統(tǒng)行為或系統(tǒng)部件的行為。通過(guò)運(yùn)用由觸發(fā)映射到反應(yīng)的一組轉(zhuǎn)換規(guī)則，系統(tǒng)(或部件)對(duì)特定的觸發(fā)(事件)做出反應(yīng)。

狀態(tài)盒。狀態(tài)盒以類似于對(duì)象的方式封裝狀態(tài)數(shù)據(jù)和服務(wù)(操作)。在這種規(guī)格說(shuō)明視圖中，表示出狀態(tài)盒的輸入(觸發(fā))和輸出(反應(yīng))。清晰盒。在清晰盒中定義狀態(tài)盒所蘊(yùn)含的轉(zhuǎn)換功能，簡(jiǎn)單地說(shuō)，清晰盒包含了對(duì)狀態(tài)盒的過(guò)程設(shè)計(jì)。11.3功能規(guī)格說(shuō)明有三種類型的盒：黑盒，狀態(tài)盒，清晰盒11.3功能規(guī)格說(shuō)22黑盒規(guī)格說(shuō)明

黑盒規(guī)格說(shuō)明描述一種抽象、觸發(fā)和反應(yīng)。函數(shù)f被應(yīng)用到輸入(觸發(fā))S的序列S*，并將它們變換為輸出(反應(yīng))R。對(duì)于簡(jiǎn)單的軟件構(gòu)件，f可以是一個(gè)數(shù)學(xué)函數(shù)，但一般情況下，使用自然語(yǔ)言(或形式化規(guī)格說(shuō)明語(yǔ)言)描述f。黑盒規(guī)格說(shuō)明黑盒規(guī)格說(shuō)明黑盒規(guī)格說(shuō)明描述一種抽象、觸發(fā)和反應(yīng)。函數(shù)f被23為面向?qū)ο笙到y(tǒng)引入的很多概念也適用于黑盒。黑盒封裝數(shù)據(jù)抽象和操縱抽象數(shù)據(jù)的操作。和類層次一樣，黑盒規(guī)約可以展示使用層次，其中，低層盒從樹(shù)結(jié)構(gòu)中的高層盒繼承屬性。黑盒規(guī)格說(shuō)明

為面向?qū)ο笙到y(tǒng)引入的很多概念也適用于黑盒。黑盒規(guī)格說(shuō)明24狀態(tài)盒規(guī)格說(shuō)明

一個(gè)狀態(tài)是某個(gè)可觀查到的系統(tǒng)行為的模型。當(dāng)進(jìn)行處理時(shí)，一個(gè)系統(tǒng)對(duì)事件(觸發(fā))作出反應(yīng)，從當(dāng)前狀態(tài)轉(zhuǎn)換到某一新的狀態(tài)。當(dāng)進(jìn)行轉(zhuǎn)換時(shí)，可能發(fā)生某個(gè)動(dòng)作。狀態(tài)盒使用數(shù)據(jù)抽象來(lái)確定到下一個(gè)狀態(tài)的轉(zhuǎn)換、以及狀態(tài)轉(zhuǎn)換后將要發(fā)生的動(dòng)作(反應(yīng))。狀態(tài)盒規(guī)格說(shuō)明一個(gè)狀態(tài)是某個(gè)可觀查到的系統(tǒng)行為的模型。當(dāng)進(jìn)25狀態(tài)盒同黑盒協(xié)作。來(lái)自某外部源及一組內(nèi)部系統(tǒng)狀態(tài)T的觸發(fā)S被輸入到黑盒中。包含在狀態(tài)盒內(nèi)的黑盒的函數(shù)g的數(shù)學(xué)描述：g∶S*×T*→R×T這里g是和特定狀態(tài)t連接的子函數(shù)。當(dāng)整體地考慮時(shí)，狀態(tài)—子函數(shù)對(duì)(t，g)定義了黑盒函數(shù)f。狀態(tài)盒規(guī)格說(shuō)明

狀態(tài)盒規(guī)格說(shuō)明

狀態(tài)盒同黑盒協(xié)作。來(lái)自某外部源及一組內(nèi)部系統(tǒng)狀態(tài)T的觸發(fā)S被26清晰盒規(guī)格說(shuō)明

清晰盒規(guī)格說(shuō)明是與過(guò)程設(shè)計(jì)及結(jié)構(gòu)化編程緊密關(guān)聯(lián)的。狀態(tài)盒中的子函數(shù)g被實(shí)現(xiàn)g的結(jié)構(gòu)化編程結(jié)構(gòu)所替代。清晰盒規(guī)格說(shuō)明清晰盒規(guī)格說(shuō)明清晰盒規(guī)格說(shuō)明是與過(guò)程設(shè)計(jì)及結(jié)構(gòu)化編程緊密關(guān)2711.4凈室設(shè)計(jì)凈室軟件工程中使用的設(shè)計(jì)方法主要運(yùn)用結(jié)構(gòu)化程序設(shè)計(jì)的原理。基本的處理函數(shù)(在規(guī)格說(shuō)明的早期求精中描述)被精化，其方法是“將數(shù)學(xué)函數(shù)逐步擴(kuò)展為邏輯連接詞(如，if-then-else)和子函數(shù)構(gòu)成的結(jié)構(gòu)，這種擴(kuò)展一直進(jìn)行下去，直到所有標(biāo)識(shí)出來(lái)的子函數(shù)可以用程序設(shè)計(jì)語(yǔ)言直接表達(dá)”。11.4凈室設(shè)計(jì)凈室軟件工程中使用的設(shè)計(jì)方法主要運(yùn)用結(jié)構(gòu)化28設(shè)計(jì)求精與驗(yàn)證

每個(gè)清晰盒規(guī)格說(shuō)明代表了一個(gè)完成狀態(tài)盒轉(zhuǎn)換所需的過(guò)程(子函數(shù))的設(shè)計(jì)。對(duì)清晰盒規(guī)格說(shuō)明，使用結(jié)構(gòu)化程序設(shè)計(jì)結(jié)構(gòu)和逐步求精。一個(gè)程序函數(shù)f被細(xì)化為子函數(shù)g和h的序列，這些又被進(jìn)一步細(xì)化為條件結(jié)構(gòu)(if-then-else和do-while)。進(jìn)一步的求精給出了連續(xù)的邏輯細(xì)化。

設(shè)計(jì)求精與驗(yàn)證每個(gè)清晰盒規(guī)格說(shuō)明代表了一個(gè)完成狀態(tài)盒轉(zhuǎn)換所29在每個(gè)求精層次，凈室團(tuán)隊(duì)執(zhí)行一次形式化正確性驗(yàn)證。為此，將一類正確性條件集合附加到結(jié)構(gòu)化程序設(shè)計(jì)結(jié)構(gòu)上。如果函數(shù)f被擴(kuò)展為序列g(shù)和h，則f所有輸入的正確性條件是：執(zhí)行g(shù)之后再執(zhí)行h能完成f的功能嗎？如果一個(gè)函數(shù)p被精化為形為if＜c＞thenqelser的條件形式，則對(duì)p的所有輸入的正確性條件是：只要條件＜c＞為真，q能完成p的功能嗎？只要條件＜c＞為假，r能完成p的功能嗎？

設(shè)計(jì)求精與驗(yàn)證

在每個(gè)求精層次，凈室團(tuán)隊(duì)執(zhí)行一次形式化正確性驗(yàn)證。為此，將一30如果一個(gè)函數(shù)m被細(xì)化為循環(huán)donwhile＜c＞則對(duì)m的所有輸入的正確性條件是：能夠保證循環(huán)終止嗎？只要＜c＞為真，循環(huán)執(zhí)行n之后能完成m的功能嗎？只要＜c＞為假，退出循環(huán)仍能完成m的功能嗎？設(shè)計(jì)求精與驗(yàn)證

如果一個(gè)函數(shù)m被細(xì)化為循環(huán)設(shè)計(jì)求精與驗(yàn)證31每當(dāng)一個(gè)清晰盒被精化為下一個(gè)詳細(xì)層次時(shí)，都應(yīng)用上面給出的正確性條件。值得注意的是：結(jié)構(gòu)化程序設(shè)計(jì)結(jié)構(gòu)的使用限制了必須進(jìn)行的正確性測(cè)試的數(shù)量。對(duì)順序結(jié)構(gòu)只檢查單個(gè)條件，對(duì)if-then-else結(jié)構(gòu)只測(cè)試兩個(gè)條件，對(duì)循環(huán)則只驗(yàn)證三個(gè)條件。設(shè)計(jì)求精與驗(yàn)證

每當(dāng)一個(gè)清晰盒被精化為下一個(gè)詳細(xì)層次時(shí)，都應(yīng)用上面給出的正32例：過(guò)程設(shè)計(jì)的正確性驗(yàn)證：設(shè)計(jì)并驗(yàn)證一個(gè)小的程序，該程序?qū)δ辰o定的整數(shù)x，找出其平方根的整數(shù)部分y。

yesno設(shè)計(jì)求精與驗(yàn)證

例：過(guò)程設(shè)計(jì)的正確性驗(yàn)證：設(shè)計(jì)并驗(yàn)證一個(gè)小的程序，該程序?qū)δ?3定義入口和出口條件。為了證明設(shè)計(jì)的正確性，需要證明圖中表示的條件init、loop、cont、yes和exit在所有情形下都是正確的。設(shè)計(jì)求精與驗(yàn)證

定義入口和出口條件。設(shè)計(jì)求精與驗(yàn)證34

1.條件init要求［x≥0andy=0］。基于問(wèn)題的需求，假定入口條件是正確的。因此，init條件的第一部分x≥0是滿足的。在流程圖中，在init條件前的語(yǔ)句設(shè)置y=0，因此，init條件的第二部分也是滿足的，因此，init為真。1.條件init要求［x≥0andy=0］?；趩?wèn)352.條件loop可能以兩種方式之一出現(xiàn)：(1)直接從init(此時(shí)loop條件被直接滿足)，或(2)通過(guò)穿過(guò)條件cont的控制流。因?yàn)闂l件cont與條件loop相同，因此，不管從哪條路徑到達(dá)它，條件loop都為真。2.條件loop可能以兩種方式之一出現(xiàn)：(1)直接從init363.條件cont:只有在y值被遞增1后，才能遇到條件cont。另外，只有在條件yes也為真時(shí)，才能調(diào)用到達(dá)條件cont的控制流路徑。因此，如果(y+1)2≤x，則y2≤x，條件cont成立。3.條件cont:只有在y值被遞增1后，才能遇到條件cont374.條件yes在如圖所示的條件邏輯中被測(cè)試，因此，當(dāng)控制流沿著所示的路徑移動(dòng)時(shí)，條件yes一定為真。4.條件yes在如圖所示的條件邏輯中被測(cè)試，因此，當(dāng)控制流385.條件exit首先要求x保持不變，對(duì)設(shè)計(jì)進(jìn)行檢查可發(fā)現(xiàn)x沒(méi)有出現(xiàn)在賦值操作的左邊，沒(méi)有使用x的函數(shù)調(diào)用，因此，x保持不變。因?yàn)闂l件測(cè)試(y+1)2≤x不成立時(shí)，才可能到達(dá)條件exit，因此(y+1)2＞x成立。此外，loop條件還必須保持為真(即，y2≤x)，因此，(y+1)2＞x和y2≤x可以組合在一起滿足exit條件。5.條件exit首先要求x保持不變，對(duì)設(shè)計(jì)進(jìn)行檢查可發(fā)現(xiàn)39保證循環(huán)終止:因?yàn)閥是遞增的，而x≥0，因此，最后(y+1)2≤x不成立，循環(huán)一定終止。

設(shè)計(jì)求精與驗(yàn)證

保證循環(huán)終止:設(shè)計(jì)求精與驗(yàn)證40設(shè)計(jì)驗(yàn)證的優(yōu)點(diǎn)

對(duì)清晰盒設(shè)計(jì)的每一步求精進(jìn)行嚴(yán)格的正確性驗(yàn)證有許多顯著的優(yōu)點(diǎn)：(1)將驗(yàn)證簡(jiǎn)化為一個(gè)有限的過(guò)程。在清晰盒中，以嵌套的、順序的方式組織控制結(jié)構(gòu)，這就自然地定義了一個(gè)層次，該層次顯示了必須被驗(yàn)證的正確性條件。(2)再怎么強(qiáng)調(diào)將驗(yàn)證簡(jiǎn)化為有限過(guò)程對(duì)質(zhì)量產(chǎn)生的正面效果都不過(guò)分。除了那些最微不足道的程序，即使所有程序都具有無(wú)限數(shù)目的可執(zhí)行路徑，也可以在有限步驟內(nèi)對(duì)它們進(jìn)行驗(yàn)證。設(shè)計(jì)驗(yàn)證的優(yōu)點(diǎn)對(duì)清晰盒設(shè)計(jì)的每一步求精進(jìn)行嚴(yán)格的正確性驗(yàn)41(3)使得凈室團(tuán)隊(duì)驗(yàn)證設(shè)計(jì)和代碼的每一行。在正確性定理的基礎(chǔ)上，團(tuán)隊(duì)可以通過(guò)小組分析和討論來(lái)執(zhí)行驗(yàn)證，并且當(dāng)在生命關(guān)鍵或使命關(guān)鍵的系統(tǒng)中需要額外的信心時(shí)，可以生成書(shū)面的證明。(4)達(dá)到幾乎零缺陷的水平。在團(tuán)隊(duì)的復(fù)審過(guò)程中，每個(gè)控制結(jié)構(gòu)的每個(gè)正確性條件被依次驗(yàn)證。每個(gè)團(tuán)隊(duì)成員必須就每個(gè)條件都是正確的達(dá)成共識(shí)，這樣只有團(tuán)隊(duì)的每個(gè)成員均未能正確地驗(yàn)證某條件時(shí)，才有可能出現(xiàn)錯(cuò)誤。設(shè)計(jì)驗(yàn)證的優(yōu)點(diǎn)(3)使得凈室團(tuán)隊(duì)驗(yàn)證設(shè)計(jì)和代碼的每一行。在正確性定理的基礎(chǔ)42(5)具有可伸縮性。每個(gè)軟件系統(tǒng)，不管有多大，均具有頂層的由順序、選擇和循環(huán)結(jié)構(gòu)構(gòu)成的清晰盒過(guò)程。(6)產(chǎn)生出比采用單元測(cè)試更好的代碼。單元測(cè)試僅僅檢查從很多可能的路徑中選出的測(cè)試路徑的執(zhí)行效果?；诤瘮?shù)驗(yàn)證的理論，凈室方法可以驗(yàn)證所有數(shù)據(jù)的每個(gè)可能的結(jié)果，因?yàn)殡m然一個(gè)程序可能有很多可執(zhí)行路徑，但它只有一個(gè)函數(shù)。驗(yàn)證也比單元測(cè)試更有效，可以在幾分鐘之內(nèi)檢查大多數(shù)驗(yàn)證條件，但單元測(cè)試要花費(fèi)大量時(shí)間去準(zhǔn)備、執(zhí)行和檢查。設(shè)計(jì)驗(yàn)證的優(yōu)點(diǎn)(5)具有可伸縮性。每個(gè)軟件系統(tǒng)，不管有多大，均具有頂層的由4311.5凈室測(cè)試凈室測(cè)試的策略在根本上不同于傳統(tǒng)測(cè)試方法。傳統(tǒng)測(cè)試方法導(dǎo)出一組測(cè)試用例發(fā)現(xiàn)設(shè)計(jì)和編碼錯(cuò)誤；凈室測(cè)試的目的是：通過(guò)證明用例的統(tǒng)計(jì)樣本的成功運(yùn)行來(lái)確認(rèn)軟件需求。11.5凈室測(cè)試凈室測(cè)試的策略在根本上不同于傳統(tǒng)測(cè)試方法。44統(tǒng)計(jì)使用測(cè)試計(jì)算機(jī)程序的用戶沒(méi)有必要去了解設(shè)計(jì)的技術(shù)細(xì)節(jié)。程序的用戶可見(jiàn)的行為通常是由用戶產(chǎn)生的輸入和事件所驅(qū)動(dòng)的。在復(fù)雜系統(tǒng)中，輸入和事件的可能的范圍(即用例)是非常廣泛的。什么樣的用例子集能夠充分驗(yàn)證程序的行為？這是統(tǒng)計(jì)使用測(cè)試關(guān)注的第一個(gè)問(wèn)題。統(tǒng)計(jì)使用測(cè)試計(jì)算機(jī)程序的用戶沒(méi)有必要去了解設(shè)計(jì)的技術(shù)細(xì)節(jié)。45統(tǒng)計(jì)使用測(cè)試“等同于以用戶試圖使用軟件的方式來(lái)測(cè)試軟件”。為了完成測(cè)試工作，凈室測(cè)試團(tuán)隊(duì)（也稱為認(rèn)證團(tuán)隊(duì)）必須確定軟件的使用概率分布。對(duì)軟件的每個(gè)增量的規(guī)格說(shuō)明(黑盒)進(jìn)行分析，并定義一組使軟件改變其行為的觸發(fā)(輸入或事件)。通過(guò)與潛在用戶的交流、使用場(chǎng)景的建立、及對(duì)應(yīng)用領(lǐng)域的全面了解，為每個(gè)觸發(fā)分配一個(gè)使用概率。按照使用概率分布為每個(gè)觸發(fā)集合生成測(cè)試用例。統(tǒng)計(jì)使用測(cè)試

統(tǒng)計(jì)使用測(cè)試“等同于以用戶試圖使用軟件的方式來(lái)測(cè)試軟件”。為46例，在家庭保安系統(tǒng)中，使用凈室軟件工程方法開(kāi)發(fā)一個(gè)軟件增量來(lái)管理用戶與安全系統(tǒng)鍵區(qū)之間的交互。對(duì)這個(gè)增量，已經(jīng)標(biāo)識(shí)出5個(gè)觸發(fā)。通過(guò)分析，給出每個(gè)觸發(fā)的概率分布百分?jǐn)?shù)。為了更容易地選擇測(cè)試用例，這些概率被映射到1至99的數(shù)字區(qū)間。

統(tǒng)計(jì)使用測(cè)試

例，在家庭保安系統(tǒng)中，使用凈室軟件工程方法開(kāi)發(fā)一個(gè)軟件增量來(lái)47為了生成符合使用概率分布的使用測(cè)試用例序列，生成1至99之間的隨機(jī)數(shù)。每個(gè)隨機(jī)數(shù)與前面概率分布的一個(gè)區(qū)間相對(duì)應(yīng)。因此，使用測(cè)試用例序列可以隨機(jī)定義，但又與觸發(fā)發(fā)生的適當(dāng)概率相對(duì)應(yīng)。例如，假定生成了下面的隨機(jī)數(shù)序列：13-94-22-24-45-5681-19-31-69-45-938-21-52-84-86-4統(tǒng)計(jì)使用測(cè)試

為了生成符合使用概率分布的使用測(cè)試用例序列，生成1至99之間48根據(jù)表中顯示的分布區(qū)間選擇適當(dāng)?shù)挠|發(fā)，從而導(dǎo)出下面的用例：AD-T-AD-AD-AD-ZST-AD-AD-AD-Q-AD-ADAD-AD-ZS-T-T-AD測(cè)試團(tuán)隊(duì)執(zhí)行這些測(cè)試用例，并對(duì)照系統(tǒng)的規(guī)格說(shuō)明來(lái)驗(yàn)證軟件的行為。記錄測(cè)試所用的時(shí)間,使得可以確定間隔時(shí)間。利用間隔時(shí)間，認(rèn)證團(tuán)隊(duì)可以計(jì)算出平均失效時(shí)間MTTF。如果進(jìn)行一個(gè)很長(zhǎng)的測(cè)試序列，沒(méi)有出現(xiàn)故障，則MTTF較低，軟件可靠性較高。統(tǒng)計(jì)使用測(cè)試

根據(jù)表中顯示的分布區(qū)間選擇適當(dāng)?shù)挠|發(fā)，從而導(dǎo)出下面的用例：統(tǒng)4911.6認(rèn)證在凈室軟件工程方法中，認(rèn)證意味著可以描述每個(gè)構(gòu)件的可靠性(用平均失效時(shí)間MTTF來(lái)度量)可認(rèn)證的軟件構(gòu)件的潛在影響遠(yuǎn)遠(yuǎn)超出了單個(gè)凈室項(xiàng)目的范圍，可復(fù)用的軟件構(gòu)件可以和它們的使用場(chǎng)景、程序觸發(fā)、以及概率分布一起存儲(chǔ)。在描述的使用場(chǎng)景和測(cè)試體系下，每個(gè)構(gòu)件都具有一個(gè)經(jīng)過(guò)認(rèn)證的可靠性。11.6認(rèn)證在凈室軟件工程方法中，認(rèn)證意味著可以描述每個(gè)構(gòu)50認(rèn)證方法包括5個(gè)步驟：1.必須創(chuàng)建使用場(chǎng)景。2.說(shuō)明使用剖面。3.從剖面中生成測(cè)試用例。4.執(zhí)行測(cè)試，記錄并分析失效數(shù)據(jù)。5.計(jì)算并認(rèn)證可靠性。11.6認(rèn)證認(rèn)證方法包括5個(gè)步驟：11.6認(rèn)證51可靠性認(rèn)證需要?jiǎng)?chuàng)建三個(gè)模型：取樣模型。軟件測(cè)試執(zhí)行m個(gè)隨機(jī)測(cè)試用例，如果沒(méi)有錯(cuò)誤發(fā)生或只有少于指定數(shù)量的錯(cuò)誤發(fā)生，則通過(guò)認(rèn)證。構(gòu)件模型。對(duì)由n個(gè)構(gòu)件組成的系統(tǒng)進(jìn)行認(rèn)證，構(gòu)件模型使得分析員能夠確定構(gòu)件i在完成前失效的概率。認(rèn)證模型。設(shè)計(jì)并認(rèn)證系統(tǒng)的整體可靠性。11.6認(rèn)證可靠性認(rèn)證需要?jiǎng)?chuàng)建三個(gè)模型：11.6認(rèn)證52That'sAll!That'sAll!53第11章凈室軟件工程基本概念凈室策略功能規(guī)格說(shuō)明凈室設(shè)計(jì)凈室測(cè)試認(rèn)證第11章凈室軟件工程基本概念5411.1基本概念凈室軟件工程(Cleanroomsoftwareengineering)是一種在軟件開(kāi)發(fā)過(guò)程中強(qiáng)調(diào)在軟件中建立正確性要求的方法。與傳統(tǒng)的分析、設(shè)計(jì)、編碼、測(cè)試和調(diào)試的周期觀點(diǎn)有所不同。11.1基本概念凈室軟件工程(Cleanroomsoft55凈室方法的觀點(diǎn)：

通過(guò)在第一次正確地書(shū)寫(xiě)代碼增量，并在測(cè)試前驗(yàn)證它們的正確性來(lái)避免成本很高的缺陷消除過(guò)程。它的過(guò)程模型是在代碼增量集成到系統(tǒng)的同時(shí)，進(jìn)行代碼增量的統(tǒng)計(jì)質(zhì)量驗(yàn)證。11.1基本概念凈室方法的觀點(diǎn)：11.1基本概念56與形式化方法技術(shù)一樣，凈室過(guò)程強(qiáng)調(diào)規(guī)格說(shuō)明和設(shè)計(jì)上的嚴(yán)格性，并且使用基于數(shù)學(xué)的正確性證明來(lái)對(duì)結(jié)果設(shè)計(jì)模型的每個(gè)元素進(jìn)行形式化驗(yàn)證。凈室方法不是先制造一個(gè)產(chǎn)品，然后再去消除缺陷，而是要求在規(guī)格說(shuō)明和設(shè)計(jì)中消除錯(cuò)誤，然后以“干凈”的方式進(jìn)行制造。凈室方法還對(duì)形式化方法進(jìn)行了擴(kuò)展，強(qiáng)調(diào)統(tǒng)計(jì)質(zhì)量控制技術(shù)，包括基于客戶對(duì)軟件的預(yù)期使用的測(cè)試。11.1基本概念與形式化方法技術(shù)一樣，凈室過(guò)程強(qiáng)調(diào)規(guī)格說(shuō)明和設(shè)計(jì)上的嚴(yán)格性57“第一次就將事情做正確”是軟件工程最重要的哲學(xué)。凈室軟件工程是這樣一個(gè)過(guò)程：它強(qiáng)調(diào)在程序構(gòu)造開(kāi)始前進(jìn)行正確性的數(shù)學(xué)驗(yàn)證，并且將軟件可靠性認(rèn)證作為軟件測(cè)試的一部分。其底線是極低的故障率，這是使用非形式化方法難于或不可能達(dá)到的。11.1基本概念“第一次就將事情做正確”是軟件工程最重要的哲學(xué)。11.1基5820世紀(jì)80年代，Mills、Dyer、及Linger最先建議將凈室原理應(yīng)用于軟件工程。雖然在軟件開(kāi)發(fā)的早期，人們對(duì)其抱以很大的希望，但它并沒(méi)有得到廣泛的使用。

11.1基本概念20世紀(jì)80年代，Mills、Dyer、及Linger最先建59

Henderson提出了沒(méi)有得到廣泛使用的三個(gè)原因：1.凈室方法學(xué)太理論化、太數(shù)學(xué)化、太激進(jìn)，難于在實(shí)際的軟件開(kāi)發(fā)中使用。2.它提倡開(kāi)發(fā)者不需要進(jìn)行單元測(cè)試，而是進(jìn)行正確性驗(yàn)證和統(tǒng)計(jì)質(zhì)量控制，這些觀念與當(dāng)前大多數(shù)軟件開(kāi)發(fā)方式有很大的偏離。11.1基本概念Henderson提出了沒(méi)有得到廣泛使用的三個(gè)原因：11603.軟件開(kāi)發(fā)產(chǎn)業(yè)的成熟度不高。使用凈室過(guò)程需要在整個(gè)生命周期階段嚴(yán)格按照定義的過(guò)程進(jìn)行。由于大多數(shù)軟件企業(yè)的運(yùn)作還處于過(guò)程成熟度中的較低級(jí)別，軟件工程師還沒(méi)有準(zhǔn)備應(yīng)用凈室技術(shù)。11.1基本概念3.軟件開(kāi)發(fā)產(chǎn)業(yè)的成熟度不高。使用凈室過(guò)程需要在整個(gè)生命周期61“程序中出現(xiàn)錯(cuò)誤的唯一方式是作者將錯(cuò)誤引入進(jìn)去的。沒(méi)有其他方式……正確實(shí)踐的目標(biāo)是：設(shè)法避免引入錯(cuò)誤，如果引入了錯(cuò)誤，通過(guò)測(cè)試或任何其他運(yùn)行程序的方式來(lái)消除錯(cuò)誤。”

HarlanMills11.1基本概念11.1基本概念6211.2凈室策略凈室方法使用增量過(guò)程模型。一個(gè)“軟件增量的流水線”由若干小的、獨(dú)立的軟件團(tuán)隊(duì)開(kāi)發(fā)。每當(dāng)一個(gè)軟件增量通過(guò)認(rèn)證，它就被集成到整體系統(tǒng)中。因此，系統(tǒng)的功能隨時(shí)間增加。11.2凈室策略凈室方法使用增量過(guò)程模型。63一旦將功能分配給系統(tǒng)的軟件元素，則可啟動(dòng)凈室增量的流水線。需要完成的任務(wù)如下：

(1)增量策劃。制定一個(gè)采用增量策略的項(xiàng)目計(jì)劃，確定每個(gè)增量的功能、預(yù)計(jì)規(guī)模、及凈室開(kāi)發(fā)進(jìn)度。(2)需求收集。為每個(gè)增量開(kāi)發(fā)更詳細(xì)的客戶級(jí)需求描述。

11.2凈室策略一旦將功能分配給系統(tǒng)的軟件元素，則可啟動(dòng)凈室增量的流水線。需64(3)盒結(jié)構(gòu)規(guī)格說(shuō)明。運(yùn)用盒結(jié)構(gòu)的規(guī)格說(shuō)明方法描述功能規(guī)格說(shuō)明。遵從操作分析原則，盒結(jié)構(gòu)“在每一個(gè)精化級(jí)別上使行為、數(shù)據(jù)及過(guò)程的創(chuàng)造性定義獨(dú)立”。(4)形式化設(shè)計(jì)。使用盒結(jié)構(gòu)方法，凈室設(shè)計(jì)是規(guī)格說(shuō)明的自然、無(wú)縫擴(kuò)展。對(duì)規(guī)格說(shuō)明(稱為黑盒)進(jìn)行迭代求精(在一個(gè)增量?jī)?nèi))類似于體系結(jié)構(gòu)設(shè)計(jì)和構(gòu)件級(jí)設(shè)計(jì)(分別稱為“狀態(tài)盒”和“清晰盒”)。

11.2凈室策略(3)盒結(jié)構(gòu)規(guī)格說(shuō)明。運(yùn)用盒結(jié)構(gòu)的規(guī)格說(shuō)明方法描述功能規(guī)格說(shuō)65(5)正確性驗(yàn)證。凈室團(tuán)隊(duì)對(duì)設(shè)計(jì)及代碼進(jìn)行一系列嚴(yán)格的正確性驗(yàn)證活動(dòng)。驗(yàn)證從最高層次的盒結(jié)構(gòu)(規(guī)格說(shuō)明)開(kāi)始，然后移向設(shè)計(jì)細(xì)節(jié)和代碼。正確性驗(yàn)證的第一層次通過(guò)應(yīng)用一組“正確性問(wèn)題”來(lái)進(jìn)行，如果這些沒(méi)有證明規(guī)格說(shuō)明是正確的，則使用更形式化的(數(shù)學(xué)的)驗(yàn)證方法。11.2凈室策略(5)正確性驗(yàn)證。凈室團(tuán)隊(duì)對(duì)設(shè)計(jì)及代碼進(jìn)行一系列嚴(yán)格的正確66(6)代碼生成、檢查和驗(yàn)證。以某種專門(mén)語(yǔ)言表示的盒結(jié)構(gòu)規(guī)格說(shuō)明被翻譯為適當(dāng)?shù)某绦蛟O(shè)計(jì)語(yǔ)言。然后，使用標(biāo)準(zhǔn)的走查或檢查技術(shù)來(lái)保證代碼和盒結(jié)構(gòu)的語(yǔ)義相符性，以及代碼的語(yǔ)法正確性。最后，對(duì)源代碼進(jìn)行正確性驗(yàn)證。

11.2凈室策略(6)代碼生成、檢查和驗(yàn)證。以某種專門(mén)語(yǔ)言表示的盒結(jié)構(gòu)規(guī)格說(shuō)67(7)統(tǒng)計(jì)測(cè)試規(guī)劃。分析軟件的預(yù)計(jì)使用情況，規(guī)劃并設(shè)計(jì)一組測(cè)試用例，以測(cè)試使用情況的“概率分布”。

11.2凈室策略(7)統(tǒng)計(jì)測(cè)試規(guī)劃。分析軟件的預(yù)計(jì)使用情況，規(guī)劃并設(shè)計(jì)一組測(cè)68(8)統(tǒng)計(jì)使用測(cè)試。對(duì)計(jì)算機(jī)軟件進(jìn)行窮舉測(cè)試是不可能的，因此，設(shè)計(jì)有限數(shù)量的測(cè)試用例總是必要的。統(tǒng)計(jì)使用技術(shù)執(zhí)行由統(tǒng)計(jì)樣本導(dǎo)出的一系列測(cè)試，這里的統(tǒng)計(jì)樣本是從來(lái)自目標(biāo)人群的所有用戶對(duì)程序的所有可能執(zhí)行中抽取的。11.2凈室策略(8)統(tǒng)計(jì)使用測(cè)試。11.2凈室策略69(9)認(rèn)證。一旦完成驗(yàn)證、檢查和使用測(cè)試(并且所有錯(cuò)誤被改正)，則對(duì)增量進(jìn)行集成前的認(rèn)證工作。

11.2凈室策略(9)認(rèn)證。一旦完成驗(yàn)證、檢查和使用測(cè)試(并且所有錯(cuò)誤被70凈室方法的特異之處

明確使用統(tǒng)計(jì)質(zhì)量控制。使用基于數(shù)學(xué)的正確性證明來(lái)驗(yàn)證設(shè)計(jì)規(guī)格說(shuō)明。實(shí)現(xiàn)了一些測(cè)試技術(shù)，這些測(cè)試技術(shù)最有可能揭示具有嚴(yán)重影響的錯(cuò)誤。

凈室方法的特異之處明確使用統(tǒng)計(jì)質(zhì)量控制。71凈室軟件工程和傳統(tǒng)軟件實(shí)踐的差別在于：它不再?gòu)?qiáng)調(diào)(有些人稱取消)單元測(cè)試和調(diào)試的作用，從而大量地減少(或取消)由軟件開(kāi)發(fā)者所承擔(dān)的測(cè)試工作量。在凈室軟件工程中，單元測(cè)試和調(diào)試被正確性驗(yàn)證和基于統(tǒng)計(jì)的測(cè)試所替代。凈室方法的特異之處

凈室軟件工程和傳統(tǒng)軟件實(shí)踐的差別在于：它不再?gòu)?qiáng)調(diào)(有些人稱取7211.3功能規(guī)格說(shuō)明不管選擇哪種分析方法，操作分析原理總是適用的。對(duì)數(shù)據(jù)、功能和行為建模，并對(duì)結(jié)果模型進(jìn)行分解,提供更進(jìn)一步的詳細(xì)信息?？傮w目標(biāo)是從捕獲問(wèn)題實(shí)質(zhì)的規(guī)格說(shuō)明(模型)移向提供重要實(shí)現(xiàn)細(xì)節(jié)的規(guī)格說(shuō)明。11.3功能規(guī)格說(shuō)明不管選擇哪種分析方法，操作分析原理總是73凈室軟件工程通過(guò)使用盒結(jié)構(gòu)規(guī)格說(shuō)明的方法來(lái)遵從操作分析原則。一個(gè)“盒”在某個(gè)細(xì)節(jié)層次上封裝系統(tǒng)(或系統(tǒng)的某些方面)。通過(guò)逐步求精的過(guò)程，盒被精化為層次?！懊總€(gè)盒規(guī)格說(shuō)明的信息內(nèi)容足以定義其精化，不需要依賴任何其他盒的實(shí)現(xiàn)”。這使得分析員能夠按層次劃分一個(gè)系統(tǒng)——從頂層的基本表示到底層實(shí)現(xiàn)的特定細(xì)節(jié)。11.3功能規(guī)格說(shuō)明凈室軟件工程通過(guò)使用盒結(jié)構(gòu)規(guī)格說(shuō)明的方法來(lái)遵從操作分析原則。74有三種類型的盒：黑盒，狀態(tài)盒，清晰盒

黑盒。黑盒刻畫(huà)系統(tǒng)行為或系統(tǒng)部件的行為。通過(guò)運(yùn)用由觸發(fā)映射到反應(yīng)的一組轉(zhuǎn)換規(guī)則，系統(tǒng)(或部件)對(duì)特定的觸發(fā)(事件)做出反應(yīng)。

狀態(tài)盒。狀態(tài)盒以類似于對(duì)象的方式封裝狀態(tài)數(shù)據(jù)和服務(wù)(操作)。在這種規(guī)格說(shuō)明視圖中，表示出狀態(tài)盒的輸入(觸發(fā))和輸出(反應(yīng))。清晰盒。在清晰盒中定義狀態(tài)盒所蘊(yùn)含的轉(zhuǎn)換功能，簡(jiǎn)單地說(shuō)，清晰盒包含了對(duì)狀態(tài)盒的過(guò)程設(shè)計(jì)。11.3功能規(guī)格說(shuō)明有三種類型的盒：黑盒，狀態(tài)盒，清晰盒11.3功能規(guī)格說(shuō)75黑盒規(guī)格說(shuō)明

黑盒規(guī)格說(shuō)明描述一種抽象、觸發(fā)和反應(yīng)。函數(shù)f被應(yīng)用到輸入(觸發(fā))S的序列S*，并將它們變換為輸出(反應(yīng))R。對(duì)于簡(jiǎn)單的軟件構(gòu)件，f可以是一個(gè)數(shù)學(xué)函數(shù)，但一般情況下，使用自然語(yǔ)言(或形式化規(guī)格說(shuō)明語(yǔ)言)描述f。黑盒規(guī)格說(shuō)明黑盒規(guī)格說(shuō)明黑盒規(guī)格說(shuō)明描述一種抽象、觸發(fā)和反應(yīng)。函數(shù)f被76為面向?qū)ο笙到y(tǒng)引入的很多概念也適用于黑盒。黑盒封裝數(shù)據(jù)抽象和操縱抽象數(shù)據(jù)的操作。和類層次一樣，黑盒規(guī)約可以展示使用層次，其中，低層盒從樹(shù)結(jié)構(gòu)中的高層盒繼承屬性。黑盒規(guī)格說(shuō)明

為面向?qū)ο笙到y(tǒng)引入的很多概念也適用于黑盒。黑盒規(guī)格說(shuō)明77狀態(tài)盒規(guī)格說(shuō)明

一個(gè)狀態(tài)是某個(gè)可觀查到的系統(tǒng)行為的模型。當(dāng)進(jìn)行處理時(shí)，一個(gè)系統(tǒng)對(duì)事件(觸發(fā))作出反應(yīng)，從當(dāng)前狀態(tài)轉(zhuǎn)換到某一新的狀態(tài)。當(dāng)進(jìn)行轉(zhuǎn)換時(shí)，可能發(fā)生某個(gè)動(dòng)作。狀態(tài)盒使用數(shù)據(jù)抽象來(lái)確定到下一個(gè)狀態(tài)的轉(zhuǎn)換、以及狀態(tài)轉(zhuǎn)換后將要發(fā)生的動(dòng)作(反應(yīng))。狀態(tài)盒規(guī)格說(shuō)明一個(gè)狀態(tài)是某個(gè)可觀查到的系統(tǒng)行為的模型。當(dāng)進(jìn)78狀態(tài)盒同黑盒協(xié)作。來(lái)自某外部源及一組內(nèi)部系統(tǒng)狀態(tài)T的觸發(fā)S被輸入到黑盒中。包含在狀態(tài)盒內(nèi)的黑盒的函數(shù)g的數(shù)學(xué)描述：g∶S*×T*→R×T這里g是和特定狀態(tài)t連接的子函數(shù)。當(dāng)整體地考慮時(shí)，狀態(tài)—子函數(shù)對(duì)(t，g)定義了黑盒函數(shù)f。狀態(tài)盒規(guī)格說(shuō)明

狀態(tài)盒規(guī)格說(shuō)明

狀態(tài)盒同黑盒協(xié)作。來(lái)自某外部源及一組內(nèi)部系統(tǒng)狀態(tài)T的觸發(fā)S被79清晰盒規(guī)格說(shuō)明

清晰盒規(guī)格說(shuō)明是與過(guò)程設(shè)計(jì)及結(jié)構(gòu)化編程緊密關(guān)聯(lián)的。狀態(tài)盒中的子函數(shù)g被實(shí)現(xiàn)g的結(jié)構(gòu)化編程結(jié)構(gòu)所替代。清晰盒規(guī)格說(shuō)明清晰盒規(guī)格說(shuō)明清晰盒規(guī)格說(shuō)明是與過(guò)程設(shè)計(jì)及結(jié)構(gòu)化編程緊密關(guān)8011.4凈室設(shè)計(jì)凈室軟件工程中使用的設(shè)計(jì)方法主要運(yùn)用結(jié)構(gòu)化程序設(shè)計(jì)的原理?；镜奶幚砗瘮?shù)(在規(guī)格說(shuō)明的早期求精中描述)被精化，其方法是“將數(shù)學(xué)函數(shù)逐步擴(kuò)展為邏輯連接詞(如，if-then-else)和子函數(shù)構(gòu)成的結(jié)構(gòu)，這種擴(kuò)展一直進(jìn)行下去，直到所有標(biāo)識(shí)出來(lái)的子函數(shù)可以用程序設(shè)計(jì)語(yǔ)言直接表達(dá)”。11.4凈室設(shè)計(jì)凈室軟件工程中使用的設(shè)計(jì)方法主要運(yùn)用結(jié)構(gòu)化81設(shè)計(jì)求精與驗(yàn)證

每個(gè)清晰盒規(guī)格說(shuō)明代表了一個(gè)完成狀態(tài)盒轉(zhuǎn)換所需的過(guò)程(子函數(shù))的設(shè)計(jì)。對(duì)清晰盒規(guī)格說(shuō)明，使用結(jié)構(gòu)化程序設(shè)計(jì)結(jié)構(gòu)和逐步求精。一個(gè)程序函數(shù)f被細(xì)化為子函數(shù)g和h的序列，這些又被進(jìn)一步細(xì)化為條件結(jié)構(gòu)(if-then-else和do-while)。進(jìn)一步的求精給出了連續(xù)的邏輯細(xì)化。

設(shè)計(jì)求精與驗(yàn)證每個(gè)清晰盒規(guī)格說(shuō)明代表了一個(gè)完成狀態(tài)盒轉(zhuǎn)換所82在每個(gè)求精層次，凈室團(tuán)隊(duì)執(zhí)行一次形式化正確性驗(yàn)證。為此，將一類正確性條件集合附加到結(jié)構(gòu)化程序設(shè)計(jì)結(jié)構(gòu)上。如果函數(shù)f被擴(kuò)展為序列g(shù)和h，則f所有輸入的正確性條件是：執(zhí)行g(shù)之后再執(zhí)行h能完成f的功能嗎？如果一個(gè)函數(shù)p被精化為形為if＜c＞thenqelser的條件形式，則對(duì)p的所有輸入的正確性條件是：只要條件＜c＞為真，q能完成p的功能嗎？只要條件＜c＞為假，r能完成p的功能嗎？

設(shè)計(jì)求精與驗(yàn)證

在每個(gè)求精層次，凈室團(tuán)隊(duì)執(zhí)行一次形式化正確性驗(yàn)證。為此，將一83如果一個(gè)函數(shù)m被細(xì)化為循環(huán)donwhile＜c＞則對(duì)m的所有輸入的正確性條件是：能夠保證循環(huán)終止嗎？只要＜c＞為真，循環(huán)執(zhí)行n之后能完成m的功能嗎？只要＜c＞為假，退出循環(huán)仍能完成m的功能嗎？設(shè)計(jì)求精與驗(yàn)證

如果一個(gè)函數(shù)m被細(xì)化為循環(huán)設(shè)計(jì)求精與驗(yàn)證84每當(dāng)一個(gè)清晰盒被精化為下一個(gè)詳細(xì)層次時(shí)，都應(yīng)用上面給出的正確性條件。值得注意的是：結(jié)構(gòu)化程序設(shè)計(jì)結(jié)構(gòu)的使用限制了必須進(jìn)行的正確性測(cè)試的數(shù)量。對(duì)順序結(jié)構(gòu)只檢查單個(gè)條件，對(duì)if-then-else結(jié)構(gòu)只測(cè)試兩個(gè)條件，對(duì)循環(huán)則只驗(yàn)證三個(gè)條件。設(shè)計(jì)求精與驗(yàn)證

每當(dāng)一個(gè)清晰盒被精化為下一個(gè)詳細(xì)層次時(shí)，都應(yīng)用上面給出的正85例：過(guò)程設(shè)計(jì)的正確性驗(yàn)證：設(shè)計(jì)并驗(yàn)證一個(gè)小的程序，該程序?qū)δ辰o定的整數(shù)x，找出其平方根的整數(shù)部分y。

yesno設(shè)計(jì)求精與驗(yàn)證

例：過(guò)程設(shè)計(jì)的正確性驗(yàn)證：設(shè)計(jì)并驗(yàn)證一個(gè)小的程序，該程序?qū)δ?6定義入口和出口條件。為了證明設(shè)計(jì)的正確性，需要證明圖中表示的條件init、loop、cont、yes和exit在所有情形下都是正確的。設(shè)計(jì)求精與驗(yàn)證

定義入口和出口條件。設(shè)計(jì)求精與驗(yàn)證87

1.條件init要求［x≥0andy=0］。基于問(wèn)題的需求，假定入口條件是正確的。因此，init條件的第一部分x≥0是滿足的。在流程圖中，在init條件前的語(yǔ)句設(shè)置y=0，因此，init條件的第二部分也是滿足的，因此，init為真。1.條件init要求［x≥0andy=0］?；趩?wèn)882.條件loop可能以兩種方式之一出現(xiàn)：(1)直接從init(此時(shí)loop條件被直接滿足)，或(2)通過(guò)穿過(guò)條件cont的控制流。因?yàn)闂l件cont與條件loop相同，因此，不管從哪條路徑到達(dá)它，條件loop都為真。2.條件loop可能以兩種方式之一出現(xiàn)：(1)直接從init893.條件cont:只有在y值被遞增1后，才能遇到條件cont。另外，只有在條件yes也為真時(shí)，才能調(diào)用到達(dá)條件cont的控制流路徑。因此，如果(y+1)2≤x，則y2≤x，條件cont成立。3.條件cont:只有在y值被遞增1后，才能遇到條件cont904.條件yes在如圖所示的條件邏輯中被測(cè)試，因此，當(dāng)控制流沿著所示的路徑移動(dòng)時(shí)，條件yes一定為真。4.條件yes在如圖所示的條件邏輯中被測(cè)試，因此，當(dāng)控制流915.條件exit首先要求x保持不變，對(duì)設(shè)計(jì)進(jìn)行檢查可發(fā)現(xiàn)x沒(méi)有出現(xiàn)在賦值操作的左邊，沒(méi)有使用x的函數(shù)調(diào)用，因此，x保持不變。因?yàn)闂l件測(cè)試(y+1)2≤x不成立時(shí)，才可能到達(dá)條件exit，因此(y+1)2＞x成立。此外，loop條件還必須保持為真(即，y2≤x)，因此，(y+1)2＞x和y2≤x可以組合在一起滿足exit條件。5.條件exit首先要求x保持不變，對(duì)設(shè)計(jì)進(jìn)行檢查可發(fā)現(xiàn)92保證循環(huán)終止:因?yàn)閥是遞增的，而x≥0，因此，最后(y+1)2≤x不成立，循環(huán)一定終止。

設(shè)計(jì)求精與驗(yàn)證

保證循環(huán)終止:設(shè)計(jì)求精與驗(yàn)證93設(shè)計(jì)驗(yàn)證的優(yōu)點(diǎn)

對(duì)清晰盒設(shè)計(jì)的每一步求精進(jìn)行嚴(yán)格的正確性驗(yàn)證有許多顯著的優(yōu)點(diǎn)：(1)將驗(yàn)證簡(jiǎn)化為一個(gè)有限的過(guò)程。在清晰盒中，以嵌套的、順序的方式組織控制結(jié)構(gòu)，這就自然地定義了一個(gè)層次，該層次顯示了必須被驗(yàn)證的正確性條件。(2)再怎么強(qiáng)調(diào)將驗(yàn)證簡(jiǎn)化為有限過(guò)程對(duì)質(zhì)量產(chǎn)生的正面效果都不過(guò)分。除了那些最微不足道的程序，即使所有程序都具有無(wú)限數(shù)目的可執(zhí)行路徑，也可以在有限步驟內(nèi)對(duì)它們進(jìn)行驗(yàn)證。設(shè)計(jì)驗(yàn)證的優(yōu)點(diǎn)對(duì)清晰盒設(shè)計(jì)的每一步求精進(jìn)行嚴(yán)格的正確性驗(yàn)94(3)使得凈室團(tuán)隊(duì)驗(yàn)證設(shè)計(jì)和代碼的每一行。在正確性定理的基礎(chǔ)上，團(tuán)隊(duì)可以通過(guò)小組分析和討論來(lái)執(zhí)行驗(yàn)證，并且當(dāng)在生命關(guān)鍵或使命關(guān)鍵的系統(tǒng)中需要額外的信心時(shí)，可以生成書(shū)面的證明。(4)達(dá)到幾乎零缺陷的水平。在團(tuán)隊(duì)的復(fù)審過(guò)程中，每個(gè)控制結(jié)構(gòu)的每個(gè)正確性條件被依次驗(yàn)證。每個(gè)團(tuán)隊(duì)成員必須就每個(gè)條件都是正確的達(dá)成共識(shí)，這樣只有團(tuán)隊(duì)的每個(gè)成員均未能正確地驗(yàn)證某條件時(shí)，才有可能出現(xiàn)錯(cuò)誤。設(shè)計(jì)驗(yàn)證的優(yōu)點(diǎn)(3)使得凈室團(tuán)隊(duì)驗(yàn)證設(shè)計(jì)和代碼的每一行。在正確性定理的基礎(chǔ)95(5)具有可伸縮性。每個(gè)軟件系統(tǒng)，不管有多大，均具有頂層的由順序、選擇和循環(huán)結(jié)構(gòu)構(gòu)成的清晰盒過(guò)程。(6)產(chǎn)生出比采用單元測(cè)試更好的代碼。單元測(cè)試僅僅檢查從很多可能的路徑中選出的測(cè)試路徑的執(zhí)行效果?；诤瘮?shù)驗(yàn)證的理論，凈室方法可以驗(yàn)證所有數(shù)據(jù)的每個(gè)可能的結(jié)果，因?yàn)殡m然一個(gè)程序可能有很多可執(zhí)行路徑，但它只有一個(gè)函數(shù)。驗(yàn)證也比單元測(cè)試更有效，可以在幾分鐘之內(nèi)檢查大多數(shù)驗(yàn)證條件，但單元測(cè)試要花費(fèi)大量