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第三次單元總結