OO第三次階段性總結

時間 2019-12-07

標籤第三次階段性總結简体版

原文原文鏈接

1、規格化設計的歷史以及人們重視的緣由

發展歷史

從20世紀60年代開始，就存在着許多不一樣的形式規格說明語言和軟件開發方法。在形式規格說明領域一些最主要的發展過程列舉以下：java

1969－1972 C.A.R Hoare撰寫了"計算機編程的公理基礎（An Axiomatic Basis for Computer Programming）"和"數據表示的正確性證實"兩篇開創性的論文，並提出了規格說明的概念。git

1974－1975 B.Liskow/S.N. Zilles和J. Guttag引入了"抽象數據類型"的概念。算法

1976 E.W. Dijkstra定義了"最弱前置條件"的概念編程

1977 R.Burstall和J.Goguen提出了第一個代數規格說明語言：Clearapp

1988 Standford的SRI開發了代數規格說明語言OBJ3ide

1980-1986 C.Jones定義了VDM語言，也就是維也納開發方法。測試

1985－1992 牛津大學的程序研究小組開發了Z規格說明語言。與此同時BP研究室開發了稱之爲B方法的面向模型的規格說明語言。this

1985－1993 在MIT和Digital SRC開發了代數規格說明語言Larchspa

從1991年開始，面向對象的形式規格說明語言開始發展，例如，Object-Z, VDM++, CafeOBJ等語言。設計

1996－2000年在歐洲CoFI（Common Framework Initiative）項目資助下開發"統一"代數規格說明語言CASL(Common Algebraic Specification Language)

重視緣由

我認爲規格首先給了你們編程時一個統一的認識，明確了程序運行的前提和程序運行後的效果，這一點在我的編程中有助於理清思路，而在集體的工程開發過程當中也有助於協做，使你們開發的方向一致。

另外一方面我認爲正確的規格能夠方便編程者進行調試，經過斷言判斷前置條件是否知足以及檢驗後置條件是否在程序運行後知足。

2、規格Bug數量及緣由分析

做業	Bug類型及細節	所在文件及行數
第九次	無	無
第十次	Effects內容爲實現算法：\result寫成了\return	不少文件中
第十一次	Effects不完整：在有try-catch的方法中忘記寫exceptional_behavior	InputHandler.java/192

規格bug緣由分析：第九次沒有被報規格bug，大概是測試者不太關心。第十次和第十一次做業中都是有所疏忽致使。其中第十次做業是一個筆誤，幾乎全部文件都寫成了\return==balabala，第十一次做業中有一個方法因爲後來有改動，沒有添加exceptional_behavior。

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

前置條件

1. 天然語言描述

1     /**
2      * @REQUIRES: k存在
3      * @MODIFIES: v
4      * @EFFECTS: v == \old(v) + 1;
5      */

很差

1     /**
2      * @REQUIRES: k != null
3      * @MODIFIES: v
4      * @EFFECTS: v == \old(v) + 1;
5      */

好

2. 不是布爾表達式

    /**
     *
     * @REQUIRES:
     *      this.taxiStatus = IDLE;
     * @MODIFIES:
     *      this.credit;
     * @EFFECTS:
     *      this.credit = \old(this.credit) + 1;
     *      (\all PassengerRequest r in range, r.grabbedByTaxi(this))
     *
     */

很差

    /**
     *
     * @REQUIRES:
     *      this.taxiStatus == IDLE;
     * @MODIFIES:
     *      this.credit;
     * @EFFECTS:
     *      this.credit = \old(this.credit) + 1;
     *      (\all PassengerRequest r in range, r.grabbedByTaxi(this))
     *
     */

好

3. 沒有規定範圍

    /**
     *
     * @REQUIRES:
     *       locX, locY, dstX, dstY；
     * @MODIFIES:
     *     edge between (locX, locY),(dstX, dstY), ConsolePrinter;
     * @EFFECTS:
     *     edge.existence == op;
     *
     */

很差

    /**
     *
     * @REQUIRES:
     *     0 <= locX, locY, dstX, dstY <= 79;
     * @MODIFIES:
     *     edge between (locX, locY),(dstX, dstY), ConsolePrinter;
     * @EFFECTS:
     *     edge.existence == op;
     *
     */

好

