一、規格化設計發展歷史及被重視的原因

　　這個問題還真的不容易，我翻了很多網頁！甚至還從百度知道裏發現了往屆學長的足跡，不過那個問題貌似到現在還沒有有效的回答。由於相關的資料不多，所以我只能根據已有的資料來闡述一下規格化設計的歷史和重要性吧。劇情不夠，臆造來湊，hhh !任何事物都有一個發展的過程，不是在編程語言才誕生時，人們就重視規格化設計了。在此之前，應該有很多人都感受到了代碼設計不規範而帶來的壞處，突然有一天，一個人發現，哎？我這樣規格化設計不就解決了問題了嗎？然後啊，開始有了一種新的事物——規格化設計。所以我們OO課程也多了一個扣分項，JSF規範檢查。

　　說到規格化設計的意義，還真的不一般。首先，用戶不必為了使用過程而費神去看過程的主體，我們只需要關註如何用就行了。其次，方便代碼的維護，這給我們的感受是非常真實貼切的，尤其在改需求時，如果你的代碼設計沒有做到規格化，那麽經常牽一發而動全身，改了一處便會帶來很多其他BUG。還有就是方便團隊開發，如果團隊裏各自寫各自的代碼，不註意協調，那麽帶來的後果的不堪設想的，規格化設計就能避免這樣的問題，從而提高團隊開發的效率。

二、規格BUG分析

　　這三次作業我總共被扣了兩個JSF，加上一個未被發現的，共三個，如下表：

　　第一個BUG是第一次接觸JSF，根本搞不懂咋寫，於是去GitHub上參考了一下學長的寫 法，然而，學長的Effects在構造方法時都是類似於this.a=a; 於是我深以為然，於是就模仿著寫，結果等到互測結束後，才知道要用 == 。另外兩個BUG是因為modifies漏掉了一些內容，因為本來已經寫好了JSF了，但是又因為debug改了一些內容，沒有更新規格，就爆炸了。這三次JSF給我的感覺就是枯燥，在我看來，OO最大的樂趣就是享受如何設計自己的項目，將原來虛無縹緲的需求變成具體的可實現的東西。然而我們在第七次作業已經完成了絕大多數的內容，再到第九次作業時去寫JSF,完全是為了應付作業而寫的規格，舉個非常不恰當的例子，就像把自己吃過的甘蔗再重新嚼一遍，嚼不好的話還要被扣分！二十多個類，幾百個方法，未免給人不佳的體驗。強烈建議下一屆應該改變一下作業順序，先寫JSF，再開始出租車，否則JSF就根本達不到預期的訓練效果。

三、五種優化寫法

　　不得不承認，我JSF寫的的確不好，後置條件為了方便，幾乎都是用自然語言寫的，因此還有很大的改進空間，以下舉幾個栗子

　　1.這是我新建一個TaxiArray的構造方法

TaxiArray(TaxiGUI taxiGUI) {
    /**
     * @REQUIRES: taxiGUI!=null
     * @MODIFIES: \this.taxis;
     * @EFFECTS:
     *          新建100輛出租車
     */
    for (int i=0;i<30;i++){
        taxis[i]=new VIPTaxi();
        taxis[i].id=i;
        taxiGUI.SetTaxiType(i,1);
    }
    for (int i = 30; i < 100; i++) {
        taxis[i] = new Taxi();
        taxis[i].id = i;
        taxiGUI.SetTaxiType(i,0);
    }
}

　　這個規範明顯就不規範，我感覺更新為下面的會更好，

        /**
         * @REQUIRES: taxiGUI!=null
         * @MODIFIES: \this.taxis;
         * @EFFECTS:
         *          (\all int i; 0<=i<30; taxis[i] == new VIPTaxi();
         *          (\all int i; 0<=i<30; taxis[i] == new Taxi();
         *          update taxiGUI
         */

　　2.這是我設置出租車狀態的代碼

 public synchronized void setToGetStop(int num) {
        /**
         * @REQUIRES: 0=<num<=99
         * @MODIFIES: \this.taxis;
         * @EFFECTS:
         *          設定指定的出租車狀態為接單後停止
         * @THREAD_REQUIRES:
         * \locked(this);
         * @THREAD_EFFECTS:
         * \locked();
         */
        taxis[num].state = "toGetStop";
        taxis[num].taketime = 0;
        taxis[num].nowx = taxis[num].toX;
        taxis[num].nowy = taxis[num].toY;
    }

