OO學習總結（三）
規格化設計
軟件工程的重要目標之一是實現軟件開發過程各階段的自動化，軟件自動化的前提是形式化,包括軟件需求規格的形式化、軟件設計規格的形式化和 算法描述的形式化。
Z語言由牛津大學程序設計研究小組開發，是一種應用較為廣泛的形式規格說明語言，它以一階謂詞邏輯和集合論為基礎對軟件系統的靜態特征和動態特征進行形象描述。
面向對象技術在系統分析設計，程序設計等方面所能提供的類層次，整體-部分關系，封裝性，繼承性使得其得到了廣泛應用。因而人們也開始研究面向對象軟件的形式規格描述問題。
從90年代初開始，國際上對Z語言的面向對象擴展相繼提出了MOOZ，Object-Z,Z++等方案，將Z語言擴展到能夠支持面向對象的系統分析方法上來。
到現在，面向對象規格化設計理論進一步豐富。比如
- 為保證程序的正確性，Hoare[1] 提出了關於接口的規格方法，即若一種方法在執行前滿足前置條件，運行後滿足後置條件，那麽這種方法就是正確的。
- Guttag[2] 使用抽象的數據類型來降低設計和實現大型軟件的復雜度，用代數公裏證明規格的正確性。
- Robert[3]提出契約式編程來表達接口的前置條件和後置條件。
- ...
可見，規格化設計是開發大型軟件項目必不可少的技術手段，學習規格化設計是重要且必要的。
[1] Hoare, C. A. R. “An Axiomatic Basis for Computer Programming.” Communications of The ACM, vol. 12, no. 10, 1969, pp. 576–580.
[2] Guttag, John V., et al. “Abstract Data Types and Software Validation.” Communications of The ACM, vol. 21, no. 12, 1978, pp. 1048–1064.
[3] Felleisen, Matthias, and Robert Bruce Findler. Behavioral Interface Contracts for Java. 2000.
規格設計的bug及原因分析
第九次作業：
| 編號 | 類別 | 所在方法 | 方法代碼行數 |
|---|---|---|---|
| 1 | Modifies邏輯錯誤 | main方法 | 37 |
測試者認為Main方法的Modifies不應為None.但是我認為整個出租車系統對Main方法來說都是內部的，也就是沒有修改外部的屬性，Main方法也沒有修改傳入的參數，所以Modifies為None我覺得是合理的。還在仲裁中。
第十次作業:
無
第十一次作業：
| 編號 | 類別 | 所在方法 | 方法代碼行數 |
|---|---|---|---|
| 1 | Modifies不完整 | Map類的構造器 | 8 |
| 2 | Modifies邏輯錯誤 | Map類createMap | 30 |
1是因為構造器修改了自身的屬性，寫Modifies沒有寫全。出現這個問題是因為在本次作業中，對地圖的構造方法進行了修改，但是遺漏了規格的更新。
2是因為createMap的MODIFIES裏有多余的內容。方法內部並沒有修改某個屬性，但MODIFIES裏寫了。也是因為本次作業修改了方法，卻遺漏了規格的更新。
前置條件/後置條件的改進
前置條件:
| 編號 | 方法 | 原寫法 | 改進寫法 |
|---|---|---|---|
| 1 | Car: driving() | None | this.map instanceof Map |
| 2 | Car: waiting() | None | this.c_map instanceof TaxiGUI |
| 3 | Car: toCus() | None | this.p instanceof Passenger; this.map instanceof Map |
| 4 | CarInfo: toString() | None | this.info != null; |
| 5 | InputHandler: loadFlow(BufferedReader br) | br!=null | br!=null; this.map instanceof Map; |
後置條件：
| 編號 | 方法 | 原寫法 | 改進寫法 |
|---|---|---|---|
| 1 | Map: findShortestPath(int start, int end, int car_type) | the map is a connected graph==>\result == path where path is a Vector containing the shortest path from point start to point end with the minimum car flow; | \result.get(0)==start && \result.get(\result.size-1)==end && (\all int i; 0<=i<=\result.size-2;isAjacent(\result.get(i), \result.get(i+1)))&& (\all Vector v; v.get(0)==start && v.get(v.size-1)==end && (\all int i;0<=i<=v.size-2;isAjacent(v.get(i),v.get(i+1)));v.size>=\result.size); |
| 2 | Map: run | 500ms after starting, decrease the value of every element in \this.flow by value of the corresponding element in \this.original_flow; | \all int i,j;0<=i,j<80;flow[i][j]==\old(flow[i][j])-original_flow[i][j]; |
| 3 | OrderTrace: cusEndPoint() | \result == Point t that represents the customer‘s destination; | \result.getX()==p.getDes()/80 && \result.getY()==\p.getDes()%80; |
| 4 | OrderTrace: cusStartPoint() | \result == Point t that represents the customer‘s position; | \result.getX()==p.getStart()/80 && \result.getY()==\result.getStart()%80; |
| 5 | PassengerQueue: 構造方法 | \this.customers == new LinkedBlockingQueue(); | \this.customers instanceof LinkedBlockingQueue(); |
功能bug
第九次作業：
| 方法名 | 功能bug | 規格bug |
|---|---|---|
| main | 1 | 1 |
第十次作業：
| 方法名 | 功能bug | 規格bug |
|---|---|---|
| InputHandler: loadMap | 1 | 0 |
| LightManager: run | 1 | 0 |
| LightManager: init | 1 | 0 |
| Car: takePassenger | 1 | 0 |
第十一次作業：
| 方法名 | 功能bug | 規格bug |
|---|---|---|
| Car: waitForLight | 1 | 0 |
| Map: 構造方法 | 0 | 1 |
| Map: createMap | 0 | 1 |
| Map: run | 1 | 0 |
規格撰寫的思路和體會
設計規格
先確定好這個方法的輸入和輸出, 確定方法內需要用到的數據結構。根據方法用到的算法，在草稿紙上演算一遍，確認只需要這些輸入就可得到想要的結果。
然後根據輸入確定REQUIRES,根據結果確定EFFECTS，根據EFFECTS確定MODIFIES。
撰寫規格
- 前置條件可根據輸入來撰寫，通常是要求輸入不為null， 如果方法內用到了對象的屬性， 應當把對該屬性的要求也加入REQUIRES
- MODIFIES主要就看方法內修改了哪些屬性，或者傳入的參數，這個比較容易。
- EFFECTS應該是規格裏最不好寫的部分了。很多東西用自然語言表述很簡單，但轉化為JSF就很麻煩。可以只看\result的特征，並將其轉化為謂詞邏輯表達出來，否則很容易將規格寫成算法實現。
OO學習總結（三）