evel 功能 過程 計算 bug 有效 開發 計算機 符號

第6章 敏捷流程 —— 6.5 敏捷的故事

　　這一小節中有一個圖表，對比了敏捷（Agile）、計劃驅動（Plan-driven）、形式化的開發方法（Formal Method）的適用範圍。裏面提到的形式化的開發方法，其基本步驟是怎樣的呢？為什麽它能有極高的可靠性呢？下面是一些關於形式化方法特點的說明，從中可以看出它能力的緣由。

　　形式化方法建立在嚴格的數學基礎上，其目標是希望能使系統具有較高的可信度和正確性，並能使系統具有良好的結構，使其易維護，關鍵是能較好地滿足用戶需求。“形式化方法”一詞雖然一直被廣泛地應用，但在不同程度上，因理解不同，使其具有了不同的含義。一般說來，形式化方法是指具有堅實數學基礎的方法，它是數學上的綜合、分析技術的應用，用於開發計算機控制的系統，經常有推理工具的支持，它可提供一個用於模型設計和分析的一個嚴格而有效的途徑。

　　形式符號系統具有一定的數學性質，所以它們非二義性的基礎在於其內在的數學結構。越是復雜的數學概念，越是建立在更原始的概念之上，如：集合、命題邏輯。這就是說，形式符號系統可以具有合適的解釋，並在理論上足以確保規範的一致性解釋。 形式規範是由一些精確的定義組成的，因為其符號系統的含義是明確定義的。相對地，若將英語作為交流媒體，將很難得到精確的規範。精確規範的直接益處在於：它能減少規範中的二義性和誤解釋的可能性（危險）。精確是形式化方法或形式符號系統的一個特征，是產生無二義性規範的主要依據。另外，形式規範主要的語用益處在於：可以對形式規範進行較詳細的構造性檢查，因為對此規範中的具體內容的含義不會有爭議，有爭議的只是內容的完備性。換句話說，精確有助於確認和交流。 由於適當的形式機制的使用，使得規範的抽象性成為可能。抽象是人們處理復雜性的主要智力工具之一，而且通過忽視不感興趣的部分，從而有助於清晰性。各種形式符號系統對於精確、抽象地表達概念具有各自不同的能力，但它們均可用於嚴密地描述概念，更重要的是，它們比自然語言的描述更嚴密、更精確、更抽象。一般地，形式系統（框架）使得表示一個規範與其相應程序之間的映射成為可能。 形式規範有一個很有價值的特性：可操縱性。這就是說，可以在明確定義的規則的指導下，分析規範或或對形式規範進行變換。利用形式規範的可操縱性可以證明規範的一致性；可以推導出關於此規範的一些重要結果；還可以驗證規範的實現過程，至少可以驗證源代碼相對於其規範的正確性。更一般地說，有可能將不同級別規範間的驗證以及規範與程序間的驗證問題簡化為形式證明問題。這樣，形式化方法就可以提供程序對應其規範的非常高的可信度。所以，可操縱性也有助於確認，並且由這種特性可以得到進一步的抽象（推導出的性質），同樣，也有助於使得規範更清晰。

4. 第6章 敏捷流程 —— 6.5 敏捷的故事

　　這一小節提到了幾種比較出名的敏捷開發方法論，如FDD、Scrum、XP、TDD。前三者在書中都有專門的介紹，但TDD，久聞其大名，到底是何許妙招？

　　TDD（Test Driven Development），即測試驅動開發的基本思想就是在開發功能代碼之前，先編寫測試代碼，然後只編寫使測試通過的功能代碼，從而以測試來驅動整個開發過程的進行。這有助於編寫簡潔可用和高質量的代碼，有很高的靈活性和健壯性，能快速響應變化，並加速開發過程。 　　測試驅動開發的基本過程如下： 　　①　快速新增一個測試 　　②　運行所有的測試（有時候只需要運行一個或一部分），發現新增的測試不能通過 　　③　做一些小小的改動，盡快地讓測試程序可運行，為此可以在程序中使用一些不合情理的方法 　　④　運行所有的測試，並且全部通過 　　⑤　重構代碼，以消除重復設計，優化設計結構

　　簡單來說，就是不可運行/可運行/重構——這正是測試驅動開發的口號。

　　可想而知，測試驅動開發會極為有效地控制開發中的bug，但是這種先寫測試代碼的方式可能讓開發人員有很大的不適應。學習適應TDD的成本會不會比它帶來的收益更高呢？這就有待我們在實踐中摸索了。

《構建之法》讀後感3