oo面向對象--規格化設計

oo面向對象--規格化設計

規格化設計與抽象

要了解規格化設計首先要了解抽象化的程序設計，二者是密不可分的。

抽象化（Abstraction）

抽象化是將數據與程序，用語義呈現他們的外觀，可是隱藏起它的實現細節。

抽象的過程能夠看作多對一的映射，讓咱們忽略個體信息，將不一樣事物當作相同的事物對待，可以減小程序的複雜度，使得程序員能夠專一在處理少數重要的部分。

發展

近幾年來，程序員對已經產生的抽象水平產生不滿，甚至不知足於在高級語言程序中廣泛實現的抽象水平，解決這個問題的方法在於創造「更高級的語言」，用相對固定的數據結構以及有很強功能的原始類型來實現，可是這種方法的缺陷在於嘉定編程語言的設計者在設計語言的時候將大多數用戶須要的抽象設計引進設計語言中，包含如此衆多的內置抽象的編程語言可能笨拙的很難使用。

另外一種可取代的方法是設計一種語言機制，容許程序員在須要的時候構建本身的抽象方法。一般的機制是使用過程（procedure）。編程語言包含了兩種重要的抽象方法：參數化抽象（abstraction by parameterization）和規格化抽象（abstraction by specification）。其中：

• 參數化抽象是用參數替換數據特徵來進行抽象。這樣可以概括出模塊，從而使其能夠用於更多的狀況。例如，能夠定義一個排序抽象，既可以實現對實數數組的排序，又可以實現對整型數組的排序，或者甚至對數組類型這類通常結構都有用。
• 規格化抽象是將運行細節（即模塊如何實現）抽象爲用戶所需求的行爲（即模塊作什麼）。這是從具體實現中抽象出模塊，須要的僅僅是模塊的實現可以匹配咱們所依賴的表述形式。

程序設計中，抽象類別包括下列4類：

1：過程抽象：可以引入一些新的操做；

2：數據抽象：可以引入新的數據對象類型；

3：反覆運算抽象：可以反覆運算遍歷在集合中的元素，而沒必要顯示如何得到元素的細節；

4：類型層次：可以從多個單獨的數據類型中抽象成幾組相關的類型。

規格

抽象用於將一個程序分解爲多個模塊，然而抽象是無形的，沒有描述，咱們就沒法知道如何將它與其實現的抽象區分。規格描述了服務的提供者和用戶之間的協定，提供者贊成編寫一個屬於規格知足集的模塊。

規格是對一個方法/類/程序的外部可感知行文的抽象表示，它的目的是爲了定義抽象的行爲。

若是一個實現提供了所描述的行爲，這個實現就知足了一個規格。

規格的含義是知足其全部程序的集合，這個集合稱爲規格知足集。

做業中的規格bug

此處爲本身統計的bug，因爲報告的jsf個數有限，本身從新看了一次仍是發現了許多bug和不規範的地方。

bug類別	Requires不完整	Modifies不完整	Effects不完整	Requires邏輯錯誤	Modifies邏輯錯誤	Effects邏輯錯誤	Effects內容爲實現算法	不符合JSF
個數	7	3	5	0	0	2	0	0
方法行數	3,5,5,13,22,20,4	5,7,7	20,30,15,17,15			30,15

BUG產生緣由

一、有些方法或者類的JSF遺漏

好比本身寫的Exception類裏面忘記寫JSF，一些信息存儲的類裏面的構造方法有時候也會忘記寫，仍是本身不夠細心。

二、沒有按照標準格式書寫

Effects以後的內容應該爲布爾表達式。像是代碼中出現的(\result = str)，這種裏面的=應該寫成==

三、程序裏面一些傳入對象的方法，對應的Requires有的沒寫。

有傳入仍是應該寫明有Requires的要求，好比傳入對象不等於null，或者對象的repOK 爲ture之類。

四、某些過程會有附加的隱式輸入，例如讀入文件和在System.out寫信息，這些也屬於過程的輸入

五、仍是偷了不少懶。。

JSF不規範的寫法及改進

有些例子前置條件和後置條件一塊兒修改了。

一、前置與後置條件：

public int getDirection(Coordinate now, Coordinate next){
            /**
     * @REQUIRES: None;
     * @MODIFIES: None;
     * @EFFECTS: (next.getX()-now.getX()==1&&next.getY()-now.getY()==0)==>(\result = 0);
    (next.getX()-now.getX() == -1 && next.getY()-now.getY()==0)==>(\result = 1);
    (next.getX()-now.getX() == 0 && next.getY()-now.getY()==1)==>(\result = 2);
    (next.getX()-now.getX()== 0 &&next.getY()-now.getY() == -1)==>(\result = 3);
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS:
     */
    }

