oo第三單元總結

一． 梳理JML語言的理論基礎、應用工具鏈狀況

JML(Java Modeling Language)是用於對Java程序進行規格化設計的一種表示語言。經過JML及其支持工具，不只能夠基於規格自動構造測試用例，並整合了SMT Solver等工具以靜態方式來檢查代碼實現對規格的知足狀況。

JML語言的理論基礎：

1. 註釋結構

JML以javadoc註釋的方式來表示規格，每行都以@起頭。有兩種註釋方式，行註釋和塊註釋。其中行註釋的表示方式爲//@annotation，塊註釋的方式爲/* @ annotation @*/。

2. JML表達式 （JML的表達式是對Java表達式的擴展，新增了一些操做符和原子表達式。）

(1).原子表達式:

\result表達式：表示一個非void類型的方法執行所得到的結果，即方法執行後的返回值。

\old(expr)表達式：用來表示一個表達式expr在相應方法執行前的取值。

\not_assigned(x,y,...)表達式：用來表示括號中的變量是否在方法執行過程當中被賦值。

\not_modified(x,y,...)表達式：與\not_assigned表達式相似。

\nonnullelements(container)表達式：表示container對象中存儲的對象不會有null。

\type(type)表達式：返回類型type對應的類型(Class)。

\typeof(expr)表達式：該表達式返回expr對應的準確類型。

(2).量化表達式:

\forall表達式：全稱量詞修飾的表達式。

\exists表達式：存在量詞修飾的表達式。

\sum表達式：返回給定範圍內的表達式的和。

\max表達式：返回給定範圍內的表達式的最大值。

\min表達式：返回給定範圍內的表達式的最小值。

\num_of表達式：返回指定變量中知足相應條件的取值個數。

(3).集合構造表達式：能夠在JML規格中構造一個局部的集合（容器），明確集合中能夠包含的元素。

(4).操做符:

子類型關係操做符：E1<:E2，若是類型E1是類型E2的子類型(sub type)，則該表達式的結果爲真，不然爲假。

等價關係操做符：b_expr1<==>b_expr2或者b_expr1<=!=>b_expr2，其中b_expr1和b_expr2都是布爾表達式，這兩個表達式的意思是b_expr1==b_expr2或者b_expr1!=b_expr2。

推理操做符：b_expr1==>b_expr2或者b_expr2<==b_expr1。

變量引用操做符：\nothing指示一個空集；\everything指示一個全集。

3. 方法規格

前置條件(requires)：對方法輸入參數的限制，若是不知足前置條件，方法執行結果不可預測，或者說不保證方法執行結果的正確性。

後置條件(ensures)：對方法執行結果的限制，若是執行結果知足後置條件，則表示方法執行正確，不然執行錯誤。

反作用(assignable或者modifiable)：方法在執行過程當中對輸入對象或this對象進行了修改.

4. 對數據規格的抽象：

不變式限制(invariant)。

約束限制(constraints)。

 JML語言的應用工具鏈狀況：

JML工具鏈

openjml：檢測JML註釋正確性，能夠自動識別和分析處理JML規格。

SMT Solver工具：以靜態方式來檢查代碼實現對規格的知足狀況。

 單元測試生成器jmlunit：能夠從JML註釋中生成JUnit測試代碼。

 

二．部署JMLUnitNG/JMLUnit，針對Graph接口的實現自動生成測試用例， 並結合規格對生成的測試用例和數據進行簡要分析

測試代碼以下：

 

 獲得的文件樹：

測試結果：

從Passed測試數據來看，自動測試選取了一些邊界條件進行測試，經過自動測試，基本能夠認爲代碼符合規格。

 

三．按照做業梳理本身的架構設計，並特別分析迭代中對架構的重構

1.第一次做業：實現一個路徑管理系統，能夠經過各種輸入指令來進行數據的增刪查改等交互。