4. 遺漏了某些條件，通常是傳入參數外的某些條件

    /**
     * @REQUIRES: mapVertex != null;
     * @MODIFIES: ConsolePrinter
     * @EFFECTS: \result == the opposite vertex of mapVertex
     */

很差

    /**
     * @REQUIRES: mapVertex != null && mapVertex.repOK == true;
     * @MODIFIES: ConsolePrinter
     * @EFFECTS: \result == the opposite vertex of mapVertex
     */

好

5. 對於一個容器中的全部對象，均須要規定前置條件

    /**
     *
     * @REQUIRES:
     *      this.edgeMap != null
     * @MODIFIES:
     *      None
     * @EFFECTS:
     *      (\exist MapEdge e, edgeMap.contains(e), \min(edgeMap.flowrates) == e.flowrate && \result == e);
     *
     * @THREAD_EFFECTS:
     *      (\ all MapEdge e in this.edgeMap);
     */

很差

    /**
     *
     * @REQUIRES:
     *      (\ all MapEdge e, this.edgeMap.contains ( e), e != null)
     * @MODIFIES:
     *      None
     * @EFFECTS:
     *      (\exist MapEdge e, edgeMap.contains(e), \min(edgeMap.flowrates) == e.flowrate && \result == e);
     *
     * @THREAD_EFFECTS:
     *      (\ all MapEdge e in this.edgeMap);
     */

好

後置條件

1. 不是布爾表達式

    /**
     *
     * @REQUIRES:
     *      this.requestQueue != null
     * @MODIFIES:
     *      None
     * @EFFECTS:
     *      return this.requestQueue;
     *
     */

很差

    /**
     *
     * @REQUIRES:
     *      this.requestQueue != null
     * @MODIFIES:
     *      None
     * @EFFECTS:
     *      \result == this.requestQueue;
     *
     */

好

2. 返回容器時不夠明確

    /**
     *
     * @REQUIRES:
     *      this != null
     * @MODIFIES:
     *      None
     * @EFFECTS:
     *      \result == (\all MapEdge e in this.edgeMap)
     *
     */

很差

    /**
     *
     * @REQUIRES:
     *      this != null
     * @MODIFIES:
     *      None
     * @EFFECTS:
     *      \result == new Arraylist<MapEdge> r;
     *      (\all MapEdge e, this.edgeMap.contains(e), r.contains(e))
     *
     */

好

3. 改變值書寫不規範

    /**
     *
     * @REQUIRES:
     *      this != null, num > 0;
     * @MODIFIES:
     *      this.credit;
     * @EFFECTS:
     *      this.credit +=  num;
     *
     */

很差

    /**
     *
     * @REQUIRES:
     *      this != null, num > 0;
     * @MODIFIES:
     *      this.credit;
     * @EFFECTS:
     *      this.credit == \old(this.credit) + num;
     *
     */

好

4. 沒有寫異常狀況

        /**
         * @REQUIRES:
         *         this.list != null;
         * @MODIFIES:
         *         None
         * @EFFECTS:
         *         this.hasNext() ==> (\result == this.list[\old(index)+1] && index == \old(index) + 1);
         *
         * @THREAD_EFFECTS:
         *      \locked(this.list);
         */

很差

        /**
         * @REQUIRES:
         *         this.list != null;
         * @MODIFIES:
         *         None
         * @EFFECTS:
         *         this.hasNext() ==> (\result == this.list[\old(index)+1] && index == \old(index) + 1);
         *         exceptional_behavior(NoSuchElementException)
         *
         * @THREAD_EFFECTS:
         *      \locked(this.list);
         */

好

5. 後置條件沒寫全

    /**
     * @REQUIRES: key != null;
     * passengerRequest != null;
     * @MODIFIES: this.unprocessedRequests, ConsolePrinter;
     * @EFFECTS: unprocessedRequests.contains(passengerRequest);
     * @THREAD_EFFECTS: \locked(this.appendlock);
     */

很差

    /**
     * @REQUIRES: key != null;
     * passengerRequest != null;
     * @MODIFIES: this.unprocessedRequests, ConsolePrinter;
     * @EFFECTS: unprocessedRequests.contains(passengerRequest); unprocessedRequests.size == \old(unprocessedRequest).size + 1
     * @THREAD_EFFECTS: \locked(this.appendlock);
     */

好