OO博客做業3：第9-11周做業總結

1、總結介紹規格化設計的大體發展歷史和爲何獲得了人們的重視

一、規格化設計的大體發展歷史

規格化設計，又稱契約式設計，最先由Bertrand Meyer於1986年提出，出自於《面向對象軟件構造》。其基礎是形式驗證、形式規格和Hoare logic。

二、規格化設計獲得重視的緣由

在大型軟件工程開發中，協同工做能力的重要性日益凸顯。「對於一個大型系統來講，光保證它的各組成成分的質量是不夠的。而最有價值的是確保在任何兩個組成部分的交接處設計明晰的彼此義務和權利規範，即所謂契約。」（《面向對象軟件構造》）

Bertrand Meyer曾在訪談中提到：「對於軟件和軟件設計者來講，爲了保證各方面的正確性和健壯性，他們就必須懂得通信的準確約束規範。在這個地方，咱們就將商業中的契約概念應用到軟件中。……商業中，咱們會經過契約——對咱們指望的彼此義務和權利的準確表述——的方式彼此協調。對於軟件來講，咱們撰寫客戶和服務例程時，都必須嚴格遵循一樣的契約表述。」

《契約式設計的收益》一文中將規格化設計的優勢歸納爲如下5方面：得到更優秀的設計、獲得更出色的文檔、支持複用、提升可靠性、幫助調試。

2、表格分析規格bug

因爲沒有被發現規格bug，此環節略過。

3、分析本身規格bug的產生緣由

因爲沒有被發現規格bug，此環節略過。

4、分別列舉5個前置條件和5個後置條件的很差寫法，並給出改進寫法

一、前置條件的很差寫法

1-1：方法將形如」(x,y)」或」x,y」的字符串轉化成一個座標點對象，原寫法：

(\exist String in; in == str1 + "," + str2);

更好的寫法是：

in == String.format(「(%d,%d)」, x, y) || in == String.format(「%d,%d」, x, y) ;

0 <= x < 80; 0 <= y < 80;

明確指出格式具體是個什麼樣子。

1-2：普通出租車的構造方法。原寫法：

int i, SafeFile fp, TaxiGUI g;

更好的寫法：

\exist int i; 0 <= i < 100;

\exist SafeFile fp; fp != null;

\exist TaxiGUI g; g != null;

方法實際上沒有對輸入進行檢查，所以前置條件必須有更嚴格的約束。

1-3：普通出租車的run()方法。原寫法：

(\exist int status; 0<=status<=3);

更好的寫法：

none;

不變式的內容是默認成立的，不必寫在這裏。

1-4：這個方法寫出來徹底沒有意義：

       /**

        * @REQUIRES:(\exist int i; 0<=i<6400);

        * @MODIFIES:none;

        * @EFFECTS:(the point that i represents is in this city)==>(\result == true);

        * (the point that i represents is not in this city)==>(\result == true);

        */

       public boolean incity(int i) {

              int x = i / 80;

              int y = i % 80;

              return (x >= 0 && x < 80 && y >= 0 && y < 80);

       }

若是認真檢查，會發現前置條件知足時，即便什麼都不作，後置條件也知足。這部分代碼必定是神志不清時寫出來的。

 

二、後置條件的很差寫法

2-1：方法傳入一個點座標，判斷當前對象表明的座標是否位於傳入座標周圍的4*4區域內，便是否須要發送給該出租車。原寫法：

(\result == (src.within()))

更好的寫法：

\result == (src.x – 2 <= x <= src.x + 2 && src.y – 2 <= y <= src.y + 2)

這種簡單的布爾類型判斷方法在寫後置條件時不免照抄代碼原文。從工程角度，這樣的方法不寫規格也無大礙，可是做爲做業訓練，仍是要寫。

2-2：重寫了點座標類的toString方法。原寫法：

(\exist String re; re == "(x,y)"); (\result == re);

更好的寫法：

