OO第三次博客做業

規格化設計發展歷史

在調研的過程當中再一次驗證了「百度搜索不適合學術」這個觀點，沒有找到合適的搜索結果後，轉用Google，才找到了一些細節。

保證程序的正確性以及減小軟件錯誤一直是程序員關注的問題，Hoare提出了基於「前置後置條件」的接口規格方法。

爲了創建正確的類規格，近些年來，研究者們進行了抽象變量、接口規格、狀態抽象、查詢方法等不一樣方面的嘗試，並取得了很大的進展。

爲保證程序的正確性， Hoare[l] 提出了關於接口的規格方法，即若一種方法在執行前知足前置條件，運行後知足後置條件，那麼這種方法就是正確的。 Hoare 提出的這個結論爲規格化發展起到了奠定的做用，也爲類中接口的規格化提供了理論基礎。

針對各方法的精確規格定義， MeyeP] 提出契約式編程延續了對方法的精肯定義，但其不足是依賴內部狀態來體現方法之間的相互依賴。

課程中使用的JSF更偏向於「契約式設計」(Design by Contract)：爲傳統的抽象數據結構增長了先驗條件、後驗條件和不變式。

規格bug分析

bug類型	bug內容	出現位置
JSF檢查->Requires不完整	忘寫JSF	Windows類
方法規格檢查->Effects不完整	JSF不完整	Taxi類
方法規格檢查->JSF不符合規範	可追蹤出租車沒有寫繼承	Taxi2類

bug產生緣由：

• 第九次做業是JSF被扣分最嚴重的一次。我是寫完代碼而後再去寫JSF，在金工實習上補全JSF就上交了，最後發現由於有一個類的JSF寫漏了，對面對每個沒寫的方法規格報了15個JSF imcomplete...
• 不是過重視JSF，致使部分後置條件不夠詳細，最後兩次做業總共被報了3個JSF。

前置條件後置條件寫法改進

前置條件

(1)修改前

/** @REQUIRES : map!=null,taxiGUI!=null,GuiInfo!=null;
     * @MODIFIES : this.id,this.credit,this.map,this.taxiGUI,this.GuiInfo,this.flowMonitor,this.VIP;
     * @EFFECTS : None;
     */

對新增變量flowMonitor判斷
修改後

/** @REQUIRES : map!=null,taxiGUI!=null,GuiInfo!=null,flowMonitor!=null;
     * @MODIFIES : this.id,this.credit,this.map,this.taxiGUI,this.GuiInfo,this.flowMonitor,this.VIP;
     * @EFFECTS : None;
     */

(2)修改前

/** @REQUIRES : id > 0;
     * @MODIFIES : None;
     * @EFFECTS : \result == id;
     */

不須要對id進行判斷
修改後

/** @REQUIRES : None;
     * @MODIFIES : None;
     * @EFFECTS : \result == id;
     */

(3)修改前

/** @REQUIRES: None;
     * @MODIFIES: None;
     * @EFFECTS: \result == System.currentTimeMills();
     */

對於Thread進行追加Require
修改後

/** @REQUIRES: None;
     * @MODIFIES: None;
     * @EFFECTS: \result == System.currentTimeMills();
     * @THREAD_REQUIRES:\locked(\this);
     * @THREAD_EFFECTS:\locked(\this);
     */

(4)修改前

/** @REQUIRES: None;
     * @MODIFIES: None;
     * @EFFECTS: (distance==1) ==> \result = true
    (distance!=1) ==> \result = false
     */

對於座標範圍的判斷
修改後

/** @REQUIRES: src>0 && src <80 && dst >0 && dst < 80;
     * @MODIFIES: None;
     * @EFFECTS: (distance==1) ==> \result = true
    (distance!=1) ==> \result = false
     */

(5)修改前

