OO第三階段總結

軟件形式化方法歷史

• 形式化方法的研究高潮始於20世紀60年代後期，針對當時所謂「軟件危機」,人們提出種種解決方法,概括起來有兩類：一是採用工程方法來組織、管理軟件的開發過程；二是深刻探討程 序和程序開發過程的規律，創建嚴密的理論，以其用來指導軟件開發實踐。前者致使「軟件工程」的出現和發展，後者則推進了形式化方法的深刻研究。通過30多 年的研究和應用，現在人們在形式化方法這一領域取得了大量、重要的成果，從早期最簡單的形式化方法一階謂詞演算方法到如今的應用於不一樣領域、不一樣階段的基於邏輯、狀態機、網絡、進程代數、代數等衆多形式化方法。形式化方法的發展趨勢逐漸融入軟件開發過程的各個階段,從需求分析、功能描述(規約)、(體系結構/算法)設計、編程、測試直至維護。

  規格BUG分析

  做業次數	規格bug	名稱	雷同bug數量
  9	4	Modifies不完整/Effects邏輯錯誤/不符合JSF規範/Requires邏輯錯誤	0
  10	1	repOK邏輯錯誤	0
  11	0	\	0

  規格BUG產生緣由

• 規格bug各自都有各自的見解，對於規格本身反正也不太理解，因此出現錯誤也不知道是真的有問題仍是這樣也行，水平不夠，繼續提升

  很差寫法及其改進

public LinkedList<Integer> getDis(int startNode , int endNode){
        /**
         * @REQUIRES:(\all int startNode; 0<=startNode<=6399);(\all int endNode; 0<=endNode<=6399);
         * @MODIFIES:None;
         * @EFFECTS:\result == map.Bfs(arrays,endNode);
         *
         */
    引用了中間變量
     public LinkedList<Integer> getDis(int startNode , int endNode){
        /**
         * @REQUIRES:(\all int startNode; 0<=startNode<=6399);(\all int endNode; 0<=endNode<=6399);
         * @MODIFIES:None;
         * @EFFECTS:return the shortest distance nodes between startNode and endNode;
         *
         */

public synchronized void Set(int startnode, int endnode , int value){ 
    /**
     * @REQUIRES:(\all int startnode; 0 <= startnode <= 6399);(\all int endnode; 0 <= endnode <= 6399);(\all int value; 0 <= value <= 6399);
     * @MODIFIES:None;
     * @THREAD_EFFECTS:lock(this);
     * @EFFECTS:set flow of the road between startnode and endnode to value;
     *
     */
    int roads = startnode*6400 + endnode;
    int roads_copy = endnode*6400 + startnode;
    roadMap.put(roads,value);
    roadMap.put(roads_copy,value);
  }
  Modifies不完整
    public synchronized void Set(int startnode, int endnode , int value){
    /**
        * @REQUIRES:(\all int startnode; 0 <= startnode <= 6399);(\all int endnode; 0 <= endnode <= 6399);(\all int value; 0 <= value <= 100);
        * @MODIFIES:roadMap;
        * @THREAD_EFFECTS:\lock(this);
        * @EFFECTS:set flow of the road between startnode and endnode to value;
        *
        */
    int roads = startnode*6400 + endnode;
    int roads_copy = endnode*6400 + startnode;
    long times = System.currentTimeMillis();
    for(int i = 0 ; i < value ; i++){
        roadMap.get(roads).add(times);
        roadMap.get(roads_copy).add(times);
    }
}

public void set(int state , int credit , int PosNode){
    /**
     * @REQUIRES:(\all int state; 0<=state<=4);(\all int PosNode; 0<=PosNode<=6399);
     * @MODIFIES:this.credit;this.posNode;this.state;
     * @EFFECTS:this.credit==credit;this.posNode==PosNode;this.state==state+1;
     *
     */
    this.credit = credit;
    this.posNode = PosNode;
    this.state = state + 1;
 }
  邏輯錯誤
    public void set(int state , int credit , int PosNode){
    /**
        * @REQUIRES:(\all int state; 0<=state<4);(\all int PosNode; 0<=PosNode<=6399);
        * @MODIFIES:this.credit;this.posNode;this.state;
        * @EFFECTS:this.credit==credit;this.posNode==PosNode;this.state==state+1;
        *
        */
    this.credit = credit;
    this.posNode = PosNode;
    this.state = state + 1;
}

功能bug與規格bug在方法上的彙集關係

• 我的感受功能bug與規格bug可能並無太大關係，測試者找bug之時，規格bug大部分不是由於功能bug致使的，而是後寫規格容易遺漏規格的要點等內容，或者是寫好規格以後修改了相應代碼，總之感受寫規格更多考慮是怎麼纔不會被扣，感受違背了教學初衷

  基本思路與體會

• 基本都是先寫好所有方法而後再動手開始寫規格,寫以前本身也確實是按照必定思路進行寫代碼的,可是沒有按照規格的方式寫下來。水平不夠，仍需繼續努力