前言
在最近的一個月的課程中，筆者對於規格化程式設計進行了深入的學習。運用面向物件抽象思想對編寫的程式進行過程抽象、異常處理、資料抽象、類的層次規格與迭代等等規格設計，使得程式結構化程度提高，具有更好的可維護性和複用性。本文通過分析並總結近三次作業規格設計情況，分享我在規格化程式設計上的見解與體會。
作業規格錯誤彙總
- 規格錯誤詳細資訊：
| 編號 | 型別 | 所在類 | 方法名稱 | 程式碼行數 | 詳細 |
|---|---|---|---|---|---|
| 1 | 前置條件不規範 | InputHandler | parseOrderReq | 5 | 未使用形式語言 |
| 2 | 前置條件不規範 | InputHandler | parseRoadChangeReq | 5 | 未使用形式語言 |
| 3 | 前置條件不規範 | InputHandler | parseSearchTaxiReq | 4 | 未使用形式語言 |
| 4 | 前置條件不規範 | InputHandler | parseSearchStateReq | 7 | 未使用形式語言 |
| 5 | 後置條件為實現演算法 | LoadFileUnit | setFlow | 23 | 未使用形式語言表示呼叫者看到的變化 |
| 6 | 後置條件為實現演算法 | LoadFileUnit | setTaxi | 34 | 未使用形式語言表示呼叫者看到的變化 |
| 7 | 後置條件為實現演算法 | LoadFileUnit | setReq | 31 | 未使用形式語言表示呼叫者看到的變化 |
| 8 | 後置條件為實現演算法 | Map | setTaxi | 1 | 未使用形式語言表示呼叫者看到的變化 |
| 9 | 後置條件為實現演算法 | ReqHandler | markServableTaxi | 4 | 未使用形式語言表示呼叫者看到的變化 |
| 10 | 後置條件為實現演算法 | ReqHandler | assignTaxi | 18 | 未使用形式語言表示呼叫者看到的變化 |
| 11 | 後置條件為實現演算法 | ReqHandler | run | 12 | 未使用形式語言表示呼叫者看到的變化 |
| 12 | 後置條件邏輯錯誤 | TaxiAction | run | 85,91,93[1] | 後置條件未描述方法所有的影響 |
- 資料彙總：
| 型別 | 總計 | 平均程式碼行數 | 最大程式碼行數 |
|---|---|---|---|
| 前置條件不規範 | 4 | 5 | 7 |
| 後置條件為實現演算法 | 6 | 18.5 | 34 |
| 後置條件邏輯錯誤 | 1 | 89.7 | 93 |
| 總計 | 11 | 33.6 | 93 |
規格錯誤分析
第九次作業
在第九次作業中，根據需求需要加入道路開關功能以及增加用於初始化系統的檔案讀取指令，並且為所有方法補充過程規格。在這次作業中由於絕大部分程式碼都是來自上一次作業，許多方法在實現前僅考慮了SOLID原則[2]而未考慮規格設計，每個方法的規格都是在實現後補充上去的（這在順序上是倒置的）。有一小部分的方法在功能與產生的作用比較繁雜，難以用形式語言進行描述，最後只能用自然語言作為替換。但對於這些方法使用自然語言也不太好說清楚其後置條件，最後導致了後置條件為演算法是實現的過程的錯誤。此外，在使用形式語言描述的時候，對於一些方法的處理邊界的描述上存在一些缺陷。
在完成這次作業前，筆者學習了使用異常丟擲來區分正常情況與異常情況。但由於在此之前設計程式碼時未考慮使用反射機制來處理異常情況，而使用形如null等變數來當作異常情況的返回。如果要加入這一功能需要重構大部分方法中的討論情況。由於時間關係，在這次作業中只在新加入的部分使用了異常處理機制。因而在舊程式碼的部分的規格設計中對於異常情況沒有顯示錶示，而是返回一些無意義的資料（從呼叫者的角度來看是不友好的）。
在測試別人的程式時發現的規格問題基本與我的相似，基本是方法的冗雜致使規格的後置條件為實現過程或者後置條件有遺漏。
第十次作業
在這次作業中，根據需求僅需增加路口的紅綠燈功能，工作量較少（雖然計算時間和流量比較困難），因此筆者將之前寫的程式碼根據過程抽象原則進行了優化。對功能較多的方法進行了重構，將其功能進行了分割，分散至不同類或者方法當中。在此之後程式中絕大多數的方法都能夠用較為簡潔的形式語言描述。因此在這次作業的測試階段，對方未報告規格錯誤。
此外，需求要求補充每個類的類規格、抽象函式以及物件有效性驗證方法[3]。由於最初設計時著重考慮了SOLID原則，程式中每個類的功能是比較明確的。因而增加類規格的困難不大，在互測階段也沒被報告錯誤。
第十一次作業
在這次作業中，根據需求需要對計程車種類進行擴充，增加一種能滿足新需求（不贅述）的計程車，以及實現迭代輸出服務記錄的功能。在繼承前一種計程車的同時要著重考慮里氏替換原則，實現有效的子類設計，並且還需附有有效性論證。具體體現在子類方法與父類方法的前置條件與後置條件的空間上。在我的程式中，子類重寫父類方法過程時僅對後置條件進行了擴充，使其能滿足里氏替換原則。因而在互測階段未被報告錯誤。在我測試的程式中，設計者將所有父類的方法複製到類子類中，並對細節進行了改動。雖然這種做法有很多贅餘，但通過論證也未發現問題。
規格優化
- 後置條件為實現過程。
優化前：
public synchronized void setTaxi(int index, int locaX, int locaY, TaxiState state)
/**
* @REQUIRES: 0<=index<100;0<=locaX<=79;0<=locaY<=79;
* @MODIFIES: gui
* @EFFECTS: (在GUI中將編號為index的計程車設定為state狀態，移至(locaX,locaY)位置);
* @THREAD_REQUIRES:\locked(this);
*/
優化後：
public synchronized void setTaxi(int index, int locaX, int locaY, TaxiState state)
/**
* @REQUIRES: (0<=index<100);(0<=locaX<=79);(0<=locaY<=79);
* @MODIFIES: gui
* @EFFECTS: (gui.taxi[index].locaX==locaX)&&(gui.taxi[index].locaY==locaY)&&(gui.taxi[index].state==state);
* @THREAD_REQUIRES: \locked(this);
*/
- 前置條件可以擴充套件，後置條件可以對異常進行處理。
優化前：
public RoadChangeReq parseRoadChangeReq(String input, long time){
/**
* @REQUIRES: input符合道路更改請求格式；
* @EFFECTS: \result==解析後的道路更改請求物件；
*/
Matcher roadReqMatcher = this.roadReqPattern.matcher(input);
if(roadReqMatcher.matches()){
return new RoadChangeReq(roadReqMatcher.group(1),
roadReqMatcher.group(2),
roadReqMatcher.group(3),
roadReqMatcher.group(4),
roadReqMatcher.group(5),
time);
}
else
return null;
}
優化後：
public RoadChangeReq parseRoadChangeReq(String input, long time) throws Exception{
/**
* @REQUIRES: input!=null；
* @EFFECTS: (!roadReqPattern.match(input))==>(\result==解析後的道路更改請求物件)；
* (!roadReqPattern.match(input))==>exception_behavior(Exception);
*/
Matcher roadReqMatcher = this.roadReqPattern.matcher(input);
if(roadReqMatcher.matches()){
return new RoadChangeReq(roadReqMatcher.group(1),
roadReqMatcher.group(2),
roadReqMatcher.group(3),
roadReqMatcher.group(4),
roadReqMatcher.group(5),
time);
}
throw new Exception("不符合道路更改請求格式")；// 可以自定義異常。
}
- 後置條件應為具體現象。
優化前：
public void setTaxi(int taxiNo, TaxiState state, int credit, int locaX, int locaY){
/**
* @REQUIRES: 0<=taxiNo<100;credit>=0;0<=locaX<79;0<=locaY<79;
* @MODIFIES: this.set,gui
* @EFFECTS: 更新出租車位置。
*/
this.set[taxiNo].setTaxiInfo(state, credit, locaX, locaY);
}
優化後：
public void setTaxi(int taxiNo, TaxiState state, int credit, int locaX, int locaY){
/**
* @REQUIRES: 0<=taxiNo<100;credit>=0;0<=locaX<79;0<=locaY<79;
* @MODIFIES: this.set,gui
* @EFFECTS: this.set[taxiNo].locaX==locaX;
* this.set[taxiNo].locaY==locaY;
* this.set[taxiNo].credit==credit;
* this.set[taxiNo].state==state;
* gui.taxi[taxiNo].locaX==locaX;
* gui.taxi[taxiNo].locaY==locaY;
*/
this.set[taxiNo].setTaxiInfo(state, credit, locaX, locaY);
}
- 後置條件應為具體現象。
優化前：
class InputListener implements Runnable {
private ReqBuffer reqBuffer;
private TaxiInfoSet taxis;
private Map map;
......
@Override
public void run() {
/**
* @MODIFIES: this.map,this.reqBuffer,this.taxis,System.out
* @EFFECTS: (監控到乘客請求)==>(解析並將請求物件加入reqBuffer);
* (監控到道路更改請求)==>(解析並更改map中的道路);
* (監控到計程車搜尋請求)==>(解析並System.out相應資訊);
* (監控到計程車狀態搜尋請求)==>(解析並System.out相應資訊);
*/
優化後：
class InputListener implements Runnable {
private ReqBuffer reqBuffer;
private TaxiInfoSet taxis;
private Map map;
/**
（省略正則表示式）
public static String REQREGEX;
public static String ROADREQREGEX;
public static String SEARCHTAXIREGEX;
public static String SEARCHSTATEREGEX;
*/
......
@Override
public void run() {
/**
* @MODIFIES: this.map,this.reqBuffer,System.out
* @EFFECTS: (System.in.match(REQREGEX))
* ==>(this.reqBuffer.contains(new Request(System.in)));
* (System.in.match(ROADREQREGEX))
* ==>(this.map.road.status==System.in.status);
* (System.in.match(SEARCHTAXIREGEX))
* ==>(System.out==this.taxis[System.in.taxiNo].info);
* (System.in.match(SEARCHSTATEREGEX))
* ==>(\all Taxi taxi;
* this.taxis.contains(taxi)
* &&taxi.state==System.in.taxiState;
* System.out.contains(taxi.info));
*/
- 後置條件可以寫為形式語言。
優化前：
private void markServableTaxi(ReqWin reqWin)
/**
* @ REQUIRES: reqWin!=null;
* @ MODIFIES: rewWin;
* @ EFFECTS: 將符合搶單條件的計程車加入至reqWin的taxiSet中；
*/
優化後：
private void markServableTaxi(ReqWin reqWin)
/**
* @ REQUIRES: reqWin!=null;
* @ MODIFIES: rewWin;
* @ EFFECTS: (\all TaxiInfo taxi;
* this.taxiSet.contains(taxi)
* &&taxi.isin(reqWin.district);
* reqWin.taxiSet.contains(taxi));
*/
作業功能錯誤彙總
第九次作業
在這次作業中筆者被報告了以下三個錯誤：
- 錯誤現象：當讀取的檔案中有多條乘客請求時程式會死鎖。
- 錯誤分析：在程式的設計中，初始化乘客請求是通過系統啟動前就將檔案中的請求解析並加入至請求快取區中；在此之後排程器將快取區中的請求取出再按排程策略分配服務的計程車。在最初的程式中，這部分的程式碼如下：
public class SysMain {
public static void main(String[] argv) {
......
LoadFileUnit loadFileUnit = new LoadFileUnit(); // 構造檔案讀取器
loadFileUnit.checkLoad(); // 檢查指令合法性
......
ReqBuffer reqBuffer = new ReqBuffer(); // 構造請求快取區
......
......
// 構造排程器
ReqHandler reqHandler = new ReqHandler(reqBuffer, taxiSet, map);
loadFileUnit.setReq(reqBuffer, map); // 逐個加入請求
new Thread(reqHandler).start(); // 啟動排程執行緒
......
}
在此之中請求快取區的容量為1。進而很明顯當請求數大於1時由於此時排程執行緒還未啟動，沒有執行緒能夠消耗快取區的請求，導致了主執行緒一直等待快取區為空。而這種情況不會發生，最後導致了死鎖。
- 錯誤改正：將排程執行緒的啟動時機提前即可。
----------分割線----------
- 錯誤現象：多輛計程車同時計算路徑時有一定機率報出
地圖不連通，程式退出並結束程式。 - 錯誤分析：在出租車計算路徑是需要使用公用的矩陣儲存廣度遍歷的結果，程式中共享資源的互斥存在缺陷導致計算進入了錯誤的步驟，得出了地圖不連通的結果。筆者在原程式中通過對課程組提供的路徑計算方法增加synchronized關鍵詞加鎖實現資源的互斥，但由於課程組提供的GUI包中大多數類的封裝問題，導致該互斥操作不完善，最終導致該錯誤發生（雖然我測了好久也沒出現這種情況）。
- 錯誤改正：構造Map類（執行緒安全類）包裝地圖操作。
----------分割線----------
- 錯誤現象：未排除相同請求。
- 錯誤分析：相關程式碼如下：
// 請求視窗集合類的插入方法
public void append(Object req) {
Request newReq = (Request)req;
System.out.println(newReq);
for(int i= 0; i < this.length; i++) {
int[] loca = this.list[i].getReq().getLoca();
int[] aim = this.list[i].getReq().getAim();
long time = this.list[i].getReq().getMakeTime();
if(newReq.getLoca()[0] == loca[0]
&& newReq.getLoca()[1] == loca[1]
&& newReq.getAim()[0] == aim[0]
&& newReq.getAim()[1] == aim[1]
&& newReq.getMakeTime() == time) {
System.out.println("相同請求 : " + newReq);
// 標記 //
}
}
// 在末尾插入。
this.list = Arrays.copyOf(this.list, ++this.length);
this.list[this.length - 1] = new ReqWin(newReq);
}
在對集合中已有的請求進行遍歷並判斷為相同請求後為中止方法，使相同請求也能被插入至請求佇列。
- 錯誤更改：在標記處增加
return;。
----------分割線----------
在第十與十一次作業時筆者未被報告程式錯誤。
在測試別人程式的過程中，筆者測試的這三位同學的程式都無法正常地執行多條乘客請求。在第九次作業時，被測試的程式在執行多條請求時會出現請求間資訊錯位的現象，初步認定是請求共享部分的互斥工作存在缺陷。在第十次作業時，被測試的程式在執行3至6條程式時會異常地停止執行，無任何反應，但不會崩潰退出。在閱讀程式碼後大致由於路徑計算時耗時過多，以致多輛計程車同時計算長距離請求時延遲較大。當執行超過7條請求時，程式會有崩潰的可能，機率隨請求數的增加而增加，崩潰的原因是堆疊溢位。在第十一次作業的時候，被測試的程式在執行多條請求時會出現嚴重的延遲現象。由於這位同學的程式碼的可讀性實在太差，筆者沒能找出導致錯誤的程式碼。
思考與體會
在經過這三次作業之後，我對於規格化程式設計的重要性有了親身體會。在編寫面向物件程式前就應當對程式中的資料和處理過程進行抽象，定義出對資料的操作以及資料管理的方式，歸納出程式中需要進行的行為，限定各個操作的邊界以及使用者可見的內容。再結合上個階段學的面向物件程式設計原則，對於程式中的類設計做出相應限定，使得編寫的類具有更好的延展性、可維護性與魯棒性。
經過總結，對於程式中方法的設計過程大致分為以下幾步：
1. 明確方法存在的意義。
2. 明確方法結果正確的判定條件。
3. 明確方法對呼叫者提出的條件，以保證結果正確。
4. 明確方法執行期間修改的資料。
5. 按照要求的方式整理前置條件、修改資料、後置條件。
經過了短暫的一個月的實踐，筆者雖對這些思想有了不少的體會，但還有待更多的實踐深化。