調研，然後總結介紹規格化設計的大致發展歷史和為什麽得到了人們的重視

emmm為這個問題翻遍百度谷歌知乎也沒有得到答案，那我就把自己認為最重要的兩點簡要說明一下吧，歡迎大家補充~

1、便於完成代碼的重用交接。

　　烏雞老師上課說到，一個代碼被重用的頻率越高，說明設計的水平越高。好的代碼一定是為他人提供便利的。而這種便利也包括引用時的確定性，調用者可以按照自己的需求和這份代碼規格對照，因此確定自己使用這個接口的安全性可靠性。並且，代碼規格也說明了調用者可視範圍內變量的變化情況，否則這種重用將是非常非常危險的。因此，規格和代碼的貼合性也變得很重要。

2、便於程序員按照真正的意願做好代碼實現和測試。

　　編程語言畢竟是自然語言之外的第二種語言，人是按照思維生成的邏輯去構造代碼實現的。而把要實現的內容完全放在腦子裏沒有進行仔細的分類梳理，在代碼越來越復雜的情況下很容易產生疏漏，也就是實現有BUG。但測試也是按照代碼邏輯產生慣性思維，所以很難找到思維漏洞的BUG。然後...然後你就變成了“我司雇來寫專門BUG的程序員”，然後你就涼了。

　　但規格是一種思維強制，強迫你按照你的預想去實現、去測試（有點像BUG樹的作用原理）、去分類，只要規格和實現完全一致，最初有思維漏洞或許可以降低檢查難度到規格層。

按照作業，針對自己所被報告的規格bug以及雷同的規格bug（限於 bug樹的限制，對手無法上報），列一個表格分析

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

這兩個JSFbug都出現在第九次作業，而且錯誤原因基本都一樣。這次作業因為一些特殊原因完成的特別倉促，也沒有進行檢查測試。產生的主要原因當然有時間方面的原因，更重要的是這兩個方法的確也比較長。

當然，我的JSFbug水平咋樣我心裏還是很有筆數的，用自然語言也比較多。只是碰上的同學都比較友好，水平不高也沒有被針對，但在三次作業中，我每次都對JSF進行優化，存在的問題選五個在下面介紹。

分別列舉5個前置條件和5個後置條件的不好寫法，並給出改進寫法

前置條件部分：

參數範圍描述不準確

例1

修改前：

/**
     * @REQUIRES:(\all int id;); 
     *              (\all int X;);
     *           (\all int Y;); 
     * @MODIFIES: cars_ID;carX;carY;carCredit;carStatus;hasTask;now_request;load_result;
     * @EFFECTS: Set these variables to their initial values;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS: 
     */
    public CarInformation(int id,int X,int Y) {
        this.carID=id;
        this.carX=X;
        this.carY=Y;
        this.carCredit=0;//信用值0
        this.carStatus=2;//等待服務狀態
        this.hasTask=false;//沒有任務
        this.now_request=null;
        this.load_result=false;
    //    System.out.println("出租車信息初始化成功");
    }

修改後：

/**
     * @REQUIRES:(\all int id;0<=id<100); 
     *              (\all int X;0<=X<80);
     *           (\all int Y;0<=Y<80); 
     * @MODIFIES: cars_ID;carX;carY;carCredit;carStatus;hasTask;now_request;load_result;
     * @EFFECTS: Set these variables to their initial values;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS: 
     */
        public CarInformation(int id,int X,int Y) {
        this.carID=id;
        this.carX=X;
        this.carY=Y;
        this.carCredit=0;//信用值0
        this.carStatus=2;//等待服務狀態
        this.hasTask=false;//沒有任務
        this.load_result=false;
    //    System.out.println("出租車信息初始化成功");
    }

例2

修改前：

