OO第三單元總結——JML

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

理論基礎：

JML(Java Modeling Language)是用於對Java程序進行規格化設計的一種表示語言。

1.註釋結構

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

2.JML表達式

2.1 原子表達式

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

\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.2 量化表達式

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

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

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

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

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

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

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

2.3 集合表達式

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

2.4 操做符

(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 。

(3) 推理操做符： b_expr1==>b_expr2 或者b_expr2<==b_expr1 。對於表達式b_expr1==>b_expr2 而言，當b_expr1==false ，或者b_expr1==true 且b_expr2==true 時，整個表達式的值爲true 。

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

3. 方法規格

前置條件(pre-condition)

前置條件經過requires子句來表示： requires P; 。其中requires是JML關鍵詞，表達的意思是「要求調用者確保P爲真」。注意，方法規格中能夠有多個requires子句，是並列關係，即調用者必須同時知足全部的並列子句要求。

後置條件(post-condition)

後置條件經過ensures子句來表示： ensures P; 。其中ensures是JML關鍵詞，表達的意思是「方法實現者確保方法執行返回結果必定知足謂詞P的要求，即確保P爲真」。一樣，方法規格中能夠有多個ensures子句，是並列關係，即方法實現者必須同時知足有所並列ensures子句的要求。

反作用範圍限定(side-effects)

反作用指方法在執行過程當中會修改對象的屬性數據或者類的靜態成員數據，從而給後續方法的執行帶來影響。從方法規格的角度，必需要明確給出反作用範圍。JML提供了反作用約束子句，使用關鍵詞assignable 或者modifiable 。從語法上來看，反作用約束子句共有兩種形態，一種不指明具體的變量，而是用JML關鍵詞來歸納；另外一種則是指明具體的變量列表。

正常功能行爲和異常行爲

public normal_behavior：正常行爲功能

public exceptional_behavior：異常行爲功能

signals子句

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

4. 類型規格

類型規格指針對Java程序中定義的數據類型所設計的限制規則，通常而言，就是指針對類或接口所設計的約束規則。

不變式invariant

不變式（invariant）是要求在全部可見狀態下都必須知足的特性，語法上定義invariant P ，其中invariant 爲關
鍵詞， P 爲謂詞。凡是會修改爲員變量（包括靜態成員變量和非靜態成員變量）的方法執行期間，對象的狀態都不是可見狀態。類型規格強調在任意可見狀態下都要知足不變式。

狀態變化約束constraint

對象的狀態在變化時每每也許知足一些約束，這種約束本質上也是一種不變式。JML爲了簡化使用規則，規定
invariant只針對可見狀態(即當下可見狀態)的取值進行約束，而是用constraint來對前序可見狀態和當前可見狀態的
關係進行約束。

應用工具：

openJML：能夠對代碼進行JML規格的語法的靜態檢查，還支持使用SMT Solver動態地檢查代碼對JML規格知足的狀況。

JMLUnitNG/JMLUnit：根據JML描述自動生成與之符合的測試樣例，重點會檢測邊界條件。

2、JMLUnitNG使用

先編寫測試類

// demo/Demo.java
package demo;

public class Demo {
    /*@ public normal_behaviour
      @ ensures \result == (a>b);
    */
    public static boolean compare(int a, int b) {
        return a>b;
    }

    public static void main(String[] args) {
        compare(111,222);
    }
}

安裝好openjml和jmlunitng

執行命令 jmlunitng demo/Demo.java 生成相應測試文件

編譯 javac -cp jmlunitng.jar demo/*.java  openjml -rac demo/Demo.java 

運行測試文件 java -cp jmlunitng.jar demo.Demo_JML_Test 

能夠看出，生成的測試數據都是邊界數據，這也符合工程測試的要求。

3、梳理架構設計，分析迭代中對架構的重構

第一次做業

類圖：

三個類，

Path類維護兩個數據成員

private ArrayList<Integer> nodes;　　
private HashMap<Integer, Integer> map;

nodes用來索引，存儲Path的節點序列，而map用來查看Path中是否包含某個節點以及統計Path不一樣節點的個數。

PathContainer類維護四個數據成員

private HashMap<Path, Integer> map1;
private HashMap<Integer, Path> map2;
private HashMap<Integer, Integer> mapnodes;
private static int pid = 0;

map1存儲鍵值對<Path,PathId>

map2存儲鍵值對<PathId,Path>

mapnodes存儲鍵值對<NodeId,該Node重複的次數>

靜態變量pid存當前最大PathId

containsPath(Path path),getPathId(Path path)使用成員map1查詢

containsPathId(int pathId),getPathById(int pathId)使用成員map2查詢

本次做業複雜度比較高且調用次數比較多的的指令是統計容器不一樣節點的個數，爲了防止tle，所以我選擇了把它分散到調用次數相對較少的方法（addPath,removePath,removePathById）中，這些方法都是改變該類成員屬性的。

添加或移除路徑時，須要給map一、map二、mapnodes添加或刪除或更新鍵值對。

在調用方法int getDistinctNodeCount()時，直接返回maonodes.size()便可，這樣即可極大的下降時間複雜度。

第二次做業

類圖：

此次做業在以前的基礎上新增了幾條指令：CONTAINS_NODE（容器中是否存在某個結點），CONTAINS_EDGE（容器中是否存在某一條邊），IS_NODE_CONNECTED（兩個結點是否連通），SHORTEST_PATH_LENGTH（兩個結點之間的最短路徑）。

對於新需求要作的變化：

很顯然前兩條指令可使用第一次做業的mapnodes來查詢。

涉及最短路徑的計算，因此須要構建一個圖的數據結構，相似於鄰接矩陣，我新增一個類GraphStructure

public class GraphStructure {
    private HashMap<Integer, HashMap<Integer, Integer>> edgeNum;
    private HashMap<Integer, HashMap<Integer, Integer>> minPathLength;
    private final int inf = 99999999;

    public GraphStructure() {
        edgeNum = new HashMap<>();
        minPathLength = new HashMap<>();
    }
    
    public void addVer(int nodeId) {}
    
    public void addEdge(int from, int to) {}

    public void removeEdge(int from, int to) {}

    public void removeVer(int nodeId) {}

    public boolean containsEdge(int fromNodeId, int toNodeId) {}

    public void floyd() {}

    public boolean isConnected(int fromNodeId, int toNodeId) {}

    public int getShortestPathLength(int fromNodeId, int toNodeId) {}

}

該類在MyGarph中被實例化一個對象。 

這個類維護一個圖結構edgeNum，採用雙層hashmap嵌套,存儲鍵值對<頂點i，Hashmap<頂點j，頂點i、j之間的邊數>>

每次添加或移除路徑時，調用該類的addVer()、addEdge()、removeVer()、removeEdge()方法來更新該類的圖結構，而後調用floyd（）來計算全部節點之間的最短路徑，將結果存到minPathLength中。

第三次做業

類圖

 

這次增長的指令是CONNECTED_BLOCK_COUNT（整個圖中的連通塊數量），LEAST_TICKET_PRICE（兩個結點之間的最低票價），LEAST_TRANSFER_COUNT（兩個結點之間的最少換乘次數），LEAST_UNPLEASANT_VALUE（兩個結點之間的最少不滿意度）。

對於新需求要作的變化：

對每一個指令添加一個類來實現相應的功能。

求解連通塊我採用的是並查集的方法。

剩下的三個因爲涉及到換乘，所以我借鑑討論區的方法，每種方法構造一個圖(在每條path中加邊，並添加能體現換乘的權重)，求此圖的最短路徑便可。求最短路徑採用的是Dijskra算法，將得到的一部分結果緩存到hashmap中，這樣帶來的好處能夠避免一些沒必要要的計算。

當添加或刪除路徑的時候，對這三個類直接從新new一個對象，而後根據容器類的path進行圖的構建。

分析：

這三次做業的迭代，每次都會添加一些新的功能，不過個人架構基本沒什麼變化，都能保證原有代碼不變，類之間的解耦作的很好，這樣對個人代碼維護起到了很大的做用。可是也有不足，就是第三次做業中類的整合作的不是很好，致使幾個類有一些重複代碼。

4、分析代碼實現的bug和修復狀況

第一次做業tle了幾個點，由於對Path類重寫hashcode()時過於複雜，複雜度爲O（n），直接返回path.size()便可修復。

第二次做業沒出現bug。

第三次做業出現大面積wa，發現原來是把Integer等同於int來對待了，直接用「==」致使只要測試點出現比較大的整數就有bug，瞭解到兩者區別，判斷Integer是否相等應該使用equals。

5、對規格撰寫和理解上的心得體會

規格和代碼是相互輔助的，藉助規格咱們能夠檢查代碼邏輯的正確性，還可使咱們的代碼更易被人理解。

規格對設計、實現、測試都是頗有用的工具。學會撰寫規格、利用規格來測試是頗有必要的。

實現代碼的時候不要被規格說明限制，例如path類中數據規格是int[]，可是實現時可使用ArrayList、Hashmap這些數據結構來下降相應方法的時間複雜度。

總之，JML這一單元讓我對面向對象有了新的思考和認識。