/** @REQUIRES : s!=null;
     * @MODIFIES : this.str;
     * @EFFECTS : str == s;
     */
    public Request(String s) {

基本數據類型不須要進行判斷（編譯器保證）
修改後

/** @REQUIRES : None;
     * @MODIFIES : this.str;
     * @EFFECTS : str == s;
     */
    public Request(String s) {

後置條件

(1)修改前

/** @REQUIRES: requestQueue!=null;taxiGUI!=null;
     * @MODIFIES: this.requestQueue,this.taxiGUI;
     * @EFFECTS: None;
     */

修改後

/** @REQUIRES: requestQueue!=null;taxiGUI!=null;
     * @MODIFIES: this.requestQueue,this.taxiGUI;
     * @EFFECTS: this.requestQueue == requestQueue, this.taxiGUI == taxiGUI;
     */

(2)修改前

/** @REQUIRES : None;
     * @MODIFIES : None;
     * @EFFECTS : \result == invariant(this);
     */

repOK 的具體判斷
修改後

/** @REQUIRES : None;
     * @MODIFIES : None;
     * @EFFECTS : \result = (requestQueue != null);
     */

(3)修改前

/**@REQUIRES : readFile!=null;taxiGUI!=null;flowMonitor!=null;GuiInfo!=null;
     * @MODIFIES : requestQueue,readFile,taxiGUI,flowMonitor,GuiInfo;
     * @EFFECTS : this.requestQueue == requestQueue;
     *      this.readFile == readFile;
     *      this.taxiGUI == taxiGUI;
     *      this.flowMonitor == flowMonitor;
     */

對新增的GuiInfo沒有修改Effects
修改後

/**@REQUIRES : readFile!=null;taxiGUI!=null;flowMonitor!=null;GuiInfo!=null;
     * @MODIFIES : requestQueue,readFile,taxiGUI,flowMonitor,GuiInfo;
     * @EFFECTS : this.requestQueue == requestQueue;
     *      this.readFile == readFile;
     *      this.taxiGUI == taxiGUI;
     *      this.flowMonitor == flowMonitor;
     *      this.GuiInfo == GuiInfo;
     */

(4)修改前

/** @REQUIRES : str!=null；
     * @MODIFIES : this.reqSame,this.timeSame；
     * @EFFECTS : \request.equals(同質請求添加到同質判斷隊列)；
     */

儘可能轉換天然語言爲邏輯語句
修改後

/** @REQUIRES : str!=null；
     * @MODIFIES : this.reqSame,this.timeSame；
     * @EFFECTS : reqSame.add(str),timeSame.add(time)
     */

(5)修改前

/** @REQUIRES : taxis!=null;
     * @MODIFIES : None;
     * @EFFECTS :None;
     */

get方法必定要寫\result !
修改後

/** @REQUIRES : taxis!=null;
     * @MODIFIES : None;
     * @EFFECTS : \result == taxis;
     */

功能bug和規格bug的彙集關係

此次博客做業這樣要求，按照可能的論證：因爲不清楚代碼的功能細節，因此致使出現了規格bug，這種規格bug伴隨着方法的功能bug出現，因此會出現聚類關係。
因爲JSF是在代碼收工以後寫的，因此基本沒有聚類關係。
三次做業最嚴重的規格bug就是忘寫部分JSF，其餘出現規格bug的地方並無出現功能問題。
若是說有什麼沒有被報的功能bug,那麼對應的規格bug必定是有的，只是沒有被抓出來而已。

設計與撰寫規格的思路

• Require部分：通常都是對於輸入的形參作非空判斷
• Modify部分：對於方法寫到的private變量挨個判斷是否修改
• Effects部分：對於Modify的變量變化的狀況進行分析

最後使用JSFTool.class進行復查

心得體會

最近幾回OO做業感受收穫比較小，在作課程做業時對於Java的語法沒有更深學習的動力，也沒有Java與其餘技術的結合應用，若是隻是完成做業只須要JavaSE的部分語法基礎而已。這兩週花費大量時間在JSF的書寫上，並且遇到對面的刁鑽扣分也容易受到打擊，可能你們都以爲相對於程序的功能Bug，要扣規格的分不要容易太多吧。

參考文獻 [1]王偉,丁二玉,駱斌.基於抽象狀態的類的行爲規格化方法[J].計算機科學,2016,43(S1):457-460.