一.規格化設計的發展歷史

在微軟的官網上，我找到了一篇描述規格的文章Specification and Verification of Object-Oriented Software,其中說到：

A system for specifying, writing, and verifying programs has many components. One component is the programming language itself and the specification constructs it contains. In some cases, specifications

are not part of the program, but are provided separately. Another component is the compiler, which generates executable code from the program. Yet another component is the program verifier, which itself can include a subcomponent that formalizes the semantics and proof obligations of the program, a subcomponent that generates logical formulas, called verification conditions, from the formalization, and a subcomponent, called the theorem prover, that analyzes the verification conditions and searches for proofs or counterexamples.

不得不承認的是，相比於代碼本身，規格的確有更強的規範性和更好的概括性，能夠在多人合作的工程中讓大家保持應有的默契。

以本學期的另一門課程操作系統為例，我們需要對已有的代碼進行補充，從而完成一個功能健全的微型操作系統，在每個函數的頭部，就有類似規格的說明，以處理缺頁中斷的pgfault函數為例，其說明為：

/* Overview:
 *      Custom page fault handler - if faulting page is copy-on-write,
 * map in our own private writable copy.
 *
 * Pre-Condition:
 *      `va` is the address which leads to a TLBS exception.
 

 *
 * Post-Condition:
 *  Launch a user_panic if `va` is not a copy-on-write page.
 * Otherwise, this handler should map a private writable copy of
 * the faulting page at correct address.
 */

有Overview,有前置條件，有後置條件，儼然一個不符合JSF語法規範的完整規格，也正是有了這些類規格的說明，才能使得同學們快速地明白函數的功能，需要滿足的需求以及需要考慮的情況，從而完成功能的實現。從數百人互相獨立地補充完成了功能一致的操作系統，就可以看出規格化設計的優勢。

正如K. Rustan M. LEINO所言，一個系統並不是代碼本身，它還應該包含規格、驗證等許多其它部分。規格設計自有其強大的生命力，不過，根據單詞是否拼錯、是不是缺個括號、等號寫成了雙等於還是單等於來評價規格的優劣，恕我不敢茍同。

二.bug分析

我的九次代碼作業公測均為全部通過，如下是我九次代碼作業在互測中被報的bug數目統計：

可以看到，我的前七次作業成績雖略有波動，但整體比較平穩。以第九次作業為過渡，我的bug數目獲得了突飛猛進的進步，屢創歷史新高度，這是為什麽呢？

首先需要聲明的是，我並沒有滿足前七次的成績而停滯不前，安於現狀。相反，在出租車系列作業中，我投入的時間更多，僅以規格的書寫為例，對代碼進行度量統計後發現，我一共使用了253個方法，規格書寫過程中，需要對每個方法的調用關系、前置後置條件進行分析，雖然其中有getter/setter此類比較容易進行規格設計的方法，但也不乏出租車運行、最短路計算等比較復雜的方法，同時我使用了IDEA中的Live Template,把更多的時間留給了設計而非書寫，僅以平均每個方法書寫規格大概需要5分鐘計，253個方法需要1265分鐘（即21小時）。而實際上，由於書寫過程中難免出現遺漏，還需要一遍又一遍地閱讀進行檢查。此時，我聽見鐘敲了一下，我只是剛剛完成了規格設計，還沒有看ISSUE上有沒有修改需求，然後開始代碼的設計、實現以及反復測試。

那bug數激增究竟是為什麽呢？

總結起來，其實我感覺經過前幾次的訓練，編程能力已經獲得了較大提升，對多線程的使用更加得心應手，不會感到難以駕馭，對整個程序架構的設計也初步有了自己的風格，此外，我還在編程進行了如下嘗試：

• 不再單純使用synchronized進行多線程互斥，為了提高並發性，嘗試使用了讀寫鎖、volatile等多種操作，盡可能減少了阻塞。
• 在流量的動態更新中，為了縮短線程啟動所需時間，引入了線程池newCachedThreadPool
• 在設計中嘗試使用了抽象類和抽象方法，使得代碼結構更加清晰
• 有意識地對每個類進行了封裝，final和private修飾符增多
• 在出租車信息輸出時借鑒了IFTTT中的SafeFile類，實現了文件寫入的線程安全

那bug數激增究竟是為什麽呢？

在經歷了憤懣、無奈、失望和深刻地自我反省等一系列激烈的情緒變化之後。我只能說，前幾次bug數目很少並不能說明我的代碼寫得多麽好，後幾次bug數目很多也不能說明我的代碼寫得多麽糟。

那bug數激增究竟是為什麽呢？

