OO第三次博客總結

1、規格化設計的大體發展歷史

　　最初的代碼所做用的對象是單獨的私人計算機，也就沒有了規格化設計的必要。大量語言的新增和軟件的不可靠，致使了20世紀60年代爆發的「軟件危機」，清晰的自此文檔引發了人們的關注。規格化帶來了諸多優勢，在此後的30年時間裏，逐步發展，加強了程序的可讀性，更便於進一步修改和移植。規格化的一步步發展，產生了基於邏輯、代數等多種形式的規格說明，爲軟件的開發和維護帶來了巨大便利。

 

2、 BUG分析

第九次

BUG內容	BUG類型	BUG代碼行數	BUG緣由	方法名
輸出信息缺乏	ERROR	20	LoadFile中叫車請求產生忘了輸出	public void LoadRequest()
初始出租車爲準備服務狀態	ERROR	20	對LoadFIle中初始設置爲準備接客的車沒有設置乘客的目的地，車輛中止	public void LoadRequest()
搶單服務->搶單出租車不是信用最高的車輛	ERROR	9	沒有對車輛credit和流量flow設置最大值，致使被爆int	public Taxi()

 沒有規格bug。

 

第十次

BUG內容	BUG類型	BUG代碼行數	BUG緣由	方法名
程序測試->正常功能測試-紅綠燈->目前紅燈->出租車下一步即將：直行	ERROR	40	送客車輛在等燈時出現了屢次停留	public void moveToDest()
程序測試->針對歷史版本的迴歸測試->是否選擇流量最少路徑	ERROR	40	對流量的處理有誤	public void analyse_req()
程序測試->針對歷史版本的迴歸測試->隨機行走的時候沒有走流量最少的路徑	ERROR	40	流量清除過快	public void analyse_req()
程序測試->正常功能測試-紅綠燈->紅綠燈時間計算有問題	ERROR	40	檢查發現沒有按想象中最近要動車輛計算，而是500ms運行一次	public void analyse_req()
規格檢查->方法規格檢查->Effects 不完整	規格	30	effects不全	public void LoadRequest()
規格檢查->方法規格檢查->Requires 不完整	規格	1	requires不全	public void set_curPoint()

彙集關係：無

 

第十一次

BUG內容	BUG類型	BUG代碼行數	BUG緣由	方法名
程序測試->正常功能測試-紅綠燈->目前紅燈->出租車下一步即將：直行	ERROR	40	送客車輛在等燈時出現了屢次停留	public void moveToDest()
規格檢查->方法規格檢查->Modifies 不完整	規格	20	modifies不完整	public void LoadFlow()
規格檢查->方法規格檢查->Modifies 不完整	規格	10	modifies不完整	public boolean startRead()
規格檢查->方法規格檢查->Requires 不完整	規格	30	requires不完整	public void readmap()
規格檢查->方法規格檢查->Requires 不完整	規格	1	requires不完整	public synchronized Request get_i()
規格檢查->方法規格檢查->Requires 不完整	規格	30	requires不完整	public void get_Range()
規格檢查->方法規格檢查->Requires 不完整	規格	20	requires不完整	public void addToCallList()
規格檢查->方法規格檢查->Requires 不完整	規格	40	requires不完整	public boolean chooseTaxi()
規格檢查->方法規格檢查->Modifies 不完整	規格	60	modifies不完整	public void analyse_req()
規格檢查->方法規格檢查->Modifies 不完整	規格	10	modifies不完整	public void move_stopping()
規格檢查->方法規格檢查->Modifies 不完整	規格	10	modifies不完整	public void move()

彙集關係：無

規格bug產生緣由：不少requires比較隱含，沒有想到。此外還有對上一次代碼的修改，卻沒有修改JSF內容，致使被報bug。

 

3、 很差寫法

前置條件：

對傳入參數要加以限制：

// 錯誤
    /**
    * @REQUIRES : None;
    */
    public synchronized Request get_i(int i) {
        return requestList.get(i);
    }

// 改進
    /**
    * @REQUIRES : i>0;
    */
    public synchronized Request get_i(int i) {
        return requestList.get(i);
    }

=和==傻傻分不清楚：

// 錯誤
　　/**
　　* @REQUIRES: x=(xi,xj);0<=xi<80 & 0<=xj<80；
　　*/
// 改進
　　/**
　　* @REQUIRES: x == (xi, xj); 0 <= xi<=80 & 0<=xj<=80;
　　*/

 前置應該爲bool表達式：

// 錯誤
　　/**
     * @REQUIRES: index is from 0 to 100;
     */
    public TaxiCar(int index) {     
        this.index = index;
    }
// 改進
　　/**
     * @REQUIRES: 0<=index<100;
     */
    public TaxiCar(int index) { 
        this.index = index;
    }

範圍錯誤：

// 錯誤
   /**
   * @REQUIRES: n>0 && n<100
   */
　　public void taxiControl(int n) {

    }
// 正確
   /**
   * @REQUIRES: n>=0 && n<100
   */
　　public void taxiControl(int n) {

    }

優先級錯誤：

// 錯誤
　　/**
     * @REQUIRES: req != null && index >= 80 || index < 0;
     */
    public Record(Request req, int index) {
        this.req = req;
        this.index = index;
    }
// 改進
　　/**
     * @REQUIRES: req != null && (index >= 80 || index < 0);
     */
    public Record(Request req, int index) {
        this.req = req;
        this.index = index;
    }

後置條件：

=和==不分：

// 錯誤
    /**
    * @EFFECTS : \result = Main.time;
    */
    public synchronized long getTime(int num)
    {
        return Main.time;
    }
// 改進  
        /**
    * @EFFECTS : \result == Main.time;
    */
    public synchronized long getTime(int num)
    {
        return Main.time;
    }   

使用天然語言：

// 錯誤
/*
* @EFFECTS: initialize the new Taxi；
*/
// 改進
/*
* \this.num == num;
*/

未處理拋出的異常：

// 錯誤
　　/**

　　* @EFFECTS:   \result == \min a;
　　*/
　　public static int min (int[ ] a) throws NullPointerException, EmptyException 
// 改進
　　/**@ EFFECTS:   normal_behavior
                \result == \min a;
　　(a == null) ==> exceptional_behavior (NullPointerException);
　　(a.length == 0) ==> exceptional_behavior (EmptyException);
　　*/
　　public static int min (int[ ] a) throws NullPointerException, EmptyException 

後置條件不完整：

// 錯誤
    /**
     * @EFFECTS : AskList.contains(ask);
     */
    public synchronized void addAsk(Ask ask){
        AskList.add(ask);
    }
// 改進
    /**
     * @EFFECTS : AskList.contains(ask) && AskList.size == \old(AskList).size + 1;
     */
    public synchronized void addAsk(Ask ask){
        AskList.add(ask);
    }

格式不正確：

// 錯誤
     /*
     *  @ EFFECTS:  (this.map==null||this.map.length==0) \result = false;
                    \result = true;
     */
    public boolean repOK() {
       
    }
// 改進
    /*
     *  @ EFFECTS:  (this.map==null||this.map.length==0)==> \result = false;
                    \result = true;
     */
    public boolean repOK() {
       
    }

 

4、 思路和體會

　　要寫好規格就要從新讀懂本身寫的函數，尤爲注意前置條件經常隱含。另外出現對代碼的修改時，要及時修改JSF，以避免JSF與代碼不配套。JSF被扣10分我是很無奈的……