/**
     * @REQUIRES:(\all int carX2;);
     *              (\all int carY2;);
     *              (\all ArrayList<Vertex> nei_Lis;);
     * @MODIFIES: None;
     * @EFFECTS: \result==new_aim;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS: 
     */
    public int Find_WhenCase2(int carX2, int carY2, ArrayList<Vertex> nei_Lis) {//在等待狀態尋找一條流量最小的道路
        int min_flownum=100000000;
        int new_aim=-1;
        for(int i=0;i<nei_Lis.size();i++) {
            int ID=nei_Lis.get(i).getID();
            int index=transIndex(ID,carX*80+carY);
            //System.out.println("進入循環，CARX CARY"+carX+" "+carY);
            if((Flow_List[carX*80+carY][index].Get_open())&&(Flow_List[carX*80+carY][index].Get_Lastflow()<min_flownum)) {
                min_flownum=Flow_List[carX*80+carY][index].Get_Lastflow();
                new_aim=i;
            }
        }
        return new_aim;
    }

修改後：

/**
     * @REQUIRES:(\all int carX2;0<=carX2<80);
     *              (\all int carY2;0<=carY2<80);
     *              (\all ArrayList<Vertex> nei_Lis;);
     * @MODIFIES: None;
     * @EFFECTS: \result==new_aim;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS: 
     */
    public int Find_WhenCase2(int carX2, int carY2, ArrayList<Vertex> nei_Lis) {//在等待狀態尋找一條流量最小的道路
        int min_flownum=100000000;
        int new_aim=-1;
        ArrayList<Integer> roadaim=new ArrayList<Integer>();
        for(int i=0;i<nei_Lis.size();i++) {
            int ID=nei_Lis.get(i).getID();
            int index=transIndex(ID,carX*80+carY);
            //System.out.println("進入循環，CARX CARY"+carX+" "+carY);
            if((Flow_List[carX*80+carY][index].Get_open())&&(Flow_List[carX*80+carY][index].Get_Lastflow()<min_flownum)) {
                min_flownum=Flow_List[carX*80+carY][index].Get_Lastflow();
                roadaim.clear();
                roadaim.add(i);
            }else if((Flow_List[carX*80+carY][index].Get_open())&&(Flow_List[carX*80+carY][index].Get_Lastflow()==min_flownum)) {
                roadaim.add(i);
            }
        }
        Random random=new Random(); 
        int begin=0;
        int end=roadaim.size()-1;
        new_aim=roadaim.get(random.nextInt(end - begin + 1) + begin);
        return new_aim;
    }

例3：

修改前：

/**
     * @REQUIRES:(\all int x;); 
     * @MODIFIES: carX;
     * @EFFECTS: carX==x;
     * @THREAD_REQUIRES:\locked(this); 
     * @THREAD_EFFECTS: \locked(); 
     */
    public synchronized void setcarX(int x) {this.carX=x;}

修改後：

/**
     * @REQUIRES:(\all int x;0<=x<80); 
     * @MODIFIES: carX;
     * @EFFECTS: carX==x;
     * @THREAD_REQUIRES:\locked(this); 
     * @THREAD_EFFECTS: \locked(); 
     */
    public synchronized void setcarX(int x) {this.carX=x;}

例4：

修改前：

/**
     * @REQUIRES:(\all int i;); 
     * @MODIFIES: carStatus;
     * @EFFECTS: carStatus==i;
     * @THREAD_REQUIRES:\locked(this); 
     * @THREAD_EFFECTS: \locked(); 
     */
    public synchronized void setcarStatus(int i) {this.carStatus=i;}

修改後：

/**
     * @REQUIRES:(\all int i;i=0/1/2/3;); 
     * @MODIFIES: carStatus;
     * @EFFECTS: carStatus==i;
     * @THREAD_REQUIRES:\locked(this); 
     * @THREAD_EFFECTS: \locked(); 
     */
    public synchronized void setcarStatus(int i) {this.carStatus=i;}

例5：

修改前：

/**
     * @REQUIRES:(\all int beginX;); 
     *              (\all int beginY;); 
     *           (\all int endX;);
     *           (\all int endY;);
     *           (\all long request_time;);
     * @MODIFIES: beginX;beginY;endX;endY;request_time;AreaX1 to AreaX4;AreaX1 to AreaX4;AreaY1 to AreaY4;
     * @EFFECTS: Set these variables to their initial values;Create area;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS: 
     */
    public Request(int beginX,int beginY,int endX,int endY,long request_time) {
        this.beginX=beginX;
        this.beginY=beginY;
        this.endX=endX;
        this.endY=endY;
        this.request_time=request_time;
        CreateArea();
    }

