面向對象程序設計第三單元總結

概述

本單元主要學習規格化的面向對象設計方法，即便用行爲接口規格語言JML(Java Modeling Language)對Java程序進行規格化設計。其中咱們在課上實驗上簡要嘗試了使用JML描述方法規格，課下做業主要是閱讀已有框架和規格，而後按照規格編寫方法完成程序。

JML語言

1.註釋結構

JML以javadoc註釋的方式表示規格，每行以@開頭。有兩種註釋方式：

//行註釋
//@annotation


//塊註釋
/*@ annotation @*/

2.JML表達式

2.1原子表達式

\result表達式：表示非void類型方法執行後的返回值。

\old(expr)表達式：用來表示一個表達式expr在相應方法執行前的取值。任何狀況下，都應該使用\old把關心的表達式取值總體括起來，不然僅僅表示引用的地址是否發生變化，而不會表示引用的對象實體內是否發生變化。

\not_assigned(x,y,...)表達式：用來表示括號中的變量是否在方法執行過程當中被賦值。實際上，該表達式主要用於後置條件的約束表示上，即限制一個方法的實現不能對列表中的變量進行賦值。

\not_modified(x,y,...)表達式：與上面的\not_assigned表達式相似，該表達式限制括號中的變量在方法執行期間的取值未發生變化。

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

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

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

2.2量化表達式

\forall表達式：全稱量詞修飾的表達式，表示對於給定範圍內的元素，每一個元素都知足相應的約束。

\exists表達式：存在量詞修飾的表達式，表示對於給定範圍內的元素，存在某個元素知足相應的約束。

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

\product表達式：返回給定範圍內的表達式的連乘結果。

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

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

\num_of表達式：返回指定變量中知足相應條件的取值個數。通常的，\num_of表達式能夠寫成(\num_of T x;R(x);P(x))，其中T爲變量x的類型，R(x)爲x的取值範圍;P(x)定義了x須要知足的約束條件。

2.3集合表達式

集合構造表達式：能夠在JML規格中構造一個局部的集合（容器），明確集合中能夠包含的元素。集合構造表達式的通常形式爲：new ST{T x| R(x) && P(x)}，其中R(x)對應集合中x的範圍，一般是來自某個既有集合中的元素。P(x)對應x取值的約束。

2.4操做符

JML表達式中能夠正常使用java語言所定義的操做符，包括算術操做符、邏輯預算操做符等。此外，JML專門又定義了以下四類操做符：

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

（2）等價關係操做符：b_expr1 <==> b_expr2或者b_expr1 <=!=> b_expr2，其中b_expr1和b_expr2都是布爾表達式，這兩個表達式的意思是b_expr1 == b_expr2或者b_expr1 != b_expr2。這兩個表達式和java重的==和!=有相同的效果，按照JML語言定義，<==>比==優先級低，<=!=>比!=優先級低。

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

（4）變量引用操做符：除了能夠直接引用java代碼或者JML規格定義的變量外，JML還提供了幾個歸納性的關鍵詞來應用相關的變量。\nothing表示一個空集；\everything表示一個全集，即包括當前做用域下可以訪問到的全部變量。

3.方法規格

方法規格的核心內容包括：前置條件、後置條件和反作用約定。

區分兩類方法：所有過程和局部過程。前者對應着前置條件恆爲真，便可以適應於任意調用場景；後者則提供了非恆真的前置條件，要求調用者必須確保調用時知足相應的前置條件。

區分兩種調用場景：正常行爲規格(normal_behavior)和異常行爲規格(exceptional_ behavior)。

（1）前置條件(pre-condition)：前置條件是對方法輸入參數的限制，若是不知足前置條件，方法執行結果不可預測，或者說不保證方法執行結果的正確性。經過requires子句來表示：requires P，requires是JML關鍵詞，表示調用者確保P爲真。方法規格中的多個requires子句爲並列關係，即調用者必須同時知足全部的並列requires要求。若是想表達或邏輯，則應該使用requires P1 || P2

（2）後置條件(post-condition)：後置條件是對方法執行結果的限制，若是執行結果知足後置條件，則表示方法執行正確，不然執行錯誤。經過ensures子句表示：ensures P，ensures是JML關鍵詞，表示方法實現者必須確保方法執行返回結果確保P爲真。方法規格中的多個ensures子句爲並列關係，即方法實現者必須同時知足全部的並列ensures要求。若是想表達或邏輯，則應使用ensures P1 || P2。

（3）反作用範圍限定(side-effects)：反作用指方法在執行過程當中對輸入對象或this對象進行了修改（對其成員變量進行了賦值，或者調用其修改方法），即方法在執行過程當中會修改對象的屬性數據或者類的靜態成員數據，從而給後續方法的執行帶來影響，因此必須明確給出反作用範圍。JML使用assignable或者modifiable關鍵詞來表示反作用的約束子句。

方法規格中還有一個關鍵詞also，有兩種使用also的場景：

（1）父類中對相應方法定義了規格，子類重寫了該方法，須要補充規格，這時需在補充的規格以前使用also

（2）一個方法規格中涉及多個功能規格描述，正常功能規格或者異常功能規格，須要使用also

方法規格還包含signals子句，其結構爲signals (Exception e) b_expr，意思是當b_expr爲true時，方法會拋出括號中給出的相應異常e。

 

4.類型規格

 類型規格指針對java程序中定義的數據類型所設計的限制規則，通常說是指針對類或接口所設計的約束規則。JML主要設計兩類限制規則，不變式限制(invariant)和約束顯示(constraints)。類型規格都是針對類型中定義的數據成員所定義的限制規則。

