第三次OO總結

規格化設計的調研

---

隨着50年代高級語言的出現，編譯技術不斷完善，涌現出多種流派的語言，其中就有里程碑式的Pascal語言；進入70年代，因爲衆多語言形成的不可移植、難於維護，Ada程序設計語言誕生了，強調大型系統可讀性勝於可寫性，Ada程序自成清晰的文檔；通過80年代計算機硬件和操做系統的改善，程序設計重點從算法和數據結構實現技術向規模說明方向轉移。從空間的角度觀察, 廣義上來講, 軟件規格說明描述的是整個軟件系統；狹義來講, 軟件規格說明描述的是軟件系統的組成部件。從時間的角度來觀察, 廣義來講, 軟件規格說明方法適用於整個軟件生命週期； 狹義上來講, 軟件規格說明方法僅適用於軟件生命週期的特定階段。規格化設計能夠提升程序的可讀性，也能夠提升閱讀效率，便於之後的修改。

 

規格bug

---

 多是我運氣太好了，這幾回都沒被扣規格的bug……

 

改進寫法

---

 1. 前置條件

1.1 忽略前置條件

previous

　　public int[][] getMatrix(Point dst){
　　/**
　　     *@ REQUIRES: None
　　     *@ MODIFIES: visited, dist
　　     *@ EFFECTS: normal_behaver
　　　　       　　　 　\result == the shortest distance between point(x,y) from point(x2,y2) ;
　　*/
　　}

View Code

late

　　public int[][] getMatrix(Point dst){
　　/**
　　     *@ REQUIRES: !tmp.empty
　　     *@ MODIFIES: visited, dist
　　     *@ EFFECTS: normal_behaver
　　　　       　　　 　\result == the shortest distance between point(x,y) from point(x2,y2) ;
　　*/
　　}

View Code

 

1.2 前置條件不全

previous

　　private void chooseTaxi(){
　　/* *
    　　*@ REQUIRES: None
　　    *@ MODIFIES: \this.TarTaxi;
   　　 *@ EFFECTS: \any int i=0;i<this.list.size;i++:!list.get(i).getTaxiState().equals(TaxiState.STOP)==> \target = list.get(i);
　　*/

　　}

View Code

late

　　private void chooseTaxi(){
　　/* *
    　　*@ REQUIRES: \this.taxi!=null&&\this.taxi is sorted by credit;
    　　*@ MODIFIES: \this.TarTaxi;
    　　*@ EFFECTS: \any int i=0;i<this.list.size;i++:!list.get(i).getTaxiState().equals(TaxiState.STOP)==> \target = list.get(i);
　　*/

　　}

View Code

 

1.3 範圍錯誤

previous

public void taxiControl(int n) {
        /**
         *@REQUIRES: n>0 && n<100
         *@MODIFIES: None;
         *@EFFECTS: ......
         */
    }

View Code

late

public void taxiControl(int n) {
        /**
         *@REQUIRES: n>=0 && n<100
         *@MODIFIES: None;
         *@EFFECTS: ......
         */
    }

View Code

 

1.4 天然語言

previous

    private int loadMap(BufferedReader Reader) throws IOException{
        /* 
        @ REQUIRES: in this method we load the map
        @ MODIFIES: Map[][]
        @ EFFECTS:     \any char!=0&&char!=1 ==>System.out&&System.exit
                    \any somewhere not cross road but has light ==>System.out&&System.exit
        */
    }

View Code

late

    private int loadMap(BufferedReader Reader) throws IOException{
        /* 
        @ REQUIRES: File(path).exist
        @ MODIFIES: Map[][]
        @ EFFECTS:     \any char!=0&&char!=1 ==>System.out&&System.exit
                    \any somewhere not cross road but has light ==>System.out&&System.exit
        */
    }

View Code

 

1.5 格式錯誤

previous