修改後：

/**
     * @REQUIRES:(\all int beginX;0<=beginX<80;); 
     *              (\all int beginY;0<=beginY<80;); 
     *           (\all int endX;0<=endX<80;);
     *           (\all int endY;0<=endY<80;);
     *           (\all long request_time;request_time>=0;);
     * @MODIFIES: beginX;beginY;endX;endY;request_time;AreaX1 to AreaX4;AreaX1 to AreaX4;AreaY1 to AreaY4;
     * @EFFECTS: Set these variables to their initial values;Create area;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS: 
     */
    public Request(int beginX,int beginY,int endX,int endY,long request_time) {
        this.beginX=beginX;
        this.beginY=beginY;
        this.endX=endX;
        this.endY=endY;
        this.request_time=request_time;
        CreateArea();
    }

後置條件：

主要是自然語言描述以及沒有對輸入非法參數的情況描述

例1：

修改前：

/**
     * @REQUIRES:(\all int id;0<=id<100); 
     *              (\all int X;0<=X<80);
     *           (\all int Y;0<=Y<80); 
     * @MODIFIES: cars_ID;carX;carY;carCredit;carStatus;hasTask;now_request;load_result;
     * @EFFECTS: Set these variables to their initial values;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS: 
     */
        public CarInformation(int id,int X,int Y) {
        this.carID=id;
        this.carX=X;
        this.carY=Y;
        this.carCredit=0;//信用值0
        this.carStatus=2;//等待服務狀態
        this.hasTask=false;//沒有任務
        this.load_result=false;
    //    System.out.println("出租車信息初始化成功");
    }

修改後：

/**
     * @REQUIRES:(\all int id;0<=id<100); 
     *              (\all int X;0<=X<80);
     *           (\all int Y;0<=Y<80); 
     * @MODIFIES: cars_ID;carX;carY;carCredit;carStatus;hasTask;now_request;load_result;
     * @EFFECTS: this.carID==id;this.carX==X;this.carY==Y;this.carCredit==0;this.carStatus==2;this.hasTask==false;this.load_result==false;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS: 
     */
        public CarInformation(int id,int X,int Y) {
        this.carID=id;
        this.carX=X;
        this.carY=Y;
        this.carCredit=0;//信用值0
        this.carStatus=2;//等待服務狀態
        this.hasTask=false;//沒有任務
        this.load_result=false;
    //    System.out.println("出租車信息初始化成功");
    }

例2：

修改前：

/**
     * @REQUIRES:(\all Flow_Count fl;); 
     *              (\all CarInformation[] cars_info;);
     *           (\all Request_List list;); 
     * @MODIFIES: flowlist;cars_info;list;
     * @EFFECTS: Set these variables to their initial values;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS: 
     */
    public MakeMap(Flow_Count fl,CarInformation[] cars_info,Request_List list,TaxiGUI g) {
        this.flowlist = fl;
        this.cars_info=cars_info;
        this.list=list;
        this.gui=g;
    }

修改後：

/**
     * @REQUIRES:(\all Flow_Count fl;); 
     *              (\all CarInformation[] cars_info;);
     *           (\all Request_List list;); 
     * @MODIFIES: flowlist;cars_info;list;
     * @EFFECTS: this.flowlist == fl;
        this.cars_info==cars_info;
        this.list==list;
        this.gui==g;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS: 
     */
    public MakeMap(Flow_Count fl,CarInformation[] cars_info,Request_List list,TaxiGUI g) {
        this.flowlist = fl;
        this.cars_info=cars_info;
        this.list=list;
        this.gui=g;
    }

例3：

修改前：

