渡過OO的死劫,瞭解規格的意義——OO第三次博客總結

當熬過了一次次黑暗,迎接咱們的倒是被扣的慘不忍睹的JSF算法

┭┮﹏┭┮數據結構


 

1、總結調研less

規格的歷史分佈式

  傳統科學的特色是發現世界,而軟件的特色是構造世界。軟件的最底層就是0,1,兩個離散的值。程序設計語言的三次分離使軟件技術產生了飛躍。oop

  程序設計的演變大體能夠分紅如下三個過程:測試

  1. 20世紀60年代之前,計算機剛剛投入實際使用,軟件設計每每只是爲了一個特定的應用而在指定的計算機上設計和編制,採用密切依賴於計算機的機器代碼或彙編語言,軟件的規模比較小,不多使用系統化的開發方式,此時的代碼更多的是私人性質的,知足我的要求的程序ui

  2. 60年代中期,大容量、高速度的計算機出現,隨之出現的是代碼量急劇提高,複雜度急劇增加、程序可靠性問題突出的問題。結果化程序設計隨之提出,它要求程序設計時以模塊爲單位,每一個模塊專職本身的工做,而要在模塊間交流,在開發者和用戶,開發者和開發者之間交流,就只須要相應接口便可;this

  3. 80年代,面向對象的設計開始在業界大行其道,相比於單純的結構化設計,面向對象的設計從審視問題的角度上就有了差別,程序發生了從圍繞「行爲」執行到圍繞「客體」執行的變化,隨之而來的,就是封裝性地提升,可重用性的提升,能夠說,面向對象進一步實現告終構化設計,是結構化設計更進一步的實現。說明是類型定義和操做描述,體是操做的具體實現。(具體的例子就是C++,Java等面嚮對象語言的類說明與類實現的分離。)解決方案設計只關注說明,實現時引用或者設計體。體的更改、置換不影響規格說明,保證了可移植性。支持多機系統,但要一樣環境。此時產生了劃時代的面向對象技術。在結構化越加明確的同時,開發者與設計者,開發者與用戶,開發者與開發者之間的交流,就須要「抽象」來實現,由於彼此間不須要關心對方的實現方法,而只須要知道這個模塊的接口有什麼要求,會改什麼,能作什麼就行。經過規格化抽象,咱們就能將這種交流變得高效,同時也下降了維護和修改的難度。spa

  4.基於構件開發:標準化的軟件構件如同硬件IC,可插拔,使用者只用外特性,不計內部實現。Web Services:軟件就是服務。分佈式,跨平臺,鬆耦合。設計

爲何規格很重要?

  這三次分離中的第二次就是OO課程要求咱們去作的,也是面向對象的精髓。在大型項目的開發中,單個項目不可能由一我的完成。多人協做共同完成任務就意味着不只僅須要知道本身的代碼作了什麼,還要知作別人的代碼作了什麼。本身的代碼是本身寫出來的,具體怎麼實現,使用了什麼樣的數據結構,使用了什麼樣的算法,固然知道本身的程序會對什麼產生影響,須要什麼樣的輸入 。假設有我的寫了一個方法,寫好了,實現了,因而,他交了這份代碼上去,你要使用這個方法,一看,這什麼**玩意。花了時間適應了代碼風格,知道要幹嗎以後,寫本身的代碼進行測試,一測,bug,找了半天,發現是他和你的代碼對於某個變量能不能修改有衝突。浪費了很長時間,再交給上面。。惡行循環。因而,規格的誕生能夠說是拯救了這個局面。拿到代碼,看前置條件,反作用,後置條件,就很清晰,永無bug(固然是不可能的)。

  軟件工程行業代碼也愈來愈複雜,多人協做是必不可少,規格在我看來是代碼風格的調和劑,多人項目運做的潤滑油。


 

2、規格bug及分析

第九次做業

Effects不完整 92行:@EFFECTS: true ==> (parse the input); 
Effects內容爲實現算法 34行:@EFFECTS: true ==> (read the map);

>此次做業兩個bug的產生一是由於方法寫的太過冗雜,致使Effects描述功能並不能描述的非常詳盡,二是一些比較奇怪的方法因爲我的能力有限只能用天然語言去儘可能的描述,好比上面的對於讀取地圖的方法。

第十次做業

Effects不完整 77行:@THREAD_EFFECTS: this.MS;
Modified不完整 59行:@MODIFIES: System.out,this.output,this.rl;缺乏