這裏輸入的兩個座標分別是當前座標和下一步的座標，這兩個座標須要知足的條件是在地圖上是相鄰的，因爲可能出現道路忽然斷開的情況，因此兩個座標的鏈接狀態未知，當時想着在代碼裏面處理了這種異常情況因此沒有寫requires，可是其實也能在requires中體現，而後在代碼中處理這種狀況，拋出異常或者返回等操做，若是不寫的話也要加入兩個座標不爲空，有輸入最好要限制其內容，什麼都不寫不是一種好的習慣。
這裏的effects書寫也不規範，要用雙等號。

修改版本：

public int getDirection(Coordinate now, Coordinate next){
/**
 * @REQUIRES: now.getX()>=0 && now.getX() < 80 
 * && now.getY() >= 0 && now.getY() < 80 && next.getX()>=0 
 * && next.getX() < 80  && next.getY() >= 0 && next.getY() < 80 
 * && graph[now.getX()*80+now.getY()][next.getX()*80+next.getY()] == 1;
 * @MODIFIES: None;
 * @EFFECTS: 
 * (next.getX()-now.getX()==1&&next.getY()-now.getY()==0)==>(\result = 0);
 * (next.getX()-now.getX() == -1 && next.getY()-now.getY()==0)==>(\result == 1);
 * (next.getX()-now.getX() == 0 && next.getY()-now.getY()==1)==>(\result == 2);
 * (next.getX()-now.getX() == 0 &&next.getY()-now.getY() == -1)==>(\result == 3);
 */
}

二、後置條件：

public void servingHandler() throws InterruptedException{
     /**管理出租車服務狀態
     * @REQUIRES: None;
     * @MODIFIES: this.newtime;this.state;this.coordinate;this.schedulerInfo;
     *      * this.info;
     * @EFFECTS: 對本線程的狀態和參數進行改變
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS: \locked(trackingInfo);
     */

    }

這個方法實現的過程有些複雜，當時直接用天然語言瞎寫了一下，沒有規範化表述。不過在此函數中調用了其餘函數，如今不知道如何將調用其餘函數的effects寫清楚。。

public void servingHandler() throws InterruptedException{
     /**
     * @REQUIRES: None;
     * @MODIFIES:\this.newtime;\this.state;
     * \this.coordinate;\this.schedulerInfo;\this.info;\System.out;
     * InfoQueue；
     * @EFFECTS:
     * desMove(currentRequest.getDestination());
     * this.credit.addAndGet(3);
     * InfoQueue.contains(schedulerInfo);
     * schedulerInfo.contains(info);
     * System.out!=null;
     * @THREAD_REQUIRES:None;
     * @THREAD_EFFECTS: \locked(trackingInfo);
     */

    }

三、前置條件和後置條件：

@Override
    public void desMove(Coordinate destination) throws InterruptedException {
         /**出租車找最短路徑行駛,找最小流量的邊
     * @REQUIRES:  (\all Coordinate a,b;map;graph[a][b] == 1)
     * @MODIFIES: this.coordinate;this.Info;newtime;
     * @EFFECTS: this.coordinate == destination;
     * @THREAD_REQUIRES:
     * @THREAD_EFFECTS:
     */
    }

這個函數是移動出租車到目標點，requires沒有限制destination的範圍，後置條件寫的過於簡略，沒有將移動過程寫清楚。

@Override
    public void desMove(Coordinate destination) throws InterruptedException {
   /**出租車找最短路徑行駛,找最小流量的邊
     * @REQUIRES: now.getX()>=0 && now.getX() < 80 && now.getY() >= 0 
     * && now.getY() < 80 
     * &&(\all Coordinate a,b;a.getX()>=0 && a.getX() < 80 && a.getY() >= 0 && a.getY() < 80 && b.getX()>=0 && b.getX() < 80 && b.getY() >= 0 && b.getY() < 80;graph[a.getX()*80+a.getY()][b.getX()*80+b.getY()] == 1)
     * //保證地圖連通
     * @MODIFIES: this.coordinate;this.Info;newtime;
     * @EFFECTS:pathway == TaxiGUI.getInstance().getShortestPath(destination))==>(\all Coordinate a;pathway;this.info.contains(a))
     * && (\all int i,int j;j < pathway.size()&&i == j * 5;info.contains(i))
     * && \this.coordinate == pathway.get(pathway.size()-1)
     * && \this.newtime == newtime + waitime + 5*pathway.size()&&info.contains(newtime);
     */
    }