/**
     * @REQUIRES: A file with the correct format and content;
     * @MODIFIES: The neighbor‘s sequence of vertices and the value of the adjacency matrix;
     * @EFFECTS:Convert the values in a file to node connections;
     * @THREAD_REQUIRES: 
     * @THREAD_EFFECTS: 
     */
    public void CreateMap() {//根據文件創建地圖
}

修改後：

/**
     * @REQUIRES: A file with the correct format and content;
     * @MODIFIES: The neighbor‘s sequence of vertices and the value of the adjacency matrix;
     * @EFFECTS:for(\all char c;c in file）
                     (c==‘1‘)==>road is opened;
                     (c==‘0‘)==>road is closed;
                     (!((c==‘0‘)&&(c==‘1‘)))==>system.exit(0);
     * @THREAD_REQUIRES: 
     * @THREAD_EFFECTS: 
     */
    public void CreateMap() {//根據文件創建地圖
}                

例4：

修改前：

/**
     * @REQUIRES: (\all int id;);
     * @MODIFIES: System.out;
     * @EFFECTS: find taxi by id;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS:
     */
    public void checkBYcarID(int id) {// 通過汽車ID查詢
        if (id >= 100) {
            System.out.println("ID越界，查詢失敗");
            return;
        }
        FileWriter fw;
        File printFile = new File(String.format("e://taxi3.txt",id));
        if (!printFile.exists()) {
            try {
                printFile.createNewFile();
            } catch (IOException e) {
                // TODO Auto-generated catch block
                e.printStackTrace();
            }
        }

        try {
            fw = new FileWriter(printFile, true);
            @SuppressWarnings("resource")
            PrintWriter pw = new PrintWriter(fw);

            CarInformation info = car_list[id];
            System.out.println("查詢時刻(100ms為基本單位):" + (long) System.currentTimeMillis() / (long) 100);
            pw.println("查詢時刻(100ms為基本單位):" + (long) System.currentTimeMillis() / (long) 100);
            pw.flush();
            System.out.println("出租車當前坐標:(" + info.getcarX() + "," + info.getcarY() + ")");
            pw.println("出租車當前坐標:(" + info.getcarX() + "," + info.getcarY() + ")");
            pw.flush();
            String status = null;
            switch (info.getcarStatus()) {
            case 0:
                status = "服務狀態";
                break;
            case 1:
                status = "接單狀態";
                break;
            case 2:
                status = "等待狀態";
                break;
            case 3:
                status = "停止狀態";
                break;
            default:
                status = "非法未知狀態";
                break;
            }
            System.out.println("出租車當前狀態:" + status);
            pw.println("出租車當前狀態:" + status);
            pw.flush();
        } catch (IOException e) {
        }
    }

修改後：

/**
     * @REQUIRES: (\all int id;);
     * @MODIFIES: System.out;
     * @EFFECTS: (0<=id<100)==>find taxi by id;
                              (!(0<=id<100))==>return;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS:
     */
    public void checkBYcarID(int id) {// 通過汽車ID查詢
        if (id >= 100) {
            System.out.println("ID越界，查詢失敗");
            return;
        }
        FileWriter fw;
        File printFile = new File(String.format("e://taxi3.txt",id));
        if (!printFile.exists()) {
            try {
                printFile.createNewFile();
            } catch (IOException e) {
                // TODO Auto-generated catch block
                e.printStackTrace();
            }
        }

        try {
            fw = new FileWriter(printFile, true);
            @SuppressWarnings("resource")
            PrintWriter pw = new PrintWriter(fw);

            CarInformation info = car_list[id];
            System.out.println("查詢時刻(100ms為基本單位):" + (long) System.currentTimeMillis() / (long) 100);
            pw.println("查詢時刻(100ms為基本單位):" + (long) System.currentTimeMillis() / (long) 100);
            pw.flush();
            System.out.println("出租車當前坐標:(" + info.getcarX() + "," + info.getcarY() + ")");
            pw.println("出租車當前坐標:(" + info.getcarX() + "," + info.getcarY() + ")");
            pw.flush();
            String status = null;
            switch (info.getcarStatus()) {
            case 0:
                status = "服務狀態";
                break;
            case 1:
                status = "接單狀態";
                break;
            case 2:
                status = "等待狀態";
                break;
            case 3:
                status = "停止狀態";
                break;
            default:
                status = "非法未知狀態";
                break;
            }
            System.out.println("出租車當前狀態:" + status);
            pw.println("出租車當前狀態:" + status);
            pw.flush();
        } catch (IOException e) {
        }
    }