>此次的bug和上次基本同樣吧。也就是方法沒有設計得很好。從第九次做業開始,不少的方法都是沿用的以前的做業,而以前已經寫好的方法從新加上規格會致使有一些本末倒置的意味,而且課下發放的JSF並不能徹底解決咱們對於規格的理解,因此在編寫程序規格時不免出現一些問題,歸結緣由仍是不熟練以及缺少相似的思想。至於新增的方法沒有寫JSF仍是由於本身先寫了方法自己,而非老師說的先寫規格再寫代碼。總之規格寫的很迷就是了。

第十一次做業

無JSF bug

 


 

 

3、很差的規格寫法及改進

前置1:賦值「=」應該改成「==」

    /**
        *@REQUIRES: s!=null,s=TAKING||s=WAITING||s=SERVING||s=STOP;
        *@MODIFIES: this.status;
        *@EFFECTS: 
        *        status==s;
        */    
    public void SetStatus(TaxiStatus s){
        this.status=s;
    }
    //正確寫法
    /**
        *@REQUIRES: s!=null,s==TAKING||s==WAITING||s==SERVING||s==STOP;
        *@MODIFIES: this.status;
        *@EFFECTS: 
        *        status==s;
        */    
    public void SetStatus(TaxiStatus s){
        this.status=s;
    }

前置2:前置條件必須爲布爾表達式

 

/**
     * @REQUIRES: index is in 0-100;
     * @MODIFIES:this.index; 
     * @EFFECTS: this.index == index;
     */
    public TaxiCar(int index) {     
        this.index = index;
    }
//正確寫法
/**
     * @REQUIRES: 0<=index<100;
     * @MODIFIES:this.index; 
     * @EFFECTS: this.index == index;
     */
    public TaxiCar(int index) { 
        this.index = index;
    }

 

前置3:直接寫null不判斷對象存在與否

 

  /**
       * @REQUIRES: None;
       * @MODIFIES: this.req; this.position;
       * @EFFECTS: this.req == req; this.position == position;
       */
      public Record(Request req, Point p) {
          this.req = req;
          this.position = p;
      }
 //正確寫法
 /**
      * @REQUIRES: req != null && p != null;
      * @MODIFIES: this.req; this.position;
      * @EFFECTS: this.req == req; this.position == position;
      */
     public Record(Request req, Point p) {
         this.req = req;
         this.position = p;
     }

 

前置4:對於數字類型範圍判斷遺漏或錯誤

/**
    *@REQUIRES:id!=null;
    *@EFFECTS: 
    *        \result==squad[id];
*/    
    public Taxi get(int id){
        return this.squad[id];
    }
//正確寫法
/**
    *@REQUIRES:id!=null,0<=id<=99;
    *@EFFECTS: 
    *        \result==squad[id];
    */    
    public Taxi get(int id){
        return this.squad[id];
    }

前置5:因爲粗心缺乏括號引發的邏輯錯誤

/**
     * @REQUIRES: req != null && index >= 80 || index < 0;
     * @MODIFIES: this.req; this.index;
     * @EFFECTS: this.req == req; this.index; 
     */
    public Record(Request req, int index) {
        this.req = req;
        this.index = index;
    }
//正確寫法
/**
     * @REQUIRES: req != null && (index >= 80 || index < 0);
     * @MODIFIES: this.req; this.index;
     * @EFFECTS: this.req == req; this.index; 
     */
    public Record(Request req, int index) {
        this.req = req;
        this.index = index;
    }

後置1:儘可能不要使用天然語言(與前置不一樣,不是必須的)

 

/**
     * @REQUIRES: req != null;
     * @MODIFIES: None;
     * @EFFECTS: 判斷起始點與目標點是否爲同一個點
     */
    public boolean samedest(Request req) {
        if(req.getSrc().equals(req.getDst())) {
            return true;
        }
        else 
            return false;
    }
//正確寫法
/**
     * @REQUIRES: req != null;
     * @MODIFIES: None;
     * @EFFECTS: (req.getSrc() == req.getDst()) ==> \result == true;
     *           (req.getSrc() != req.getDst()) ==> \result == false;
     */
    public boolean samedest(Request req) {
        if(req.getSrc().equals(req.getDst())) {
            return true;
        }
        else 
            return false;
    }

 

