隨著第四次出租車作業的結束，整個OO課程最艱難的工程部分就宣告結束了，頭發總算是保住了。首先感謝各位測我的dalao沒有對本菜雞兒的代碼大開殺戒（諸如報20個JSF錯之類的），這還是讓我挺高興的，某些OO中經常出現的很糟心的事情沒有發生在我的身上（同時也為遇到了這些事情的同學默哀）。這四次OO作業的一個很大的側重點就是對規格的訓練，諸如對JSF，Overview，repOK等等的書寫與實現。在大家經歷了多線程電梯和IFTTT的折磨之後，對多線程的應用和處理已經日益精進，然而當大家在寫出租車代碼暗自得意的時候，JSF這個東西無疑是給了大家當頭一棒。所以，本次博客在日常分析bug的基礎之上，還增加了很多和規格有關的東西。

　　關於規格化設計的大致發展歷史和為什麽得到了人們的重視的問題，各大搜索網站基本沒有給出明確的答案（我在必應搜這個的時候甚至搜到了前兩天同學的博客hhh可見這東西網上很少）。將網上七零八落的資料結合起來還是能勉強得出一些結論的。國際標準化組織ISO曾經給出過軟件的需求規格說明書，即SRS，但需求調查，分析工作告一段落的時候，人們需要對這些需求進行規格化描述，整理成文，這是在軟件工程中相當有價值的一個文件。可能這就是規格化早期的情況，那時候的規格化主要面向於工程化開發的，具體的規格也相對較大，比如說針對某些特定的用戶群體，使用特定的實現方式等。但是隨著計算機科學的不斷發展，規格變得越來越小，從最開始的面向大工程的規格描述，逐漸變成了我們今天所寫的某一個函數的規格。規格化之所以受到人們的重視，在於其能夠很好地描述程序員在進行項目開發是需要幹什麽，怎麽幹的問題。一個良好的規格，能讓程序員在程序開發中保持一個清晰的思維，降低錯誤發生的幾率，同時也能在交互的時候讓用戶明確地知道輸入和輸出的關系，什麽輸入能夠讓程序正常運行，得出正常的結果，而什麽輸入是非法的，不應該出現的。總之，規格的存在使得程序的開發效率，與用戶的交互效果得到了很大的提升。

　　關於第三單元的三次作業的規格bug，所列出的表格如下：

三單元第一次作業

三單元第二次作業

三單元第三次作業

　　在第一次作業中，我的規格BUG的主要產生問題體現在對JSF語法的認識不清晰，不透徹，於是在某些固定格式上犯錯。JSF不同於自然語言，自然語言有很多種描述方法，因此有很大的歧義性，而JSF的描述比較明確，所以說規範JSF格式是非常重要的。除此之外還有線程方法忘記寫其獨有的JSF了，這也是對JSF格式不熟悉而造成的。在第二次作業中，一些JSF的邊界性問題仍然出現，比如某些特殊函數（如Main，構造函數等需不需要寫JSF等）；而且repOK方法的構造出現失誤，不能保證在初始化時repOK恒為真，這是對不變式在各種情況下的應用的不熟練。第三次作業中，仍然是邊界性的錯誤。。。想當然地認為repOK方法不用實現JSF造成失分。

　　下面列舉幾個前置條件和後置條件的不好寫法及其改進措施：

　　1.@REQUIRES:balabala... 改進@REQUIRES: balabala...(冒號後面有空格)

　　2.@REQUIRES: 變量a有效 改進：將變量a有效用JSF語言描述，自然語言講不清楚。。。

　　3.@REQUIRES: 變量a非空 改進：a != null 盡量不用自然語言表述

　　4.@REQUIRES: a = 100 || a = 1 改進：a == 100 || a == 1

　　5.@REQUIRES: a > 0 && a < 100 改進：0 < a < 100

　　6.@EFFECTS: 函數返回值為0 改進：\result == 0（盡量避免用自然語言描述）

　　7.@EFFECTS: size = size + 1 改進：size = (\old)size + 1

　　8.@EFFECTS: a = 0 改進：a == 0（後置條件必為布爾表達式）

　　9.@EFFECTS: if(a == 0) then \result == 1 改進(a == 0) ==> (\reuslt == 1) （後置條件中不應描述算法）

　　10.@EFFECTS: vector.containsABCTogether() 改進vector.contains(A) && vector.contains(B) && vector.contains(C)（盡量用簡單的單詞來描述）

　　接下來給出被報的功能bug與規格bug在方法上的聚集關系，列表如下所示（第三單元第一次作業沒有被查出功能性bug）

第二次作業

第三次作業

　　最後對規格的撰寫做一個總結，我在設計規格時的思路和設計方法時的思路一致，即先定方法的輸入和想要方法達成的目的（有時是返回值，有時是修改變量），然後再定要修改的全局變量，然後開始規格的撰寫，使用JSF的一些格式來完成規格，不到迫不得已（比如說當函數比較長導致EFFECTS不好描述的時候）不用自然語言來描述。然後開始進行函數的撰寫，最後再對照JSF的三項來檢查函數的實現是否與JSF的一致。其實當定好了規格之後你就可以直接開始寫函數了，所以我個人覺得最先開始定規格是特別重要的，在定規格的時候順便你也能理清方法的實現思路等等，定好了規格之後你就可以開始隨意開火了，先下鍵盤寫規格或者直接寫方法都可以。最後不要忘了對照著JSF檢查一下函數的實現是否與JSF有出入，然後根據出入分析決定是修改JSF還是修改函數本身。

　　總之，第三次博客作業到這裏就結束了，這標誌著OO之路基本可以說告一段落了。當然，還不能開浪，畢竟以後還有JSF的公測（我可不想被扣上20個JSF的錯。。。）。

第十二次OO作業