　　改進後：

        /**
         * @REQUIRES: 0=<num<=99
         * @MODIFIES: \this.taxis;
         * @EFFECTS:
         *         \taxis[num].state == "toGetStop"; 
         *         \taxis[num].taketime == 0;
         *         \taxis[num].nowx == taxis[num].toX;
         *         \taxis[num].nowy == taxis[num].toY;
         * @THREAD_REQUIRES:
         * \locked(this);
         * @THREAD_EFFECTS:
         * \locked();
         */

　　3.我的重寫toString方法

 public String toString() {
        /**
         * @REQUIRES: None;
         * @MODIFIES: None;
         * @EFFECTS: 重寫toString
         */
        return "from (" + from[0] + "," + from[1] + ") to (" + to[0] + "," + to[1] + ") time " + time;
    }

　　改為：

         /**
         * @REQUIRES: None;
         * @MODIFIES: None;
         * @EFFECTS: \result == "from (" + from[0] + "," + from[1] + ") to (" + to[0] + "," + to[1] + ") time " + time;
         */

　　4.我的將請求加入到請求隊列中的方法

 private synchronized void addRequest(Request request) {
        /**
         @REQUIRES: request!=null
         @MODIFIES: \this.requests;
         @EFFECTS: 向requests中加入請求
         @THREAD_REQUIRES:
         \locked(this);
         @THREAD_EFFECTS:
         \locked();
         */
        requests.add(request);
    }

　　改為：

         /**
         @REQUIRES: request!=null
         @MODIFIES: \this.requests;
         @EFFECTS:  (\requests.size == \old(\requests).size+1) && (\requests.contains(a)==true);
         @THREAD_REQUIRES:
         \locked(this);
         @THREAD_EFFECTS:
         \locked();
         */

　　5.這是判斷紅綠燈地圖中的一行是否符合Map規範的方法

 public boolean checkMap(String s) {
        /**
         @REQUIRES: s!=null;
         @MODIFIES: None;
         @EFFECTS: 判斷s是否符合地圖中每一行的規範
         */
        s = s.replaceAll("\\s*", ""); //去除字符串中所有空字符
        if (s.length() != 80) //判斷一行是否有80個字符
            return false;
        for (int i = 0; i < 80; i++) {
            if (s.charAt(i) != ‘0‘ && s.charAt(i) != ‘1‘) { //判斷是否由0,1組成
                return false;
            }
        }
        return true;
    }

　　改為：

         /**
         @REQUIRES: s!=null;
         @MODIFIES: None;
         @EFFECTS: \result==(s.replaceAll("\\s*", "").length ==80) &&(all int i;0<=i<=80; s.charAt(i) == ‘0‘ || s.charAt(i) == ‘1‘))
         */

四、功能BUG和規格BUG的聚集關系

　　由上面的表格來看，我的功能BUG和規格BUG之間的關系不太緊密，可能是因為代碼都是在規格之前寫的因素吧，這三次作業，平均每次只要加100-200行代碼就行，因此，第七次作業的

代碼已經免去了重新設計的步驟，所以規格只能在代碼後寫！

五、心得體會

　　這三次作業和電梯比起來好多了，電梯是我永遠的噩夢！通過這三次作業的洗禮，也就意味著OO代碼作業結束啦！hhh，OO真的難，從開學到現在，我感覺我老了一年（QWQ），天天刷夜刷的。不過收獲也是很多的，從寫不到200行JAVA代碼的小白到現在2000行的出租車，能力在不知不覺間就提升了，所有努力都是有回報的，突然想起一首老歌（也是童年的回憶）：

每一次
都在徘徊孤單中堅強
每一次
就算很受傷也不閃淚光
我知道
我一直有雙隱形的翅膀
帶我飛 飛過絕望
不去想
他們擁有美麗的太陽
我看見
每天的夕陽也會有變化
我知道
我一直有雙隱形的翅膀
帶我飛 給我希望
我終於看到所有夢想都開花
追逐的年輕
歌聲多嘹亮
我終於翺翔
用心凝望不害怕
哪裏會有風就飛多遠吧
不去想
他們擁有美麗的太陽
我看見
每天的夕陽也會有變化
我知道
我一直有雙隱形的翅膀
帶我飛 給我希望
我終於看到所有夢想都開花
追逐的年輕
歌聲多嘹亮
我終於翺翔
用心凝望不害怕
哪裏會有風就飛多遠吧
隱形的翅膀讓夢恒久比天長
留一個願望讓自己想象

OO第三次博客作業