OO第三次博客做業

1， 規格化設計的發展歷程

關於規格化設計一詞，能找到的資料實在少之又少。在筆者已經找到的資料中，筆者認爲，規格化設計來自於歷史上第一次軟件危機以後，雖然當時已經有了大量的面向過程式的編程語言譬如COBOL,BASIC,C語言等等，可是其中含有的大量的goto語句致使的麪條式代碼極大地限制了程序規模。

爲了解決如上的問題，人們提出告終構化程序設計這一中編程範型。它採用子程序（函數就是一種子程序）、代碼區塊、for循環以及while循環等結構，來替換傳統的goto。但願藉此來改善計算機程序的明晰性、質量以及開發時間，而且避免寫出麪條式代碼。

可是，因爲硬件的飛速發展，業務的需求愈來愈複雜，爆發了第二次軟件危機。這次危機主要體如今「可擴展性」，「可維護性」兩個方面。因爲傳統面向過程式的編程難以適應快速多變的業務需求，於是產生了面向對象式的編程思想。在筆者看來，規格化設計一詞，是在結構化設計的基礎上，爲了適應程序的「可擴展性」和「可擴展性」而衍生出來的重要設計思想。

一個通過優秀的規格化設計的程序，有着以下的優點：其一，有助於開發者們相互理解對方的程序，方便程序員之間的分工，加快開發速度。現在的工程，每每都是由一個團隊共同完成。那麼對於團隊中的成員來講，互相理解對方的代碼是十分重要的，這樣才能更好地完成某個項目。其次，對於編寫函數庫的程序員來講規格化設計更爲重要。其緣由就在於函數庫的使用者並不須要知曉庫程序員的代碼思路與實現過程，他只須要知道庫中的某個函數，它須要的參數是什麼，會對什麼數據進行修改，修改的效果是什麼，也就是咱們JSF中的REQUIRES,MODIFIES,EFFECTS三個重要的功能。其二，規格化的設計能很好地提升程序的「可擴展性」與「可維護性」。當開發者清楚本身所寫的每個方法的規格時，他可以很快速地針對每個bug追本溯源，找出問題所在。其次，在面對現在工程需求快速變化的狀況時，開發者經過規格化的設計能夠很好地瞭解本身的程序應該如何進行修改以適應需求的變化。

2，三次做業的規格BUG

筆者的後三次出租車的做業並無在規格上被測試者報告BUG，但這並不意味着筆者的規格便沒有任何的錯誤，僅僅是遇到了「心地善良」的測試者罷了。

那麼筆者便來本身細數本身在規格上出現的紕漏以及修改的方案。

3，JSF不規範的寫法以及改進

1)

 1 /**
 2      * @REQUIRES:(\all String str;str != null,path != null)
 3      * @MODIFIES:fw
 4      * @EFFECTS:
 5      *     (\all str != null) ==> fw.write(str+"\n"); 
 6      */
 7     public static void appendFile(String Path,String str) {
 8         try {
 9             File f = new File(path);
10             FileWriter fw = new FileWriter(f, true);
11             fw.write(str + "\n");
12             fw.close();
13         } catch(Exception e) {
14         }
15     }
16 }

該方法的的做用顯而易見，即是向文件中寫入信息，那麼該方法的JSF出了什麼紕漏呢？

首先咱們對REQUIRES的定義是什麼？它的定義是前置條件，也就是執行該方法前對該輸入或者系統狀態的要求。

該方法的前置條件是字符串str的含義是文件的路徑，那麼其前置條件即是str是合法的文件路徑，而源代碼中的前置條件僅僅強調了path != null，顯然這並無知足要求。

而MODIFIES的定義反作用，是對input的修改，即對輸入的修改。顯而易見的是，本方法並無對輸入進來的str進行任何修改，所以沒法知足要求。

最後的EFFECTS的定義是後置條件，即執行後的返回結果或者系統狀態應該知足的約束。本方法對系統形成的影響是往文件中寫入字符串

所以對該規格的改進爲：

 1 1 /**
 2  2      * @REQUIRES:(str!=null) && (path is a legitimate file path) 
 3  3      * @MODIFIES:none
 4  4      * @EFFECTS:
 5  5      *     (\all str != null) ==> fw.write(str+"\n"); 
 6  6      */
 7  7     public static void appendFile(String Path,String str) {
 8  8         try {
 9  9             File f = new File(path);
10 10             FileWriter fw = new FileWriter(f, true);
11 11             fw.write(str + "\n");
12 12             fw.close();
13 13         } catch(Exception e) {
14 14         }
15 15     }
16 16 }