例5：

修改前：

/**
     * @REQUIRES: (\all int status;);
     * @MODIFIES: System.out;
     * @EFFECTS: find taxi by status;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS:
     */
    public void checkBYcarStatus(int status) {// 通過狀態查詢
        if (!((status == 0) || (status == 1) || (status == 2) || (status == 3))) {
            System.out.println("查詢狀態非法，查詢失敗");
            return;
        }
        for (int i = 0; i < 100; i++) {
            CarInformation info = car_list[i];
            if (info.getcarStatus() == status) {
                System.out.println("滿足條件的出租車編號:" + info.getcarID());
            }
        }
    }

修改後：

/**
     * @REQUIRES: (\all int status;);
     * @MODIFIES: System.out;
     * @EFFECTS:
 ((status == 0) || (status == 1) || (status == 2) || (status == 3))==>find taxi by status;
(!((status == 0) || (status == 1) || (status == 2) || (status == 3))) ==>return;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS:
     */
    public void checkBYcarStatus(int status) {// 通過狀態查詢
        if (!((status == 0) || (status == 1) || (status == 2) || (status == 3))) {
            System.out.println("查詢狀態非法，查詢失敗");
            return;
        }
        for (int i = 0; i < 100; i++) {
            CarInformation info = car_list[i];
            if (info.getcarStatus() == status) {
                System.out.println("滿足條件的出租車編號:" + info.getcarID());
            }
        }
    }

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

這裏就不放表格了，因為測試的同學（雖然不知道是哪位仁兄）沒有對我特別嚴格，而且實名承認自己是先寫的代碼後補的JSF，被報的JSFBUG和功能BUG沒有對應關系，但不代表JSF的書寫沒有問題。

下面分析一下功能BUG中的問題，都截取自沒有測試沒有debug的第九次作業，共3個。

1、等待狀態出租車走了回頭路：

沒有使用真正的隨機，而是使用的循環break；使得每次選路都有一定規律，而且使用500ms清空一次流量的辦法，數據訪問一定的卡頓滯後。

2、等待服務狀態20s未停止1s：

在輸出和判斷邏輯裏使用了假時間，但初始為等待狀態的出租車在假時間增加上有漏洞，不能按時增加到20s

3、測試接口沒有正確實現：

這個Bug....實在是太低級了emmm 因為沒有進行任何測試所以也沒看出來。原因是邏輯表達式(!((status==0)||(status==1)||(status==2)||(status==3))) 寫成了&&

所以，無論多忙，還是要好好測試，好好測試，好好測試！不然八成會涼。

歸納自己在設計規格和撰寫規格的基本思路和體會

因為都是寫好了代碼才補的規格，所以談不上什麽太有價值的體會，只好把自己撰寫jsf的主要方法簡要談一談。

REQUIRES：我一般是光標點到變量上面，利用eclipse自帶的陰影檢查這個變量是方法內部聲明的還是外部可見的。

MODIFIES：特別註意對非內部聲明變量的賦值和return。

EFFECTS：一般就講述什麽條件下會得到什麽樣的返回結果。不要提及算法本身的過程。以及特別註意寫明對非法輸入參數的處理結果。

THREAD_RQUIRES\THREAD_EFFECTS：查看方法是否帶鎖。

總結

總之，OO課程雖然接近尾聲了，一路遇到了很多很多友好的測試者感覺很幸運很感恩，但並不能因此掩蓋自己的問題，我自己心裏很明白作為一個預備程序猿和優秀的同學差距還是非常非常大，要學的東西還是太多，以後無論是自學還是正常學習課程都要多向身邊比自己強的人謙虛請教，進步，永不止步。

OO課程第三次總結QWQ