OO做業總結（三）

類規格設計

 因爲沒能找到關於類規格設計的發展歷史，因此結合程序設計思想的發展來談談規格化設計。

最先的程序設計都是採用機器語言來編寫的,直接使用二進制碼來表示機器可以識別和執行的指令和數 據。簡單來講,就是直接編寫 0 和 1 的序列來表明程序語言。機器語言由機器直接執行,速度快,但一個很明顯的缺點就是:寫起來實在是太困難了；因而有了面向過程變成，相比面向機器的思想來講,面向過程是一次思想上的飛躍,將程序員從複雜的機器操做和運行的細節中解放出來,轉而關注具體須要解決的問題;面向過程的語言也再也不須要和具體的機器綁定,從而具有了移植 性和通用性;面向過程的語言自己也更加容易編寫和維護。這些因素疊加起來,大大減輕了程序員的負擔, 提高了程序員的工做效率,從而促進了軟件行業的快速發展。

但在這種設計模式下，不可避免的會產生面條式的代碼，極大地限制了程序的規模——結構化設計應運而生：它是一種編程範型，採用子程序（函數就是一種子程序）、代碼區塊、for循環以及while循環等結構，來替換傳統的goto。但願藉此來改善計算機程序的明晰性、質量以及開發時間，而且避免寫出麪條式代碼，這就是規格化設計的起源，而且一直髮展至今。

在實際的生活中，開發都是以團隊爲單位的，團隊之間的交流主要是經過代碼，因此代碼要具備可讀性；同時，實際的生活中代碼的維護也是至關重要的，而維護代碼的那些人卻並不必定是代碼的做者，這就更要求代碼要具備很好的可維護性；另外，在咱們開發程序的過程當中，規格的設計更有助於避免浪費更多的時間來debug，若是一開始設計好了規格，而後嚴格按照這個規格來完成代碼，能夠很好的避免功能性bug。所以，因爲以上列舉出來的部分優勢，這些看似優勢浪費時間的類規格一直在人們心中佔據重要的位置。

bug分析

本次課程若是燒腦的地方除了互測估計就是這個jsf的書寫了，並非說難度很大，而是要寫得真正的規範感受太難，並且很耗時間，寫了這麼多規格並無很大的收穫。因此這幾回的規格都是寫完了方法而後後面來添加的，並無達到規格應有的左右，好比實驗課上先寫規格而後再寫方法代碼。這幾回做業測我程序的同窗都很nice，並無扣我規格的bug。

關於功能性的bug，因爲這幾回做業是在第七次做業的基礎上進行修改，因此只要實現了指導書的要求，應該能很好的避免功能性bug。第十一次做業被同窗報了一個功能bug，是關於走回頭路的。我本身本地跑了一下他的測試代碼（全部的車初始化在一個點，並且該點周圍只有一條邊），現象是根本看不出現象，多是由於電腦太卡了吧也多是程序自己就有問題，不過我依然以爲這種測試樣例可能大部分代碼跑出來效果都同樣，因此本身也沒去管這個bug了。 

很差的寫法和改進

（1）如下是我出租車類中設置狀態的方法：

/**@REQUIRE: None;
 * @MODIFIES: status;
 * @EFFECTS:
 * (s == 3) ==> status == Status.STILL;
 * (s == 0) ==> status == Status.SERVE;
 * (s == 2) ==> status == Status.WAIT;
 * (s == 1) ==> status == Status.GOTORDER;
 * @ THREAD_EFFECTS:\locked();
 */

　　

以上的規格感受應該是合理的，就是以爲有點醜，因此稍微改了一下（可能仍是很醜）：

    /**@REQUIRE: None;
     * @MODIFIES: status;
     * @EFFECTS:
      (s == 3) ==> status == Status.STILL   ||
      (s == 0) ==> status == Status.SERVE   ||
      (s == 2) ==> status == Status.WAIT    ||
      (s == 1) ==> status == Status.GOTORDER;
     * @ THREAD_EFFECTS:\locked();
     */　　

（2）如下是我出租車類中的設置目標點的規格：

    /**
     * @ MODIFIES: to;
     * @ EFFECTS:
     * this.to == to;
     * @ THREAD_EFFECTS:\locked();
     */　　