（1）不變式(invariant)：不變式是要求在全部可見狀態下都必須知足的特性，語法定義爲invariant P,其中invariant爲關鍵詞，P爲謂詞。可見狀態(visible state)有：

①對象的有狀態構造方法(用來初始化對象成員變量初值)的執行結束時刻

②在調用一個對象回收方法(finalize方法)來釋放相關資源開始的時刻

③在調用對象o的非靜態、有狀態方法(non-helper)的開始和結束時刻

④在調用對象o對應的類或父類的靜態、有狀態方法的開始和結束時刻

⑤在未處於對象o的構造方法、回收方法、非靜態方法被調用過程當中的任意時刻

⑥在未處於對象o對應類或者父類的靜態方法被調用過程當中的任意時刻

由上可看出，凡是回修改爲員變量的方法執行期間，對象的狀態都不是可見狀態。

JML區分兩種不變式：①靜態不變式(static invariant)針對類中的靜態成員變量取值進行約束②實例不變式(instance invariant)針對靜態成員變量和非靜態成員變量的取值進行約束。

（2）狀態變化約束(constraint)：對象的狀態在變化時也會知足一些約束，用constraint來對前序可見狀態和當前可見狀態的關係進行約束。JML也區分了兩類約束：①static constraint：指涉及類的靜態成員變量②instance constraint：涉及類的靜態成員變量和非靜態成員變量。

JML應用工具鏈狀況

JML語言的工具鏈目前有不少，比較經常使用的是有，OpenJML能夠用來檢查JML的規範性，JMLUnitNG能夠用來自動化生成測試數據，SMTSolver能夠用來檢查代碼等價性。

 

三次做業分析

第一次做業

架構分析

實現細節

本次做業因爲是繼承官方接口，因此方法和接口一致，可是實現細節上，MyPath類利用了ArrayList存路徑的點，用HashMap記錄一條Path中不一樣的點。MyContainer類利用兩個HashMap構造了Path和PathId之間的雙映射，便於path和pathId之間的互相查詢，值得注意的是在利用path做爲HashMap的索引時，要重寫MyPath類的HashCode方法。而後還構建了一個HashMap用來存Container中不一樣的結點。因爲做業輸入的指令絕大多數是查詢指令，因此我在每次add和remove時更新要查詢的數據，例如不一樣結點數，而後每次查詢時直接返回結果，而不用從新計算一遍，這樣就極大下降了時間複雜度。

BUG分析

因爲此次做業比較簡單，在強測和互測中都未出現BUG。

第二次做業

架構分析

實現細節

第二次做業在第一次做業的基礎上，增長了圖的結構及和圖有關的計算等要求。實現細節上，MyPath類和第一次做業沒有任何變化。MyGraph類在MyContainer類的基礎上，加入了圖的結構相關的屬性和方法。因爲我是採用通常的二維數組的鄰接矩陣來存圖而不是鄰接表來存圖，而結點的值在Int範圍以內，不能做爲數組的下標，因此我構造了一個HashMap來表示結點和結點序號即數組下標之間的映射，並維護了一個Stack來存儲當前可用的結點序號即數組下標。而後因爲要實現圖的結點間的最短路徑的查詢，我還創建了一個distance二維矩陣來存儲每兩個結點之間的最短路徑。同第一次做業同樣，此次做業也是查詢指令佔絕大多數，我在第一次做業add和remove的更改中，新添加了對於圖和結點間的最短路徑的更新，對於圖的更新就是更新結點下標和鄰接矩陣，更新結點間的最短路徑就是經過bfs得到所有結點的最短路徑而後記錄下來。

BUG分析

此次做業雖然比第一次做業增長了有關圖的相關運算，難度增長了一點，可是強測和互測依然沒有被找出BUG。可是在完成做業時，本身找出了幾個BUG，一個是在判斷兩個點之間是否有邊時忘記判斷這兩個點是否存在於圖中。另外一個是bfs時，忘記初始化距離矩陣，這就形成每次bfs都是在上一次的結果的基礎上遍歷的，會形成remove一條path以後，查詢以前存在的而更新後不存在的結點間的距離時出錯。

第三次做業

架構分析

 

實現細節

第三次做業在第二次做業的基礎上，要求實現一個地鐵系統的管理，並計算和地鐵相關的最短換乘次數、最少票價和最少不滿意度，實際上這三種計算都是最短路問題。在計算這些最短路時，我採起了不拆點的方法，但這要求在通常權重矩陣的基礎上增長每兩個點之間的權重，因此在MyPath類中，我把每一條Path都創建成了圖，並經過Floyd算法求path內部的最少票價和最少不滿意度，並用HashMap存儲，當作外部訪問的接口。而後MyRailwaySystem中，新增長了兩個結點之間的最短換乘次數、最少票價和最少不滿意度的存儲矩陣以及對應的權重矩陣。而後在MyGraph的基礎上，在每次add和remove時，更新最短換乘次數、最少票價和最少不滿意度的權重矩陣，而後再利用Floyd求出對應的結果便可。

BUG分析

本次做業雖然在第二次做業的基礎難度又上了一個臺階，可是在強測和互測上依然沒有發現BUG。然而在寫做業時，本身測試發現了三個BUG，是在計算最少票價、最少換乘次數和最少不滿意度時沒有判斷兩個結點相同時的狀況致使出錯。

感想體會

經過本單元的學習，我體會到了JML的好處，就是在進行代碼架構的時候，對每一個類和每個方法進行約束，考慮正常和異常的狀況，這樣在撰寫代碼的時候，只要JML設計合理，在代碼能正確完成JML的要求後，工程的正確性和穩定性能獲得極高保障。