(\result == ret)==>(ret == 「(」 + x + 「,」 + y + 「)」);

對後置條件的理解出現誤差。

2-3：針對控制檯輸入的格式檢查。原寫法：

(\exists byte op);

        * (in.matches(req))==>(op == 1);

        * (in.matches(load))==>(op == 2);

        * (in.matches(road))==>(op == 3);

        * (in == end)==>(op == 4);

        * else (op == -1);

        * (\result == op);

更好的寫法：

(\result == 0)==>(in == 「END」);

(\result == 1)==>(in.matches(req));

(\result == 2)==>(in.matches(load));

(\result == 3)==>(in.matches(road));

(\result == -1)==>otherwise;

首先，JSF應該避免使用中間變量。原來的寫法暴露了實現細節。

其次，更推薦將\result做爲蘊含式的前件。

最後，所謂「更好的寫法」應該避免使用otherwise。這裏保留是考慮程序的可擴展性，即新增控制檯指令。然而，這就要求程序員必須頭腦清醒，明確otherwise什麼時候被觸發。

2-4：向隊列加入一條請求。原寫法：

(queue.length == \old(queue)+1);

(queue[length-1] == req);

更好的寫法：

(queue.size == \old(queue).size + 1) && (queue.contains(req));

原文第二行屬於暴露細節的寫法。出現類似問題的還有從隊列取出請求的方法。

2-5：SafeFile類的構造方法。原寫法：

(!fname.valid())==>(throw Exception);

(fname.valid)==>(create the file and its writer);

更好的寫法：

(fname.valid)==>(this.file == File(fname));

( ! fname.valid)==>(exceptional_behavior(IOException));

原文寫法沒有遵循JSF語法。

5、按照做業分析被報的功能bug與規格bug在方法上的彙集關係

第九次做業：道路臨時開關、道路流量

沒有被發現任何bug

 

第十次做業：紅綠燈系統

BUG10-1：出租車crash

奇怪，這個BUG沒法復現。

 

第十一次做業：可追蹤出租車

BUG11-1：出租車回頭問題，流量處理不當

相關方法：public void run_edge()

方法規格沒被報告bug，可是規格是拿天然語言表述的。可見本身在一個方法裏面加入了過多功能，代碼行數達到50行。

BUG11-2：遠距離出租車接客

相關方法：

public int dispatch(Request r)

public boolean receive(Request r)

public boolean within(_Point src)

方法dispatch的規格經本身檢查與實際方法代碼有出入，可見本身沒有按照規格編寫方法。本身對於「什麼樣的出租車能夠接單」這個問題在規格設計時就沒想清楚，寫出來的代碼天然是有漏洞的。

BUG11-3：出租車尋找最短路徑時數組越界

相關方法：public void search(int dst)

規格寫得太簡略，並且邏輯有問題。下一個點必須在城市地圖內。這一點不但寫規格時沒寫，並且寫代碼時也沒注意，不出問題纔怪。

BUG11-4：不一樣時的相同位置請求衝突。

相關方法：public void search(int dst)

不徹底是這個方法的問題。沒有認真讀下發的gui.java代碼，使用裏面的函數時沒有仔細分析其實現邏輯。

6、概括本身在設計規格和撰寫規格時的基本思路和體會

一、針對方法規格

方法規格主要包含REQUIRES, MODIFIES, EFFECTS三部分。

REQUIRES即前置條件，是調用者傳入參數等方面所必須知足的約定。若是須要傳對象或容器，通常都會要求對象不爲空，容器有元素。此外，我還會思考數據具備的實際含義。運行在一個城市的出租車系統，傳入的座標點顯然不能超出城市範圍，出租車的位置和狀態必須有效，等等。不作格式檢查的輸入提取，也要在前置條件寫清楚輸入格式。

MODIFIES寫方法會改變的數據。這裏的數據應該理解爲用戶（或使用你代碼的程序員）關心的數據，所以局部變量的改變大可沒必要寫在這裏。類屬性的改變也沒有必要全寫，只須要填寫呈現給用戶看的那部分數據的改變。