四、前置條件和後置條件：

public static boolean judegeValid(Coordinate a, Coordinate b){
    /**
     * @REQUIRES: None;
     * @MODIFIES: None;
     * @EFFECTS: 判斷是否符合座標輸入條件
     */
     
     }

因爲有輸入參數，應該對參數範圍加以規範和約束。
effects書寫也不符合規範。

public static boolean judegeValid(Coordinate a, Coordinate b){
    /**
     * @REQUIRES: a instanceof Coordinate && b instanceof Coordinate && a! = null && b!=null;
     * @MODIFIES: None;
     * @EFFECTS:(a.isOutOfBound()||b.isOutOfBound()||a.equals(b))==> \result == false;
     *!(a.isOutOfBound()||b.isOutOfBound()||a.equals(b))==> \result == true;
     */
     
     }

五、前置條件和後置條件：

public void RoadStatusHandler(String cmd){
   /**
     * @REQUIRES:
     * @MODIFIES: TaxiGUI;
     * @EFFECTS: 改變道路開關；
     */
     }

String cmd不能是null，雖然也在代碼中有處理，effects沒寫清楚。。

public void RoadStatusHandler(String cmd){
   /**
     * @REQUIRES: str instanceof String;str!=null;
     * @MODIFIES: TaxiGUI;System.out;
     * @EFFECTS: !cmd.isValid()==>System.out == "#set Status Format Error";
     * cmd.matches(this.m)&&cmd.isValid()&&m.group(5).equals("OPEN")==>TaxiGUI.getInstance().graph[m.group(1)*80+m.group(2)][m.group(3)*80+m.group(4)]==1;
     * cmd.matches(this.m)&&cmd.isValid()&&m.group(5).equals("CLOSE")==>TaxiGUI.getInstance().graph[m.group(1)*80+m.group(2)][m.group(3)*80+m.group(4)]==0;
     */
     }

六、前置條件和後置條件

public void RequestHandler(String cmd) throws RequestFormatErrorException,InterruptedException{
          /**
     * @REQUIRES:
     * @MODIFIES: rcv;
     * @EFFECTS: 請求讀入
     */
    }

沒有寫異常狀況，requires不完整，effects不完整

public void RequestHandler(String cmd) throws RequestFormatErrorException,InterruptedException{
 /**
     * @REQUIRES:cmd instanceof String && cmd! = null;
     * @MODIFIES: rcv;System.out;
     * @EFFECTS: cmd.isValid()==>\this.rcv.contains(new PassengerRequest request);
     * !cmd.isValid()==>e == exceptional_behavior(RequestFromatErrorException)&&System.out == e.getMessage();
     
     */
    }

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

方法名	功能bug數目	規格bug數目
public void input()	2	1
public void SetRoadStatus(Coordinate a1,Coordiante a2)	1	0
public void randomMove()	1	1

個人功能bug主要在代碼實現上面有問題，其實和規格的bug聯繫並無很大。

規格設計思路及體會

老師在課上強調，要先寫出規格再開始寫代碼。也就是要先抽象出這個類或者方法的功能，輸入輸出再進行代碼的書寫，寫出來的內容要符合規格的敘述。因此構思抽象規格是放在首位的，關注的是行爲，而不是實現行爲的細節。

一個規格的語義包含三部分：需求（Requires），修改（Modifies），結果（Effects）。

一、requires：規格須要有足夠的限制性來排除其抽象的用戶不可接受的任何實現，這就須要在requires裏面明確指出來。一個局部的過程規格老是包含了一個requires格式，有些時候編程應該檢查requires中的約束條件，若是不知足就跑出一個異常。

二、modifies：列出了被修改的全部輸入名稱，作到不遺漏。

三、effects：全部爲被requires格式排除的輸入描述了過程的行爲，必須定義產生了何種輸出，同時必須定義被列在modifies格式中的輸入作的修改所產生的結果。在本課程中須要用到規範化的表達，實際工程上也有用到簡潔的天然語言表達，可是必定要表述清楚，而且符合邏輯。

四、線程類的requires和effects須要書寫，但通常不要給使用者限制requires.

實際上因儘量避免使用requires格式，由於若是輸入產生了不知足requires的格式的時候，規格並無給出相應的操做。因此設計抽象的時候要設計成知足最小限度的受限，對過程行爲的細節僅僅作必要的限制，給實現者更多的自由，能夠進行更加有效的編程。