2)

 1 /**
 2      * @REQUIRES:Point p,q;int f;
 3      * @MODIFIES:flow[][];
 4      * @EFFECTS:
 5      *     (isAdh(p,q) == false) ==> (/result == false);
 6      *     (isAdh(p,q) == true) ==> (/result == true)&&(flow[getPointId(p)][getPointId(q)] == flow[getPointId(p)][getPointId(q)]+f)&&(flow[getPointId(q)][getPointId(p)] == flow[getPointId(q)][getPointId(p)]+f);
 7      */
 8     public boolean addFlow(Point p, Point q, int f) {
 9         if(!isAdj(p, q)) {
10             return false;
11         }
12         synchronized(flow) {
13             flow[getPointId(p)][getPointId(q)] += f;
14             flow[getPointId(q)][getPointId(p)] += f;
15         }
16         return true;
17     }

該方法的REQUIRES不符合要求，應該要標明p，q和f的要求等狀況

修改方法以下所示

/**
     * @REQUIRES:(Point p,q;p!=null,q!=null;int f,f > 0);
     * @MODIFIES:flow[][];
     * @EFFECTS:
     *     (isAdh(p,q) == false) ==> (/result == false);
     *     (isAdh(p,q) == true) ==> (/result == true)&&(flow[getPointId(p)][getPointId(q)] == flow[getPointId(p)][getPointId(q)]+f)&&(flow[getPointId(q)][getPointId(p)] == flow[getPointId(q)][getPointId(p)]+f);
     */
    public boolean addFlow(Point p, Point q, int f) {
        if(!isAdj(p, q)) {
            return false;
        }
        synchronized(flow) {
            flow[getPointId(p)][getPointId(q)] += f;
            flow[getPointId(q)][getPointId(p)] += f;
        }
        return true;
    }

3)

/**
     * @MODIFIES: None
     * @EFFECTS: /result == dist[getPointId(q)];
     */
    public int getDistance(Point p, Point q) {
        int[] dist = new int[map_size * map_size];
        int[] minFlow = new int[map_size * map_size];
        Point[] prev = new Point[map_size * map_size];
        minPath(p, q, dist, minFlow, prev);
        return dist[getPointId(q)];
    }

本方法沒有寫清楚前置條件和反作用

該方法並不只僅是得到p，q兩點之間的距離，它爲了獲得這個距離尋找了兩點之間的最短路徑，所以會有必定的反作用。

修改方法以下所示：

 1 /**
 2      *REQUIRES:(Point p,q;p != null,q != null);
　　　　  * @MODIFIES: minPath(p, q, dist, minFlow, prev);
 3      * @EFFECTS: /result == dist[getPointId(q)];
 4      */
 5     public int getDistance(Point p, Point q) {
 6         int[] dist = new int[map_size * map_size];
 7         int[] minFlow = new int[map_size * map_size];
 8         Point[] prev = new Point[map_size * map_size];
 9         minPath(p, q, dist, minFlow, prev);
10         return dist[getPointId(q)];
11     }

4，功能BUG與規格BUG的聚焦分析

筆者的功能BUG與規格的BUG之間並無太大的聯繫，可能緣由在於筆者是在寫完整個程序以後方纔寫的規格，並且因爲部分方法所完成的功能太多，行數過長，於是致使JSF難以完成，所以這部分的JSF筆者並無很好地去完善，測試者也並無認真地去追究這些問題。

3，設計規格和撰寫規格的基本思路和體會

筆者在完成這三次做業的時候，是先寫完整個程序以後再去寫的每一個方法和類的規格，仔細分析，有好有壞，可是弊大於利。其好處就在於寫程序的時候不須要考慮的規格的問題，於是能提升速度。可是缺點也很明顯，因爲沒有事先設計好規格，沒有仔細明確每一個方法的要求，目的，以及反作用，在後期DEBUG的時候會形成巨大的困擾——不知道到底是哪一個類，哪一個方法的問題。所以，痛定思痛事後，仍是應該養成先肯定好每一個類的目標，即Overview，再肯定爲了完成這些目標所須要的方法，肯定其REQUIRES,MODIFIES,EFFECTS，而後再依據本身的規格去實現本身的代碼。我想這樣的話可以減小很多DEBUG的時間，也能達到規格化訓練的目的。更加劇要的是，這樣作能夠更加方便測試者理解而且測試你的程序，利己利人，何樂而不爲呢？

以上即是筆者對於這三次做業的拙見，OO這門課即將到達尾聲，一路走來經歷了太多，正如那句耳熟能詳的話語：OO不易，和諧6系。爲了完成做業常常熬夜通宵什麼的確實付出了不少，但一樣的是，咱們收穫的，也不少！