EFFECTS即後置條件，是方法執行完畢返回結果、類屬性等數據所知足的約定。初學者（包括我）每每容易將部分算法邏輯展現在裏面，但這是不可取的行爲。實際上，EFFECTS向方法調用者屏蔽了部分細節，進行了一層抽象。調用者和用戶只關心方法執行後的效果、返回值知足的條件，並不關心值是如何獲得的。另外，EFFECTS內容爲實現算法也每每暗示着做者是在方法完成以後再補充的規格。根據Head First Java的講法，正確的順序首先是寫僞代碼和測試代碼，即首先想清楚方法的執行效果，而後纔是具體實現（寫正常代碼）。本末倒置每每是這類問題的深層緣由。

初學者寫面向對象程序，容易出現所謂「麪條代碼」的問題，將全部業務邏輯放在一個方法裏面。我本身提煉出一個規律：方法的代碼超過了50行，EFFECTS部分每每也超過5行。若是在寫規格時感到寫起來很是困難（不知如何歸納），或是寫了太多（超過5行），每每方法的功能還能進行分拆。所以，先寫EFFECTS的另外一個好處是倒逼程序員對業務邏輯進行拆分整合，避免「麪條代碼」。

二、針對類規格

類規格的核心是編寫OVERVIEW，對於子類能夠編寫INHERIT，不變式也能夠寫在INVARIANT部分。

OVERVIEW闡明類的目標或總體輪廓。OO程序的類大致能夠分爲以方法爲核心和以數據爲核心兩種。前者的OVERVIEW側重類的目標：提供什麼方法、如何處理數據。後者的OVERVIEW側重總體輪廓：管理什麼數據。對於後者，應該避免我互測環節拿到的將全部屬性列舉出來的錯誤。類須要對用戶進行一層抽象，給用戶看到的應該是他關心的、抽象事後的數據。把全部細節展現給用戶實則是不安全的行爲，代碼可維護性也很差。就拿普通出租車而言，用戶關心的頂可能是出租車編號、當前狀態、當前位置。其它一些標記搶單之類的變量不必讓用戶知道和看到。

INVARIANT即表示不變式，是斷定對象是否有效的布爾表達式，對應boolean repOK()方法。在實現其它方法前寫出表示不變式和repOK方法，能夠倒逼設計者思考類所構造的對象的實際意義，在編寫方法過程當中繃緊一根弦，確保方法調用先後對象的有效性。寫不變式時應抓住程序的實際應用場景，以指導書規定和嘗試輔助判斷。

三、雜感

首先談談本身出現的問題：愈來愈懶得作自我測試。用來處理測試文件輸入的那個類居然一組樣例也沒跑過，最後確定是崩。儘管本身能夠找馮如杯比賽忙、操做系統難寫之類的理由，可是測試者歷來不會心慈手軟。這也不是未來走上工做崗位應該有的態度。本身編寫測試用例時，也不能對本身太好。爲了測試多線程的正確性，兩條請求之間間隔的時間不能太長，不然不少潛在的問題查不出來。（例如BUG11-2）總之，寫完代碼以後要多進行自我測試，寫出來的程序錯誤才更少。

其次談談廣泛出現的問題：要求用JSF寫規格後，不少人沒有把它當成訓練面向對象思惟的途徑，而當成了增長扣分收入的法寶。他們對拿到的互測代碼大量地報告規格BUG，其中不少BUG未必真實。這實際上曲解了老師的本意，浪費了提高本身能力的機會，得不償失。一方面，但願這些學生端正學習態度，切實鍛鍊自身能力，而不是追求一個外在的分數。另外一方面，但願教學組增長對亂扣分行爲的檢查和懲處力度。

總之，編寫規格的質量不要僅依賴測試者的評價，要多結合課件、文檔說明，找本身的不足並改進。