如果非要解釋的話，可以用觀察者偏見來說明。由於觀察者個人的動機和預期不同，可以導致觀察者對同一件事物的評論截然不同。觀察者偏見就像一個過濾器，一些事情被視為是相關和重要的而獲得註意，而另外一些則被視為無關和不重要的而被忽略。具體來說，在每次作業中，每個人都可以拿到兩份代碼，一份是自己的，一份是他人的。如果帶有觀察者偏見看自己的代碼，可能會對自己的代碼產生自信，許多本身很輕易應該檢查出來的錯誤可能就會被忽視。而如果帶有較深的觀察者偏見看別人的代碼，可能就會覺得這份代碼非常糟糕，應該被找出許多bug才對。這也是在申訴階段鬧出了許多矛盾甚至笑話的根源。

而另一個經典的社會心理學實驗斯坦福監獄實驗可能更能說明這一問題。當被賦予了不同角色之後，一個人的行為可能會在不覺間發生變化。情景力量對人的行為的影響程度可能是不可估量的。在互評過程中，每個人都有兩個角色，一個是被測試者，處於相對弱勢，如果想要申訴成功一個bug，可能需要花費相當多的時間和口舌；而另一個則是測試者，如果想要保持已有的“成果”，就得“堅守陣地”，不為所動。大家就是在這兩個角色中不斷切換，不斷改變自己的說話語氣和行為方式。當然每個個體受角色和規則的影響程度可能是不同的，因此就會呈現出不同的測試者和被測者組合，導致了有的同學最終bug少，而有的同學最終bug多（像我）。

下面曬一下我被報的系列bug供大家賞玩，其中不乏一些新奇有趣的(不要有分支和錯誤類型對不上的錯覺，它就是這麽被報的)：

功能性bug

規格bug

（有部分用簡短語句實在描述不清的並沒有在下列表格中體現）

三.分析自己規格bug產生的原因

心理學中，對於失敗的歸因可以分為內部歸因和外部歸因兩個維度，歸因風格的不同可以極大的影響個體的動機、心境和行為。鑒於許多同學在博客中已經進行了外部歸因，我在這裏暫且總結一下內因：

• 方法數目太多（當然這是一個原因，但並不是一個問題），導致書寫規格的工作量大，容易出錯
• 少部分方法存在先寫代碼，最後補規格的現象，因此可能漏掉前置條件或者後置條件
• 重構代碼時忘記修改規格
• 檢查不夠細致，例如仔細檢查兩遍程序，結果還是把兩個“==”錯寫成了“=”
• 對規格的具體要求沒有反復確認，被報了bug以後才知道對文件的寫操作必須寫在MODIFIES裏

四.前置條件和後置條件的不好寫法

1.前置條件

        /**
        * @REQUIRES: next!=null && next.length>6400;
        * @MODIFIES: next
        * @EFFECTS: next記錄root到des最短路徑上每個點的後繼結點
         *             \result==(root到des的最短路徑長度)
        */
        ===============================================================================
        /**
        * @REQUIRES: next!=null && next.length>6400 && 0<=root<6400;
        * @MODIFIES: next
        * @EFFECTS: next記錄root到des最短路徑上每個點的後繼結點
         *             \result==(root到des的最短路徑長度)
        */

/**
        * @REQUIRES:  0 <=id< 100 && credit>=0 && pos_x>=0 && pos_x<80 && pos_y>=0 &&pos_y<80;
        * @MODIFIES: this.id;
         *            this.credit;
         *            this.pos_x;
         *            this.pos_y;
         *            this.sendInfo;
         *            this.state;
        * @EFFECTS: this.id == id;
         *         this.credit == credit;
         *         this.pos_x == pos_x;
         *         this.pos_y == pos_y;
         *         this.sendInfo == new SendInfo(id,new Coordinate(pos_x,pos_y),new Req(),new Vector<ReceiveInfo>(),true);
         *         this.state 為state對應的狀態
        */
        =====================================================================================
        /**
        * @REQUIRES:  0 <=id< 100 && credit>=0 && pos_x>=0 && pos_x<80 && pos_y>=0 &&pos_y<80;
        * @MODIFIES: this.id;
         *            this.credit;
         *            this.pos_x;
         *            this.pos_y;
         *            this.sendInfo;
         *            this.state;
        * @EFFECTS: this.id == id;
         *         this.credit == credit;
         *         this.pos_x == pos_x;
         *         this.pos_y == pos_y;
         *         this.sendInfo == new SendInfo(id,new Coordinate(pos_x,pos_y),new Req(),new Vector<ReceiveInfo>(),true);
         *         (state==0)==>this.state = STATE.SERVICE;
         *          (state==1):this.state == STATE.RECEIVE;
         *          (state==2):this.state == STATE.WAIT;
         *          (state==3):this.state == STATE.STOP;
        */