第一次做業由於須要求出容器內不一樣結點個數，而那時候沒有了解hashset，hashmap，一直用的是ArrayList，當每次求容器內不一樣結點個數，採用了快排，而後在計算不一樣結點的算法，沒有進行充分的測試，致使強測沒過。聽同窗講思路分析後，重構了此次做業的架構。

重構後的架構以下：

MyPath類除了記錄結點的容器（ArrayList）nodes外，還使用了一個容器（HashSet）distinctode用於記錄不一樣結點，這樣distinctnode.size就表示了MyPath裏面不一樣結點的個數了。MyPathContainer類中使用了三個容器，一個是記錄所有Path的容器（ArrayList），一個是記錄Path序號的容器（ArrayList）,還有一個記錄所有Path的全部不一樣結點的HashMap容器，鍵值爲結點，value爲結點的數量，當有新的Path進入或者刪除Path時，只需取出該結點對應的value，對value進行操做便可。

2. 第二次做業：在第一次做業的基礎上，實現一個無向圖系統。

架構以下：

第二次做業相對第一次做業，只須要多實現containsNode(), containsEdge(), isConnected(), getShortestPathLength()四個方法。在第一次做業的基礎上，增長了兩個類，Dijkstra和Edge類，MyGraph增長一個容器(HashMap，key爲Edge,value爲equal key的數量)edges在每次增長或者刪除Path時，只需作到和distinctnode相同的操做便可，先判斷，而後決定是否改變value，containsNode(), containsEdge()只需用上面的算法便可實現，isConnected(), getShortestPathLength()兩個方法主要與Dijkstra類有關，由於考慮到時間複雜度，採用迪傑斯特拉算法，而且保存中間已經算出的距離，當沒有增長或者刪除的操做，若已經在前面算出了距離，下次須要用時直接返回就行；當有增長或者刪除的操做時，就須要改變整張圖，須要從新計算。

 3. 第三次做業：實現一個簡單地鐵系統。

架構以下：

第三次做業相對於第二次做業主要是多了四個問題，連通塊，LeastTransfer（最少換乘次數），LeastPrice（最少票價），LeastUnpleasantValue（最小不滿意度）的問題，其他與第二次做業一致，連通塊和最少換乘次數是基於一個圖操做的，即建一個圖把每個條路徑上全部相連的點都記錄下來，且相連點之間的距離均爲1，使用迪傑斯特拉算法求兩點之間的距離時就是求出最少換乘次數，經過廣度優先算法，便可求出連通塊數量；LeastPrice（最少票價），LeastUnpleasantValue（最小不滿意度）這兩個問題基於添加結點解決，將全部在兩條Path中出現的結點一分爲二，兩個點之間距離爲轉乘票價或者轉乘的不滿意度，只需這樣，而後採用迪傑斯特拉算法算出最小值便可。

 

四．按照做業分析代碼實現的bug和修復狀況

第一次由於架構的問題，致使強測超時，沒有進入互測，除了重構外，還發現了一個bug，經過ArrayList存數據時，取出來的並非該數據，而是Integer對象。

第二次互測時被找出了一個bug，以前是當起點與終點相同時，沒有將該邊加入邊的容器中，致使告終果的錯誤。

第三次做業由於優化不夠的問題，致使了強測中兩個點沒有過，修復時作了一些優化，由於是迪傑斯特拉算法，因此當知道起點和終點時，能夠計算起點到終點，也能夠計算終點到起點，找中間計算結果時能夠找兩次後再進行更新，這樣，應該能節省一點時間。

 

五．闡述對規格撰寫和理解上的心得體會

使用規格能將一個問題講清楚，能將一個方法描述清楚，只不過由於這樣，規格寫起來可能會比天然語言表達更加繁雜；

經過規格也能進行自動化測試，可以使本身寫的代碼更加可靠，之前只能對一個類進行測試，經過規格測試工具可以對一個方法進行測試，這樣，之後出現bug的機率也變小了；

經過規格，也能使一個方法作一件事，若是將全部事都交給一個方法來實現，規格將會變得很是複雜；

規格也能將設計與實現分離開，各作各的，不容易產生錯誤。