OO9~11次作業總結
一、規格化設計的發展歷史
第一代計算機軟件出現在1946~1953年，使用機器語言編寫，由0和1組成。不同的計算機使用不同的機器語言，程序員必須記住每條及其語言指令的二進制數字組合，因此，只有少數專業人員能夠為計算機編寫程序，這就大大限制了計算機的推廣和使用。用機器語言進行程序設計不僅枯燥費時，而且容易出錯。
在這個時代的末期出現了匯編語言，它使用助記符表示每條機器語言指令，例如ADD表示加，SUB表示減，MOV表示移動數據。相對於機器語言，用匯編語言編寫程序就容易多了。
1954年後，計算機硬件變得更加強大，需要更強大的軟件工具使計算機得到更有效地使用。IBM公司從1954年開始研制高級語言，同年發明了第一個用於科學與工程計算的FORTRAN語言。1959年，賓州大學的霍普（Grace Hopper）發明了第一個用於商業應用程序設計的COBOL語言。1964年達特茅斯學院
此時，計算機軟件實際上就是規模較小的程序，程序的編寫者和使用者往往是同一個（或同一組）人。由於程序規模小，程序編寫起來比較容易，也沒有什麽系統化的方法，對軟件的開發過程更沒有進行任何管理。這種個體化的軟件開發環境使得軟件設計往往只是在人們頭腦中隱含進行的一個模糊過程，除了程序清單之外，沒有其他文檔資料。
1965年後，計算機的性能進一步大幅提升，因此出現了分時操作系統，負責組織和安排各個作業。1968年荷蘭計算機科學家狄傑斯特拉（Edsgar W.Dijkstra）發表了論文《GOTO語句的害處》
20世紀70年代出現了結構化程序設計技術，Pascal語言和Modula-2語言都是采用結構化程序設計規則制定的，Basic這種為第三代計算機設計的語言也被升級為具有結構化的版本，此外，還出現了靈活且功能強大的C語言。同時，許多不同的形式規格說明語言和軟件開發方法也在不斷發展。1974到1975年間，B.Liskow/S.N. Zilles和J. Guttag引入了"抽象數據類型"的概念。1976年E.W. Dijkstra定義了"最弱前置條件"的概念。1977年R.Burstall和J.Goguen提出了第一個代數規格說明語言：Clear。1980到1986年間C.Jones定義了VDM語言，也就是維也納開發方法。1985到1992年間牛津大學的程序研究小組開發了Z規格說明語言。與此同時BP研究室開發了稱之為B方法的面向模型的規格說明語言。從1991年開始，面向對象的形式規格說明語言開始發展，例如，Object-Z, VDM++, CafeOBJ等語言。隨著時間的推進以及軟件規模的擴大，規格化設計越來越得到人們的重視。
二、規格BUG及產生原因
在最近三次作業中，互測同學均沒有指出我的規格BUG。但是我自己認為還是存在一些問題的。
出現規格問題的原因我認為主要有以下三點：
（1）先完成了方法，後完成規格。當方法比較復雜時，完成的規格無法全面反映方法編寫時的全部效果；
（2）debug時對方法進行了修改，急於驗證效果，當編程程序問題解決之後，忘記了更新修改方法的規格；
（3）對於JSF的具體實現細節了解的不多，對於復雜的方法不清楚應當如何描述規格。
三、規格寫法以及改進
前置條件：
1、
/** * 讀入測試文檔（Load命令),如果文檔符合要求，那麽就將需要初始化的信息存儲到Smap,Sflow,Staxi,Sreq中，如果不符合要求，退出 * @REQUIRES: path!=NULL , path!="" , Smap!=NULL , Sflow!=NULL , Staxi!=NULL , Sreq!=NULL , light!=NULL * @MODIFIES : System.out,Smap,Sflow,Staxi,Sreq,light; * @EFFECTS : * (File(path).exists && File(path).meetrequirement)==>(Smap.size!=0||Sflow.size!=0||Staxi.size!=0||Sreq.size!=0); * (!(File(path).exists && File(path).meetrequirement))==>System.out(error information); */ public static void loadInit(String path,Vector<String> Smap,Vector<String> Sflow,Vector<String> Staxi,Vector<String> Sreq,int[][] light)
前置條件應是一個可以判斷的邏輯表達式，連接符應當是&& ：
/** * 讀入測試文檔（Load命令),如果文檔符合要求，那麽就將需要初始化的信息存儲到Smap,Sflow,Staxi,Sreq中，如果不符合要求，退出 * @REQUIRES: path!=NULL && path!="" && Smap!=NULL && Sflow!=NULL && Staxi!=NULL && Sreq!=NULL && light!=NULL; * @MODIFIES : System.out,Smap,Sflow,Staxi,Sreq,light; * @EFFECTS : * (File(path).exists && File(path).meetrequirement)==>(Smap.size!=0||Sflow.size!=0||Staxi.size!=0||Sreq.size!=0); * (!(File(path).exists && File(path).meetrequirement))==>System.out(error information); */ public static void loadInit(String path,Vector<String> Smap,Vector<String> Sflow,Vector<String> Staxi,Vector<String> Sreq,int[][] light)
2、
1 /** 2 * 初始化一個出租車對象，隨機生成出租車的位置，給各項屬性賦值 3 * @MODIFIES : this.x,this.y,this.num,this.state,this.credit,gui; 4 * @EFFECTS : 5 * 給出租車對象的各種屬性賦初值並在GUI上顯示; 6 */ 7 public TAXI(int i,TaxiGUI _gui,Graph _g,Output _out)
這是一個普通出租車類的構造方法，起初沒有考慮構造方法的前置條件，但實際上應當考慮各項參數的有效性，後修改為：
/** * 初始化一個出租車對象，隨機生成出租車的位置，給各項屬性賦值 * @REQUIRES: 0<=i<=100 && _gui!=NULL && _g!=NULL && _out!=NULL; * @MODIFIES : this.x,this.y,this.num,this.state,this.credit,gui; * @EFFECTS : * 給出租車對象的各種屬性賦初值並在GUI上顯示; */ public TAXI(int i,TaxiGUI _gui,Graph _g,Output _out)
3、
/** * 求（x，y）到各個可能方向上的流量值，存儲到_flow[]中 * @REQUIRES:0<=x<80 && 0<=y<80 && _flow!=NULL && dir!=NULL; * @MODIFIES: _flow[]; * @EFFECTS: * _flow[]中存儲於dir[]對應的方向的流量值 */ public synchronized void getFlow(int x,int y,int[] _flow,int[] dir,int count)
前置條件的要求不夠細致全面，應當補全為：
/** * 求（x，y）到各個可能方向上的流量值，存儲到_flow[]中 * @REQUIRES:0<=x<80 && 0<=y<80 && _flow!=NULL && _flow.length==count && dir!=NULL && dir.length==count && count>0; * @MODIFIES: _flow[]; * @EFFECTS: * _flow[]中存儲於dir[]對應的方向的流量值 */ public synchronized void getFlow(int x,int y,int[] _flow,int[] dir,int count)
4、
/** * 出租車為等待服務狀態，將出租車變為接單狀態並修改出租車的req屬性; * @REQUIRES: _req!=NULL && this.gui!=NULL; * @MODIFIES : this.state,this.req,this.gui; * @EFFECTS : * (this.state==2)==>(this.state==1 && this.req==_req) && \result==true; * (this.state!=2)==>\result==false; */ public synchronized boolean getandsetState(CRequest _req)
沒有對參數的類型進行判斷，應當改為：
/** * 出租車為等待服務狀態，將出租車變為接單狀態並修改出租車的req屬性; * @REQUIRES: _req!=NULL && this.gui!=NULL && _req instanceof CRequest; * @MODIFIES : this.state,this.req,this.gui; * @EFFECTS : * (this.state==2)==>(this.state==1 && this.req==_req) && \result==true; * (this.state!=2)==>\result==false; */ public synchronized boolean getandsetState(CRequest _req)
5、
/** * 根據spfa計算的最優路徑信息，返回目標為no1號點的出租車下一步應該去的位置; * @MODIFIES: None; * @EFFECTS: * 返回目標為no1號點的出租車下一步應該去的點的編號; */ public int printPath(int no1,int no2,int pre[])
沒有明確前置條件，應當改為：
/** * 根據spfa計算的最優路徑信息，返回目標為no1號點的出租車下一步應該去的位置; * @REQUIRES: (0<=no1<6400 && 0<=no2<6400 && pre!=NULL); * @MODIFIES: None; * @EFFECTS: * 返回目標為no1號點的出租車下一步應該去的點的編號; */ public int printPath(int no1,int no2,int pre[])
後置條件：
1、
/** * 讀入測試文檔（Load命令),如果文檔符合要求，那麽就將需要初始化的信息存儲到Smap,Sflow,Staxi,Sreq中，如果不符合要求，退出 * @REQUIRES: path!=NULL && path!="" && Smap!=NULL && Sflow!=NULL && Staxi!=NULL && Sreq!=NULL && light!=NULL; * @MODIFIES : System.out,Smap,Sflow,Staxi,Sreq,light; * @EFFECTS : loadfile中的信息存儲到Smap,Sflow,Staxi,Sreq,light中，並輸出錯誤信息； */ public static void loadInit(String path,Vector<String> Smap,Vector<String> Sflow,Vector<String> Staxi,Vector<String> Sreq,int[][] light)
盡量避免使用自然語言，應當改為：
/** * 讀入測試文檔（Load命令),如果文檔符合要求，那麽就將需要初始化的信息存儲到Smap,Sflow,Staxi,Sreq中，如果不符合要求，退出 * @REQUIRES: path!=NULL && path!="" && Smap!=NULL && Sflow!=NULL && Staxi!=NULL && Sreq!=NULL && light!=NULL; * @MODIFIES : System.out,Smap,Sflow,Staxi,Sreq,light; * @EFFECTS : * (File(path).exists && File(path).meetrequirement)==>(Smap.size!=0||Sflow.size!=0||Staxi.size!=0||Sreq.size!=0); * (!(File(path).exists && File(path).meetrequirement))==>System.out(error information); */ public static void loadInit(String path,Vector<String> Smap,Vector<String> Sflow,Vector<String> Staxi,Vector<String> Sreq,int[][] light)
2、
/** * 判斷輸入的字符串，如果輸入的字符串符合規定的指令，那麽就解析相關指令信息，存儲到req中，返回1；如果指令是測試接口指令，那麽返回相應的數值；如果是非法指令，返回0； * @REQUIRES: str!="" && req!=NULL; * @MODIFIES : System.out,req; * @EFFECTS : * 如果字符串是合法請求，存入req中，並返回1；如果是非法請求，返回其他數值； */ public static int inputcheck(String str,CRequest req)
避免使用自然語言，並且表達應當覆蓋所有可能分支，改為：
/** * 判斷輸入的字符串，如果輸入的字符串符合規定的指令，那麽就解析相關指令信息，存儲到req中，返回1；如果指令是測試接口指令，那麽返回相應的數值；如果是非法指令，返回0； * @REQUIRES: str!="" && req!=NULL; * @MODIFIES : System.out,req; * @EFFECTS : * (str.isLegalRequest)==>(req.time!=0 && (!(req.x==0 && req.tx==0 && req.y==0 && req.ty==0)))&&\result==1; * (str.isTrequest)==>\result==-2; * (str.isSrequest)==>\result==-3; * (str.isRrequest)==>\result==-4; * (str.isillegal)==>\result==0; * (str.equals("END"))==>\result==-1; */ public static int inputcheck(String str,CRequest req)
3、
/** * 拷貝指令到t * @REQUIRES: this!=NULL && t!=NULL; * @MODIFIES: t.x,t.y,t.tx,t.ty,t.time; * @EFFECTS: * t.x==this.x , t.y==this.y , t.tx==this.tx , t.ty==this.ty , t.time==this.time; */ public void copy(CRequest t)
應當使用&&連接符連接多個條件，改為：
/** * 拷貝指令到t * @REQUIRES: this!=NULL && t!=NULL; * @MODIFIES: t.x,t.y,t.tx,t.ty,t.time; * @EFFECTS: * (t.x==this.x && t.y==this.y && t.tx==this.tx && t.ty==this.ty && t.time==this.time); */ public void copy(CRequest t)
4、
/** * 判斷(x1,y1)和(x2,y2)是否相連 * @MODIFIES: None; * @EFFECTS: * graph[x1*80+y1][x2*80+y2]==1 ==> \result==true; * !(graph[x1*80+y1][x2*80+y2]==1) ==> \result==false; */ public boolean isConnected(int x1,int y1,int x2,int y2)
遺漏某些條件，應當改為：
/** * 判斷(x1,y1)和(x2,y2)是否相連 * @MODIFIES: None; * @EFFECTS: * (x1>=0 && x1<80 && y1>=0 && y1<80 && x2>=0 && x2<80 && y2>=0 && y2<80 && graph[x1*80+y1][x2*80+y2]==1) ==> \result==true; * (!(x1>=0 && x1<80 && y1>=0 && y1<80 && x2>=0 && x2<80 && y2>=0 && y2<80 && graph[x1*80+y1][x2*80+y2]==1)) ==> \result==false; */ public boolean isConnected(int x1,int y1,int x2,int y2)
5、
/** * 將存儲在this.flows中有用的流量信息存儲到_flows中 * @REQUIRES: 0<=x<80 && 0<=y<80 && _flows!=NULL; * @MODIFIES: _flows; * @EFFECTS: * 有用的流量信息被存儲到_flows中； */ public synchronized void flows2flow(int x,int y, ArrayList<Flow> _flows)
盡量避免使用自然語言，應當改為：
/** * 將存儲在this.flows中有用的流量信息存儲到_flows中
* @REQUIRES: 0<=x<80 && 0<=y<80 && _flows!=NULL; * @MODIFIES: _flows; * @EFFECTS: * (\all int i;0<=i<flows.size; flows.get(i).from==x*80+y && (abs(flows.get(i).to-(x*80+y))==1 || abs(flows.get(i).to-(x*80+y))==80); _flows.contains(flows.get(i))==true ) */ public synchronized void flows2flow(int x,int y, ArrayList<Flow> _flows)
四、功能bug與規格bug在方法上的聚集關系
在最近三次作業中，沒有被報規格BUG，並且除了第10次作業，其余兩次作業沒有出現功能性BUG。
第十次作業中，被報的三個BUG均是由於一個獲取上一個500ms流量的方法在實現時出現了BUG。對於這個獲取流量的方法，由於可能出現多個出租車線程同時訪問，所以存在線程安全問題。我在設計時考慮了此問題，對此將其中對於地圖信息操作的部分加了鎖。可能是我的測試不夠充分，本地運行無誤的情況下，在互測同學運行時出現了錯誤。在後續的作業中，我采用了新的流量計算方法，解決了這個問題。
| 方法名 | 錯誤原因 | 功能BUG數 | 規格BUG數 | |
| OO10 | graph.getFlow(); | 對於線程安全問題考慮不全 | 3 | 0 |
對於這個出錯的方法，其JSF並不存在問題，但是我沒有按照JSF準確無誤的實現這個方法。這主要是由於先寫代碼，後補充規格的設計順序造成的。可以看到，規格在程序設計中是多麽重要！
五、感想體會
我認為課上對於規格的講解過於缺乏。以JSF為例，我們在一次課堂上能獲得的知識實在過於有限，而且大多是理論層面的，課上僅僅給出幾個簡單的例子，然後課下作業就要求我們將所有的方法都書寫JSF。我認為在這種情況下要將JSF寫好，並且真正起到正面作用是不可能的。課上給出的例子都是類似數值計算，標準的數據結構的操作等等容易使用邏輯表達式進行表達的例子。但是我們的作業是模擬出租車運行這種比較抽象的活動，對於我們來說其中存在太多太多不知道該怎麽表達的情況。舉個例子，一個將地圖文件轉化為圖的鄰接矩陣的方法，我應當如何表示鄰接矩陣中存儲了正確的文件中圖的信息呢？每個元素都是0或者1麽？但是每個元素都是0或者1也不能表達正確的圖的全部信息。再比如說如何表示向控制臺輸出某些信息？main()，run()這種方法運行起來之後沒有特殊情況不會停止的方法又應當如何表示後置條件呢？上述的幾個問題僅僅是完成作業中遇到問題的冰山一角。對於這些問題，連助教都無法做出統一有效的回復。由於給出的JSF標準中沒有這些情況的具體例子，我們無奈只能使用自然語言或者其他方法進行表達。讓規格應當起到的作用大打折扣。
如果情況至此結束倒還好，但更加令我無奈的是我們在沒有統一標準的情況下需要對其他同學的規格進行評測，並且可以拿到分數。這難道不是一種不公平麽？心狠手辣就可以拿到很高的分數，放寬標準就可能被別人狠宰一刀。這已經偏離了這門課的目的。
在課下作業已經結束之後的OO實驗課上我們才看到了規範合理的JSF，但是此時提交的作業已經無法修改，而且我認為OO實驗課上給出的JSF以及其對應的方法仍然是數值修改，標準數據結構操作之類十分容易進行邏輯表達的方法，與我們的作業情況仍是相距甚遠。我相信大多數同學對於OO實驗課上給出的JSF都能夠正確的寫出對應的方法，也能夠根據方法寫出規範的JSF。但是對於我們的作業，要做到一樣的程度實在是過於艱難。
種種問題導致我認為規格設計並不能起到課上宣傳的所謂積極作用，最起碼在我們的作業中看來是這樣。書寫規範成為了應付作業，敷衍了事，甚至因為可能被扣分而影響了正常的程序設計，成為了一個很大的負擔。我希望課程組能夠廣泛聽取同學們的意見，將OO課程越辦越好。
OO9~11次作業總結