public void run(Taxi t){
        /*
          @ REQUIRES: \t.status.equals(TaxiStatus.SERVING);
          @ MODIFIES: None 
          @ EFFECTS: ......
         */
    }

View Code

late

public void run(Taxi t){
        /**
         @ REQUIRES: t.status.equals(TaxiStatus.SERVING);
         @ MODIFIES: None
         @ EFFECTS: ......
         */
    }

View Code

 

2. 後置條件

2.1 天然語言

previous

    public synchronized void changeRoute() {
        /*
        @ REQUIRES: None
        @ MODIFIES: None
        @ EFFECTS: get the minimum flow and change the route
         */
    }

View Code

late

    public synchronized void changeRoute() {
        /*
        @ REQUIRES: None
        @ MODIFIES: None
        @ EFFECTS: \result = this.route = this.map.minRoute(this.position, point);
         */
    }

View Code

 

2.2 後置條件不全

previous

    private int getDir(Point from, Point to){
        /* 
        @ REQUIRES: None
        @ MODIFIES: None
        @ EFFECTS:     (to.getX() - from.getX() > 0) \return = 0;//D
                    (to.getX() - from.getX() < 0) \return = 1;//U
                    (to.getY() - from.getY() > 0) \return = 2;//R
                    (to.getY() - from.getY() < 0) \return = 3;//L
        */
    
    }

View Code

late

    private int getDir(Point from, Point to){
        /* 
        @ REQUIRES: None
        @ MODIFIES: None
        @ EFFECTS:     (to.getX() - from.getX() > 0) \return = 0;//D
                    (to.getX() - from.getX() < 0) \return = 1;//U
                    (to.getY() - from.getY() > 0) \return = 2;//R
                    (to.getY() - from.getY() < 0) \return = 3;//L
                    \return = 4;
        */
    
    }

View Code

 

2.3 沒有體現modified的改變

previous

    public void run() {
        /* 
        @ REQUIRES: None
        @ MODIFIES: system， r, position. credit, state, req, route, timer
        @ EFFECTS:     \this.state = 2&&\this.reqList.isEmpty==>\this.lastposition = \old.this.position;\this.position = getNextPos();t+=0.2+checkLight(lastposition, position, p);
                    \this.state = 2&&!\this.reqList.isEmpty==>\this.lastposition = \old.this.position;\this.position = getNextRoute();t+=0.2+checkLight(lastposition, position, p);
                    \this.state = 1||\this.state = 3==>this.lastposition = \old.this.position;\this.position = getNextRoute();t+=0.2+checkLight(lastposition, position, p);
                    \this.state = 0 ==> t+=0.2+checkLight(lastposition, position, p);
        */
    }

View Code

 

2.4 不符合格式規定

previous

    public boolean repOK() {
        /*
        @ REQUIRES: None
        @ MODIFIES: None
        @ EFFECTS:  (this.map==null||this.map.length==0) \result = false;
                    \result = true;
         */
    }

View Code

late

    public boolean repOK() {
        /*
        @ REQUIRES: None
        @ MODIFIES: None
        @ EFFECTS:  (this.map==null||this.map.length==0) ==> \result == false;
                    (this.map!=null&&this.map.length!=0) ==> \result == true;
         */
    }

View Code

 

2.5 忽略後置條件

 

心得體會

---

這個規格也不知道該說點什麼，都是寫完代碼看着複製粘貼，改改格式，而後基本也都是電工課解決的hhh可能以後3次要認真一點了

 

我一直很佛，對本身的程序和別人的程序都是隨便測幾個，雖然這不是對學術負責的態度？可是以爲吧幾天寫出來的東西怎麼也會有錯，至少我是這麼認爲本身的。自從ifttt自暴自棄，我就沒被報過bug（除了第一次出租車的loadfile有點問題，主要仍是自暴自棄吧）多是大難不死必有後福？不過OO卻是讓我知道了要更熱愛生活，否則除了黑黢黢的屏幕，什麼都不剩了。