１、規格化設計的歷史（附參考鏈接～）

1950，第一次分離，主程序和子程序的分離
　　產生基本的軟件開發過程：分析—設計—編碼—測試，使大型軟件系統的開發成為可能

1975—1980，第二次分離，規格說明（Spec）和體（body）的分離

　　說明是類型定義和操作描述，體是操作的具體實現。
　　（具體的例子就是C++,Java等面向對象語言的類說明與類實現的分離。）
　　解決方案設計只關註說明，實現時引用或者設計體。
　　體的更改、置換不影響規格說明，保證了可移植性。
　　支持多機系統，但要同樣環境。
　　此時產生了劃時代的面向對象技術。

1995—2000，第三次分離，對象使用和對象實現的分離

　　基於構件開發：

　　標準化的軟件構件如同硬件IC，可插拔，使用者只用外特性，不計內部實現。

主要參考：

http://blog.sina.com.cn/s/blog_473d5bba010001x9.html

２、規格化設計為什麽得到人們的重視？

規格化設計在單人、短期、一次性項目開發中作用並不明顯，但是大量的軟件開發項目並不符合以上幾個特點。

　　·對多人開發而言，好的規格設計大大增強代碼可讀性，便於在程序員之間共享。利於分工協作，從而提高開發效率。

　　·對長期、非一次性項目而言，規格設計能夠減小“遺忘成本”，降低開發人員變動的代價，幫助後來的設計者更好理解函數（方法）作用而忽視具體實現細節，利於後期維護。

３、Ｂｕｇ分析

　　由上表來看，規格bug和功能bug之間並沒有太大的聚集關系，很大程度上是因為設計規格和構想代碼實現之間順序顛倒，以後要在這方面多加註意。

４、不規範的JSF及改進

①沒有對傳入參數不能為null加以約束。

/**
     * @MODIFIES: rq, inq;
     * @EFFECTS: rq == _rq && inq == _inq;
     */
＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝
/**
     * @REQUIRES: _rq != null && _inq != null;
     * @MODIFIES: this;
     * @EFFECTS: rq == _rq && inq == _inq;
     */

②沒有對出租車各參量範圍加以限制。

/**
     * @REQUIRES: None;
     * @MODIFIES: this;
     * @EFFECTS:  sets == _s && setc == c && setx == x && sety == y && wcount == 0 && needset == true;
     */
==========================
/**
     * @REQUIRES: 0<= credit < 1000 && 0 <=x,y<80 && 0<=_s<4;
     * @MODIFIES: this;
     * @EFFECTS:  sets == _s && setc == c && setx == x && sety == y && wcount == 0 && needset == true;
     */

③effects描述不完整

/**
     * @REQUIRES: detail != null;
     * @MODIFIES: OutputStream;
     * @EFFECTS: \file(E:\\detail.txt).size >= \old(\file(E:\\detail.txt)).size;
     */
＝＝＝＝＝＝＝＝＝＝＝＝＝＝
/**
     * @REQUIRES: detail != null;
     * @MODIFIES: OutputStream;
     * @EFFECTS: \file(E:\\detail.txt).size == \old(\file(E:\\detail.txt)).size + \old(detail).size && detail.equals(">>>>>>>>>>>");
     */ 

④

    /**
     * @REQUIRES: lt >= 0;
     * @MODIFIES: sta, begin;
     * @EFFECTS: \result == \old(lt)+1000;
     */
＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝
    /**
     * @REQUIRES: lt >= 0;
     * @MODIFIES: sta, begin;
     * @EFFECTS: \result == \old(lt)+1000 && wcount == 0 && lastdir == Direc.NO;
     */

⑤

/**
     * @REQUIRES: lt >= 0;
     * @MODIFIES: posi, sta, detail, task;
     * @EFFECTS: \result == \old(lt)+500+waittime || \result == \old(lt)+1000;
     */
＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝
    /**
     * @REQUIRES: lt >= 0;
     * @MODIFIES: posi, sta, detail, task;
     * @EFFECTS: \result == \old(lt)+500+waittime && detail.equals(\old(detail)+出租車該次形式信息);
     */

５、心得體會

　　規格設計所帶來的好處不言而喻，但前提是有一套邏輯嚴密並且同學們能夠深入理解的規格體系。在這三次作業的JSF中，無論是從自己的代碼，還是被測同學的代碼中，都能發現一個嚴重的問題：要麽JSF書寫不完整，要麽出現了大量的自然語言（而這是被禁止的）。究其原因，在這幾次JSF作業中，同學們能夠參考的、成體系的文檔只有第九次作業下發的簡略的JSF使用說明和幾個簡單的使用樣例。但不可避免的，每人對作業實現方式彈性大，程序中個別方法功能較復雜，僅從簡單的樣例很難推測出正確的JSF表達方法。

　　另外，開始寫JSF時已經實現了簡單的出租車系統，即使後來的設計新增了一些功能，很多人規格設計和代碼實現仍然會次序顛倒。

　　不過，學會規格設計的思想還是很重要的，JSF書寫的練習也算是小有幫助吧。

JSF３次作業總結