OO第三次單元總結
一、規格化設計發展歷史
軟件規格化方法，最早可追溯到20世紀50年代後期對於程序設計語言編譯技術的研究，當時出現了各種語法分析程序自動生成器以及語法制導的編譯方法，使編譯系統的開發從“手工藝制作方式”發展成具有牢固理論基礎的系統方法。規格化設計的研究高潮始於20世紀60年代後期，針對當時所謂的“軟件危機”，人們提出種種解決方法，如采用工程方法來組織、管理開發過程和通過鉆研規律建立嚴密的理論以指導開發實踐。
經過30多年的研究和應用，如今人們在規格化設計取得了大量、重要的成果，從早期最簡單的一階謂詞演算到現在應用於不同領域、不同階段的基於邏輯、狀態機、網絡、進程、代數等眾多規格形式化方法，它的發展趨勢是逐漸融入設計開發的各個階段，從需求分析、功能描述、算法設計、編程、測試直到維護。
規格化設計對代碼的創作者和使用者都有重要的作用。對於編程者，規範的設計有助於架構的建立和調整，有助於完善修正細節，有助於未來的維護和擴展；對於使用者，規格化的呈現有助於理解剖析，避免不必要的誤解和分歧，同時也利於高效的閱讀和學習。
二、bug分析
三次作業總共被報了四個規格bug，很遺憾的是其中有三個都是“忘記寫了”……emm反思一下第十次可能和趕時間有關，但是第十一次在時間蠻充裕的情況下就真的是粗心沒檢查的鍋。另外一個關於repOK的bug，我覺得測試者說的很有道理。因為在原來的repOK方法中，只要出現了對象型的變量我一律用“！=null”來處理，但是想想每個對象的類中也有它自己的repOK，理應傳承下來，只有滿足了所有的repOK才能說明科學合理性。
雖然從表格上看，功能bug與規格bug確實沒有重合的地方，但是這並不意味著兩者就毫無關聯。兩次作業中功能出現的問題集中在input、run、randomdrive這些代碼規模較大，邏輯較復雜的方法中，本身規格就很難概括，只能借助自然語言的幫助，加上關鍵步驟的布爾表達式來描述。由於規格無法涵蓋細小邏輯，很難體現出錯誤疏漏，或者換一種說法，書寫規格沒有起到應有的作用，所以從報告bug的角度，就看不出聯系了。
三、規格改進示例
- 前置條件
/** * @REQUIRES: * 0<=index<=6399; * @MODIFIES:None; * @EFFECTS: * normal_behavior: * !(\exist int next;map.reachlist[index].contains(next)) ==> \result==index; * 在index的可達節點中隨機選取一個兩點之間邊流量最小的節點next. * \result==next; * exception_behavior(Exception e): * \result==index;*/
↓
/** * @REQUIRES: * 0<=index<=6399; * 0<=oldindex<=6399; * @MODIFIES:None; * @EFFECTS: * normal_behavior: * !(\exist int next;map.reachlist[index].contains(next)) ==> \result==index; * 在index的可達節點中隨機選取一個兩點之間邊流量最小的節點next. * \result==next; * exception_behavior(Exception e): * \result==index; */
······································································································································
/** * @REQUIRES: * 0<=start<=6399; * 0<=end<=6399; * 0<=flow<=100; * @MODIFIES: * \this.flow; * @EFFECTS: * \this.flow[start][end]==flow; * \this.flow[end][start]==flow; */
↓
/** * @REQUIRES: * 0<=start<=6399; * 0<=end<=6399; * distance from start to end is 1. * 0<=flow<=100; * @MODIFIES: * \this.flow; * @EFFECTS: * \this.flow[start][end]==flow; * \this.flow[end][start]==flow; */
······································································································································
/** * @REQUIRES: * 0<=index<=6399; * 0<=next<\this.reachlist[index].size(); * @MODIFIES:None; * @EFFECTS: * type==0 ==> \result==\this.reachlist[index].get(next); * type==1 ==> \result==\this.initreachlist[index].get(next); */
↓
/** * @REQUIRES: * 0<=index<=6399; * 0<=next<\this.reachlist[index].size(); * type==0 || type==1; * @MODIFIES:None; * @EFFECTS: * type==0 ==> \result==\this.reachlist[index].get(next); * type==1 ==> \result==\this.initreachlist[index].get(next); */
······································································································································
/** * @REQUIRES:None; * @MODIFIES:None; * @EFFECTS: * (r‘s time,start_x,start_y,end_x,end_y are equal to this‘s) ==> \result==true; * !(r‘s time,start_x,start_y,end_x,end_y are equal to this‘s) ==> \result==false; */
↓
/** * @REQUIRES: * r!=null; * @MODIFIES:None; * @EFFECTS: * (r‘s time,start_x,start_y,end_x,end_y are equal to this‘s) ==> \result==true; * !(r‘s time,start_x,start_y,end_x,end_y are equal to this‘s) ==> \result==false; */
······································································································································
/** * @REQUIRES:None; * @MODIFIES:None; * @EFFECTS: * \result==\this.inputs.get(i).start_x; */
↓
/** * @REQUIRES: * 0<=i<\this.inputs.size(); * @MODIFIES:None; * @EFFECTS: * \result==\this.inputs.get(i).start_x; */
······································································································································
- 後置條件
/** * @REQUIRES:None; * @MODIFIES: * \this.credit; * @EFFECTS: * \this.credit==\this.credit+1; */
↓
/** * @REQUIRES:None; * @MODIFIES: * \this.credit; * @EFFECTS: * \this.credit==\old(\this.credit)+1; */
······································································································································
/** * @REQUIRES: * req!=null; * @MODIFIES:None; * @EFFECTS: * \result == request in inputs that equals req ; */
↓
/** * @REQUIRES: * req!=null; * @MODIFIES:None; * @EFFECTS: * \result == (\exist Request r; inputs.contains(r);r.equals(req)); * @THREAD_REQUIRES: * \locked(\this); * @THREAD_EFFECTS: * \locked(); */
······································································································································
/** * @REQUIRES: * req!=null; * @MODIFIES: * \this.inputs; * @EFFECTS: * \this.inputs.contains(req) ; * @THREAD_REQUIRES: * \locked(\this); * @THREAD_EFFECTS: * \locked(); */
↓
/** * @REQUIRES: * req!=null; * @MODIFIES: * \this.inputs; * @EFFECTS: * \this.inputs.contains(req) && \this.inputs.size()=\old(\this.inputs).size()+1; * @THREAD_REQUIRES: * \locked(\this); * @THREAD_EFFECTS: * \locked(); */
······································································································································
/** * @REQUIRES:None; * @MODIFIES: * \this.reachlist; * \this.initreachlist; * @EFFECTS: * \this.reachlist == new Vector<Integer>(); * (\all Vector x;reachlist.contains(x);x!=null); * \this.initreachlist == new Vector<Integer>(); * (\all Vector x;initreachlist.contains(x);x!=null); */
↓
/** * @REQUIRES:None; * @MODIFIES: * \this.reachlist; * \this.initreachlist; * @EFFECTS: * \this.reachlist!=null; * (\all Vector x;reachlist.contains(x);x!=null); * \this.initreachlist!=null; * (\all Vector x;initreachlist.contains(x);x!=null); */
······································································································································
/** * @REQUIRES:None; * @MODIFIES:None; * @EFFECTS: * \result==queue!=null && inputs!=null && taxigui!=null && outFile!=null && taxis!=null && taxiInfo!=null && map!=null; */
↓
/** * @REQUIRES:None; * @MODIFIES:None; * @EFFECTS: * \result==queue!=null && inputs!=null && taxigui!=null && outFile!=null && taxis!=null && taxiInfo!=null && map!=null && queue.repOK() && inputs.repOK() && (\all Taxi t;taxis.contains(t);t.repOK()) && map.repOK(); */
······································································································································
四、思路與體會
由於出租車的框架是在第七次作業時搭建好的，後面基本沒有做出大的變動，所以大部分的規格是看著方法補充。前置條件就從傳入的參數入手，基本類型需要判斷在指定範圍內，對象類型則要求不為空。中間條件抓住本類的類變量，逐一檢查是否在此方法中被改變。後置條件比較復雜，需要兼顧條件判斷、數組遍歷、返回值、類變量前後改變等，如果是邏輯太多的方法就只能挑出關鍵步驟，借助自然語言描述。
不同的遭遇，不同的體會。在三次作業的互測過程中，測試者並沒有死摳我的規格細節，扣的分主要是因為自己的粗心大意，所以在承受範圍之內。至於書寫規格的體會，由於沒有做到像老師在課堂上說的 “先寫規格後寫代碼”，整個過程可以說是“重溫方法思路，再按規定格式翻譯一遍”。雖然體驗效果有些欠佳，但依然不能否認規格化設計的重要性。在真正的工程化編程中，規格的確有提高效率，減少出錯的作用。同時我也認為，“規格化”不僅僅是貫徹體現在方法前的幾行JSF註釋中，更重要的是從構想到實施的過程，真正具有 “規格化”的思想。
OO第三次單元總結