面向對象第三次博客
規格化設計的發展歷史和重要性：
規格化設計與結構化、模塊化設計密不可分。從計算機開始發展以來，隨著代碼量的不斷增加，程序功能的不斷復雜化，簡單的面向過程編程不再能夠滿足人們的需要，因此，出現了結構化程序設計。
在之後程序設計思想的不斷發展過程中，規格越來越顯得重要。Dijkstra 於 1968 發表了著名的《GOTO 有害論》的論文,提出了程序設計中常用的GOTO語句的三大危害,引起了長達數年的論戰,並由此產生了結構化程序設計方法。第一個結構化的程序語言Pascal也在此時誕生,並迅速流行起來。
在此之後，隨著硬件的快速發展，程序的復雜度迎來了再一次的飛躍，而這時出現了面向對象編程。此後規格化得到了人們越來越多的重視，因為其可以幫助設計者更好的設計自己的程序，避免在設計過程中產生嚴重錯誤，同時也能夠增強程序的可維護性。
作業中的規格BUG及出現原因：
列舉不好的前後置條件並給出改進寫法：
1. 前置條件
(1)
/**
* @REQUIRES: None;
* @MODIFIES: credits;
* @EFFECTS: credits == \old(credits)+x;
*/
改進寫法：由於出租車作業中出租車的信用只可能增加，所以這個函數中x的值只能為正數，需要在Requires中限制x為正數，改進為：
/**
* @REQUIRES: x>0;
* @MODIFIES: credits;
* @EFFECTS: credits == \old(credits)+x;
*/
(2)
/**
* @REQUIRES: (\all int i; 0 <= i < 80; m[i].length() == 80 );
* @MODIFIES: map;
* @EFFECTS: map == m;
*/
改進寫法：由於地圖是80X80的數組，所以既要判斷傳入數組的行數為80，又要判斷其列數為80。Requires中只進行了每行列數的判斷，還需要限制行數為80行，改進為：
/**
* @REQUIRES:
(\all int i; 0 <= i < 80; m[i].length() == 80 )&&(m.length()==80);
* @MODIFIES
* @EFFECTS: map == m;
*/
(3)
/**
* @REQUIRES: (i>=0 && i<80) && (t>0) && (g!=null) && (p!=null);
* @MODIFIES:
* System.out, id, status, time, x, y, reqID, reqSet, posSet;
* @EFFECTS:
* Initial the position and state of a special taxi;
*/
改進寫法：這是可追蹤出租車構造函數的JSF，由於可追蹤出租車的序號為0-29，因此Requires中i的範圍應該為[0,30]，改進為：
/**
* @REQUIRES: (i>=0 && i<30) && (t>0) && (g!=null) && (p!=null);
* @MODIFIES:
* System.out, id, status, time, x, y, reqID, reqSet, posSet;
* @EFFECTS:
* Initial the position and state of a special taxi;
*/
(4)
/**
* @REQUIRES: (0<=x1<80) && (0<=y1<80) && (0<=x2<80) && (0<=y2<80) && (count>0);
* @MODIFIES: flow, initial, System.out;
* @EFFECTS:
*count>=0 ==> flow[x1*80+y1][x2*80+y2]== count;
*count>=0 ==> flow[x2*80+y2][x1*80+y1]== count;
*count>=0 ==> initial.contains(x1);
*count>=0 ==> initial.contains(y1);
*count>=0 ==> initial.contains(x2);
*count>=0 ==> initial.contains(y2);
*count>=0 ==> initial.contains(count);
改進寫法：在這裏Requires和Effects中count的取值產生了沖突，其實count是否為0並不影響程序正確執行，但是為了JSF的一致，還是要把Requires改進為：
/**
* @REQUIRES: (0<=x1<80) && (0<=y1<80) && (0<=x2<80) && (0<=y2<80) && (count>=0);
* @MODIFIES: flow, initial, System.out;
* @EFFECTS:
*count>=0 ==> flow[x1*80+y1][x2*80+y2]== count;
*count>=0 ==> flow[x2*80+y2][x1*80+y1]== count;
*count>=0 ==> initial.contains(x1);
*count>=0 ==> initial.contains(y1);
*count>=0 ==> initial.contains(x2);
*count>=0 ==> initial.contains(y2);
*count>=0 ==> initial.contains(count);
(5)
/**
* @REQUIRES: x!=null;
* @MODIFIES: queue;
* @EFFECTS:
*queue.contains(x);
改進寫法：這個函數是把請求x加入到隊列中，在這裏還需要對請求的類別進行判斷，即只把乘客請求加入到隊列中，不用管開關路請求，將其修改為：
/**
* @REQUIRES: (x!=null)&&(x.gettype()==0);
* @MODIFIES: queue;
* @EFFECTS:
*queue.contains(x);
2. 後置條件
(1)
/**
* @REQUIRES: None;
* @MODIFIES: None;
* @EFFECTS: /result == map;
*/
改進寫法：這個函數是返回地圖數組，由於地圖在程序中是共享資源，因此這個方法是加了synchronized關鍵字的，所以還要寫Thread_requires和Thread_effects。
/**
* @REQUIRES: None;
* @MODIFIES: None;
* @EFFECTS: /result == map;
* @THREAD_REQUIRES: \locked(this);
* @THREAD_EFFECTS: \locked();
*/
(2)
/**
* @REQUIRES: (x!=null)&&(x.gettype()==0);
* @MODIFIES: queue;
* @EFFECTS: Append the request to the queue;
改進寫法：這個函數是把用戶請求x加入到隊列中，Effects是比較容易使用布爾表達式的，因此最好把自然語言寫為布爾表達式，將其修改為：
/**
* @REQUIRES: (x!=null)&&(x.gettype()==0);
* @MODIFIES: queue;
* @EFFECTS:
* ! (\old(queue).contains(x)) ==> queue.contains(x);
* queue.size() == \old(queue).size()+1;
(3)
/**
* @REQUIRES: new File(s).isFile() ;
* @MODIFIES: map;
* @EFFECTS:
* Parse the map and check it;
改進寫法：這個函數接收一個文件的路徑，然後從該文件中提取地圖信息，當地圖信息發生錯誤，拋出異常，因此在Effects中要有關於異常的Effects：
/**
* @REQUIRES: (x!=null)&&(x.gettype()==0);
* @MODIFIES: queue;
* @EFFECTS:
* Parse the map and check it;
* (\exist int i; 0<=i<=map.length,0<=j<=map[i].length; map[i][j]<0) ==> exceptional_behavior(InvalidException);
功能BUG與規格BUG的內聚關系：
心得體會：
個人寫規格的基本思路就是，先寫方法再寫規格，至於為什麽這麽做，在下文有說。首先根據方法對參數的要求來寫Requires，再從方法中找到會被改變的類屬性，以此來寫Modifies，最後用自然語言或者布爾表達式（盡可能用布爾表達式）來寫方法的Effects。除此之外還要註意同步方法和拋出異常方法的規格書寫。
這三次作業給我最大的感受就是寫代碼的難度比前幾次作業要簡單，但是相應地要花部分時間在寫規格上面。寫規格這個作業的出發點是好的，就是為了讓我們養成良好的寫代碼的習慣，增強代碼的可讀性和維護性等。但是在現階段的作業來說，在測試別人的代碼時，讀規格除了檢查JSF是否有BUG之外個人感覺作用不大。對於那些行數比較少的方法，讀規格和讀代碼的時間是差不多的，不如直接讀代碼，完全弄清楚這個方法的含義。而對於那些行數比較多的方法，寫的規格根本不能完全地、詳細地體現出這個方法做了什麽，歸根結底還是要去讀代碼。
除此之外個人感覺“先寫規格再寫方法”的這個要求對於這三次作業來說不太合理，因為規格是我們在寫了出租車的基本框架之後才要求添加的。這幾次的作業我都是在寫完方法之後才為方法添加規格，事實上這的確比先寫規格再寫方法節約時間。
總之，寫規格的出發點是好的，但是在實現過程中可能因為其他的一些原因讓人覺得這個東西沒什麽用，還浪費許多時間。希望OO課在以後發展的過程中能夠解決這些困擾的問題，讓學生不再有那麽多怨言吧。
面向對象第三次博客