public static void stay(long time) 
        /**
         * @REQUIRES: None
         * @MODIFIES: None
         * @EFFECTS:  None
         */
  =========================================================================================
   /**
         * @REQUIRES:time>0;
         * @MODIFIES: None
         * @EFFECTS:  None
         */

2.後置條件

        /**
         * @REQUIRES: lightmap!=null && lightmap.length>=WIDTH*WIDTH;
         * @MODIFIES: System.out;
         * @EFFECTS: normal_behavior
         *             (\exist int i,j;0<=i<WIDTH && 0<=j<WIDTH;(i,j) isn‘t crossroads) ==>
         *                 (輸出提示信息 && lightmap[i][j]= 0;)
         *             (\exist int i,j;0<=i<WIDTH && 0<=j<WIDTH;lightmap[i][j]!=0 && lightmap[i][j]!=1)==>
         *                 exceptional_behavior(MyException);
         */ 
         ==============================================================================
         /**
         * @REQUIRES: lightmap!=null && lightmap.length>=WIDTH*WIDTH;
         * @MODIFIES: System.out;
         * @EFFECTS: normal_behavior
         *             (\exist int i,j;0<=i<WIDTH && 0<=j<WIDTH;(i,j) isn‘t crossroads) ==>
         *                 (輸出提示信息 && lightmap[i][j]= = 0;)
         *             (\exist int i,j;0<=i<WIDTH && 0<=j<WIDTH;lightmap[i][j]!=0 && lightmap[i][j]!=1)==>
         *                 exceptional_behavior(MyException);
         */

private void doReceive(){
        /**
        * @REQUIRES: pos!=null;task!=null;next!=null;next.length>6400;
        * @MODIFIES: cal_path;curr_time;task;next;state;
        * @EFFECTS:  (\old(cal_path)==false && curr_time-task.getSend_time()>Time.go_cost)==>
         *              (curr_time == task.getSend_time()+(Time.go_cost-Time.granularity)+(Math.abs(random.nextInt())%Time.granularity));
         *
         *             (\old(cal_path)==false)==>
         *             (task.start_time==curr_time && next更新為起點到終點的最短路 && cal_path==true);
         *
         *             (\old(cal_path)==true && pos.equals(task.getPassenger_posi()))==>
         *             (task.getin_time==curr_time && task.getPass_receive().contains(passby) &&
         *             curr_time==\old(curr_time)+Time.stop_cost && state==STATE.SERVICE && cal_path==false);
         *
         *             (\old(cal_path)==true && !pos.equals(task.getPassenger_posi()))==>
         *             (task.getPass_receive().contains(passby));
        */
  ===========================================================================================
     /**
        * @REQUIRES: pos!=null;task!=null;next!=null;next.length>6400;
        * @MODIFIES: cal_path;curr_time;task;next;state;
        * @EFFECTS:  (\old(cal_path)==false && curr_time-task.getSend_time()>Time.go_cost)==>
         *              (curr_time == task.getSend_time()+(Time.go_cost-Time.granularity)+(Math.abs(random.nextInt())%Time.granularity));
         *
         *             (\old(cal_path)==false)==>
         *             (task.start_time==curr_time && next==(The shortest path from the beginning to the end) && cal_path==true);
         *
         *             (\old(cal_path)==true && pos.equals(task.getPassenger_posi()))==>
         *             (task.getin_time==curr_time && task.getPass_receive().contains(passby) &&
         *             curr_time==\old(curr_time)+Time.stop_cost && state==STATE.SERVICE && cal_path==false);
         *
         *             (\old(cal_path)==true && !pos.equals(task.getPassenger_posi()))==>
         *             (task.getPass_receive().contains(passby));
        */

五.按照作業分析被報的功能bug與規格bug在方法上的聚集關系

事實上，功能bug和規格bug在方法上著實沒有呈現出什麽聚集關系，就第十一次功能和規格bug數目1：14來看，他們的相關系數應該在0附近波動。

如下是三次作業中兩種bug的占比：

六.總結體會

在第十一次作業中，我所拿到Readme有13頁之長，在最後一頁留了一首小詩。雖然我拿到質量好的代碼一般是抱著學習的態度閱讀的，並不在意是否能找出bug，但這首詩還是給了我一些觸動。

在這次博客的結尾我也想把它送給諸位：

煮豆燃豆萁，

豆在釜中泣。

本是同根生，

相煎何太急？

面向對象階段總結 | 叁