後置2:缺乏程的規格

        /**
        *@MODIFIES: System.out;
        *@EFFECTS: 
        *        true==>(do the things below in an endless loop)==>(wait())==>(dispatch());
        */    
    public void run(){
        while(true){
            try {
                synchronized(this.MS){
                    this.MS.wait();
                    this.dispatch();
                }
                //System.out.println(System.currentTimeMillis());
            } catch (Throwable e) {
                System.out.println("Error in Scheduler");
                System.exit(0);
            }
        }
    }
    //正確寫法
        /**
        *@MODIFIES: System.out;
        *@EFFECTS: 
        *        true==>(do the things below in an endless loop)==>(wait())==>(dispatch());
        *@THREAD_EFFECTS: this.MS;
        */    
    public void run(){
        while(true){
            try {
                synchronized(this.MS){
                    this.MS.wait();
                    this.dispatch();
                }
                //System.out.println(System.currentTimeMillis());
            } catch (Throwable e) {
                System.out.println("Error in Scheduler");
                System.exit(0);
            }
        }
    }

後置3:未處理異常(沒有說明)

public static int min (int[ ] a) throws NullPointerException, EmptyException 
/**@ 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);
*/

後置4:方法行數太多致使描述遺漏或沒法描述

    /**
    *@MODIFIES: this.light,this.lightmap;
    *@EFFECTS: 
    *        Change the lights
    */
    public void Change(){
        for(int i=0;i<80;i++){
            for(int j=0;j<80;j++){
                if(Main.light[i][j]==1){
                    Main.light[i][j]=2;
                    guigv.lightmap[i][j]=1;
                    Main.TG.SetLightStatus(new Point(i,j),1);
                }
                else if(Main.light[i][j]==2){
                    Main.light[i][j]=1;
                    guigv.lightmap[i][j]=2;
                    Main.TG.SetLightStatus(new Point(i,j),2);
                }
            }
        }
    }
    //正確寫法
    /**
    *@MODIFIES: this.light,this.lightmap;
    *@EFFECTS: 
    *        (\all int i,j,k;0<=i,j<80,light[i][j]>0)==>
    *        ((light[i][j]==1)==>(light[i][j]==2&&lightmap[i][j]==1)&&(light[i][j]==2)==>(light[i][j]==1&&lightmap[i][j]==2));
    */
    public void Change(){
        for(int i=0;i<80;i++){
            for(int j=0;j<80;j++){
                if(Main.light[i][j]==1){
                    Main.light[i][j]=2;
                    guigv.lightmap[i][j]=1;
                    Main.TG.SetLightStatus(new Point(i,j),1);
                }
                else if(Main.light[i][j]==2){
                    Main.light[i][j]=1;
                    guigv.lightmap[i][j]=2;
                    Main.TG.SetLightStatus(new Point(i,j),2);
                }
            }
        }
    }

後置5:描述邏輯不正確或不許確

/**
     * @REQUIRES : None; 
     * @MODIFIES : this.AskList;
     * @EFFECTS : AskList.contains(ask);
     */
    public synchronized void addAsk(Ask ask){
        AskList.add(ask);
    }
//正確寫法
/**
     * @REQUIRES : None; 
     * @MODIFIES : this.AskList;
     * @EFFECTS : AskList.contains(ask) && AskList.size == \old(AskList).size + 1;
     */
    public synchronized void addAsk(Ask ask){
        AskList.add(ask);
    }

 

4、功能bug與規格bug的聚焦關係

做業次數 功能bug數 規格bug數 聚焦關係
第九次 2 2 無明顯關係
第十次 7 2 無明顯關係
第十一次 2 0 無明顯關係

其實從bug數上根本看不出來在功能上和規格上的bug之間有什麼明顯的關係。但我確實比較傾向於一個好的規格,必然是一個代碼行數比較少,並且功能單一且明確的方法所具有的。而這樣的代碼寫出來在功能上的bug也十分容易被發現並改正。從整個程序的設計來考慮,當一個方法的規格複雜時,必然須要更多的篇幅和代碼來進行實現,出現bug的概率也會越大。因此咱們之後寫代碼必定要以規格來寫代碼。

 


 

 

5、心得體會

  其實說關於設計規格和撰寫規格的思路與體會也並無什麼特別的,由於咱們在訓練撰寫規格是在之前寫的方法的基礎上去完善的。可是因爲之前寫的方法功能比較雜糅,並且個別方法特別長,因此並非很好地去撰寫一個比較標準的規格。咱們也沒有進行一個先寫規格再根據規格寫代碼的訓練,對於這方面我也沒有經驗。可是我仍是覺的這方面的訓練是十分有必要的。由於一個好的代碼必定是可移植好維護的,而設計一個好的規格是寫一個好的代碼的基礎。

  最後但願你們都能善良一點,開心一點,共同迎接OO勝利的曙光咯~

相關文章
相關標籤/搜索