而這個方法的實現是這樣的：

    public synchronized void setTo(Point p) {

        to.setLocation(p.x, p.y);
    }

很明顯這個規格的REQUIRE是要寫的，因此改進以下：

   /**@ REQUIRES: p != null;
     * @ MODIFIES: to;
     * @ EFFECTS:
     * this.to == to;
     * @ THREAD_EFFECTS:\locked();
     */

（3）如下是我週期爲7.5s的監控線程的構造方法 ，同理其REQUIRE也有問題：

   /**
     @ MODIFIES:    TIME; taxi; from; to; num;
     @ EFFECTS:
     this.TIME == TIME; this.taxi == taxi;
     this.num == num; this.from == from;
     this.to == to;
     */

　改進：

   /**@REQUIRE: taxi != null; from != null; to != null; TIME >= 0;
     @ MODIFIES:    TIME; taxi; from; to; num;
     @ EFFECTS:
     this.TIME == TIME; this.taxi == taxi;
     this.num == num; this.from == from;
     this.to == to;
     */　　

（4）接下來是我調度類中的一個獲取出租車信息的方法的規格：

    /**@ REQUIRES: str != {};
     @ MODIFIES:    None;
     @ EFFECTS:
        (\exist int i; 0 <= i < str.length; str.charAt(i) >= '0' && str.charAt(i) <= '9')
        && (\all int j; 0 <= j < i; str.charAt(j) < '0' || str.charAt(j) > '9')
        && (\exist int k; i <= k < str.length; str.charAt(k) >= '0' && str.charAt(k) <= '9')
        && (k+1 >= str.length || str.charAt(k+1) < '0' || str.charAt(k+1) > '9')
        && (\all int l; i <= l <= k; str.charAt(l) >= '0' && str.charAt(l) <= '9')
        ==> (\result == new Point(Integer.parseInt(str.substring(i, k+1), k+1)));
     */

　　乍一看感受很合理，可是仔細看卻發現有錯誤：好比第一個邏輯表達式中定義的i的做用域只有第一行代碼，並不能被後面的代碼所識別，改進以下：

    /**@ REQUIRES: str != {};
     @ MODIFIES:    None;
     @ EFFECTS:
        (\exist int i; 0 <= i < str.length; (str.charAt(i) >= '0' && str.charAt(i) <= '9'
        && (\all int j; 0 <= j < i; str.charAt(j) < '0' || str.charAt(j) > '9')
        && (\exist int k; i <= k < str.length; str.charAt(k) >= '0' && str.charAt(k) <= '9')
        && (k+1 >= str.length || str.charAt(k+1) < '0' || str.charAt(k+1) > '9')
        && (\all int l; i <= l <= k; str.charAt(l) >= '0' && str.charAt(l) <= '9'))
        ==> (\result == new Point(Integer.parseInt(str.substring(i, k+1), k+1)));
     */

　　改進以後就能夠改變上面的不足。

（5）接下來是我十一次做業的特殊出租車的構造方法：

    /**@REQUIRES:
     *  No >= 0 && No < 100; mi != null; taxigui != null;
     * @MODIFIES:
     *  No; mi; taxigui;
     * @EFFECTS:
     *  this.mi == mi; this.taxigui == taxigui; this.No == No;
     */

　　這個規格和第四個規格相似，都感受是合理的，卻有一點點小問題，傳進來的taxigui不能保證是合法的，因此REQUIRE得重寫，改進以下：

    /**@REQUIRES:
     *  No >= 0 && No < 100 && mi != null && taxigui != null && taxigui.repOk();
     * @MODIFIES:
     *  No; mi; taxigui;
     * @EFFECTS:
     *  this.mi == mi; this.taxigui == taxigui; this.No == No;
     */

基本思路和體會

這幾回做業的規格都是在完成代碼以後添加的，因此不必定合乎要求，不過在實驗課上嘗試了先寫規格再寫代碼，以爲這樣的模式也還行，不過這就對設計的要求高了一些，若是一開始設計有誤，會浪費更多時間。

最後一次oo的代碼做業，好像並無什麼特別的感受，之後終於有更多時間作其餘事情了，開心。