OO_Unit3_JML規格模式

---恢復內容開始---

[CSDN博客連接](https://blog.csdn.net/weixin_43387647/article/details/90451173) @[toc] ## 1、JML語言的理論基礎及應用工具鏈 #### （一）定義： JML(Java Modeling Language)：對Java程序進行規格化設計的一種表示語言。JML是一種行爲接口規格語言 （Behavior Interface Specification Language，BISL），基於Larch方法構建。BISL提供了對方法和類型的規格定義 手段。所謂接口即一個方法或類型外部可見的內容。 #### （二）契約式設計核心思想： 軟件系統中的元素之間相互合做以及「**責任**」與「**義務**」 1. 指望全部調用它的客戶模塊都保證必定的進入條件：這就是函數的**先驗條件**—客戶的義務和供應商的權利，這樣它就不用去處理不知足先驗條件的狀況。 2. 保證退出時給出特定的屬性：這就是函數的**後驗條件**—供應商的義務，顯然也是客戶的權利。 3. 在進入時假定，並在退出時保持一些特定的屬性：**不變式**。

method A(){
   assert(前置條件)
  	do something
   assert(後置條件)
   return 
}

（三）特色：

1. 跳過方法的實現，直接描述方法的功能
2. 規範化的註釋，而且可以被自動檢測正確性

（四）用法：

具體使用詳見《JML Level 0手冊》

1. 開展規格化設計。這樣交給代碼實現人員的將不是可能帶有內在模糊性的天然語言描述，而是邏輯嚴格的規
   格。
2. 針對已有的代碼實現，書寫對應的規格，從而提升代碼的可維護性。這在遺留代碼的維護方面具備特別重要的意義。

（五）工具鏈：

1. 使用到IDEA的OpenJML插件，檢查JML是否符合規格gitHub下載地址
   openJML。
2. 使用JUnit生成測試樣例，進行單元化測試

2、部署SMT Solver並驗證

很遺憾，電腦不兼容openJML，按照教程嚴格執行，卻一直失敗：

1. 下載時出錯：
   
2. 配置時出錯：
   用IDEA導入包時不能識別

3、JMLUnitNG/JMLUnit自動生成測試用例

（一）對Edge類的hashCode進行測試

• 源碼：

public int hashCode() {
    int[] array = new int[3];
    array[0] = min;
    array[1] = max;
    array[2] = pathId;
    return Arrays.hashCode(array);
}

• 測試：

@Test
public void hashCodeTest() {
    assertNotEquals(new Edge(-69,54,1).hashCode(),
            new Edge(-68,23,1).hashCode());
    //Values should be different. Actual: -34843
    
    HashSet<Integer> set = new HashSet<>();
    for (int i = -50; i < 50; i++)
        for (int j = -50; j < 50; j++) {
            Edge edge = new Edge(i, j, 1);
            set.add(edge.hashCode());
        }
    assertEquals(set.size(), 5050);
    //java.lang.AssertionError: 
    //    Expected :2704
    //    Actual   :5050      i!=j: (100+1)*100/2
}

• 結果：發現此hashCode生成不能知足需求，使得兩個不一樣的邊hashCode的值不一樣
• hashCode與equals具備如下規範：
  1. 若重寫equals(Object obj)方法，有必要重寫hashcode()方法，確保經過equals(Object obj)方法判斷結果爲true的兩個對象具有相等的hashcode()返回值。
  2. 若是equals(Object obj)返回false，即兩個對象「不相同」，並不要求對這兩個對象調用hashcode()方法獲得兩個不相同的數。
  3. Java運行時環境是怎樣判斷HashSet和HastMap中的兩個對象相同或不一樣：先判斷hashcode是否相等，再判斷是否equals。
• 修正：
  反hash（但願創建一個hashCode到Edge自己一一對應的映射）的前提：任何兩個同類型不一樣的對象的哈希值不一樣

public int hashCode() {
    return (min + "," + max + "," + pathId).hashCode();
}

（二）針對Graph接口的測試用例

@Test
    public void getLeastTransferCountTest() {
        Path path = new MyPath(1,2,3);
        MyRailwaySystem system = new MyRailwaySystem();
        system.addPath(path);
        path = new MyPath(2,4,5,6);
        system.addPath(path);
        path = new MyPath(3,5);
        system.addPath(path);

        try {
            assertEquals(system.getLeastTransferCount(1,6),1);
            //java.lang.AssertionError: 
            //Expected :2
            //Actual   :1
        } catch (Exception e) {
            e.printStackTrace();
        }
    }

根聽說明信息，發如今dijstra更新過程當中出現錯誤，在bug修復處分析了具體緣由及解決方式。

4、架構設計

（一）類圖設計

本單元做業要求依次實現四個類：

• 使用Path接口的MyPath
• 使用PathContainer接口的MyPathContainer
• 使用Graph接口的MyGraph
• 使用RailwayStation接口的MyRailwayStation

其中，MyPathContainer是MyPath的容器，而且實現了MyGraph的部分功能。所以，MyGraph中以MyPathContainer做爲組成元素之一。同理，MyRailwayStation將MyGraph做爲組成元素之一。各種包含關係以下：

在後續迭代過程當中，不對前面實現過的類進行修改，僅是擴展添加新的屬性及方法（遵循OCP原則：面對需求，對程序的改動是經過增長新代碼進行的，而不是改變原來的代碼。）

（二）算法設計

本次做業比較關鍵的幾個方法爲：

1. MyPathContainer.getDistinctNodeCount()

• 不能在每次接到指令DISTINCT_NODE_COUNT時都從新計算一遍，所花的時間複雜度是不能承受的。最開始我就是直接遍歷，致使第一次強測爆40
• 須要有一個圖來存每個節點信息：

private HashMap<Integer, Integer> nmap = new HashMap<>();
//node的容器<node,number（node出如今各個路徑中的次數）>

• 每次加入或刪除路徑時對其更新
• 接到指令DISTINCT_NODE_COUNT時直接返回nmap.size();

2. MyGraph.getShortestPathLength(int fromNodeId, int toNodeId)

• 使用到BFS：一種單元擴張的搜索方式。其適用的前提是保證value嚴格遞增。
• 而且BFS的時間複雜度對單源是o(v+e)，對全圖搜索複雜度爲o(v(v+e))
• 須要有一個鄰接鏈表存儲點之間關聯關係（使用到鍵爲node，值爲邊集合的HashMap，所以還須要設一個創建從邊的hash值到邊自己的映射），一個距離矩陣來存儲距離信息：

private HashMap<Integer, HashSet<Integer>> linkMap;
private HashMap<Integer, HashMap<Integer, Integer>> disMap;
private HashMap<Integer, Edge> edgeMap;//hashCode(edge)-->edge(a,b)

• 其中距離矩陣是周密矩陣：第二次限制|node|<=250，第三次限制|node|<=120
• 此處存距離的disMap其實直接用矩陣存儲的時空效率更高
• 接下來是對單源距離圖的更新：須要fromSet, nextSet進行廣度優先搜索，每次將fromSet所鏈接而未到達的點放入nextSet，算法較爲簡單

3. MyRailwayStation.getLeastTicketPrice(int fromNodeId, int toNodeId)
   MyRailwayStation.getLeastTransferCount(int fromNodeId, int toNodeId)
   MyRailwayStation.getLeastUnpleasantValue(int fromNodeId, int toNodeId)

• 使用到dijstra方法：相似於最小生成樹，是BFS的升級版，應用到鄰接鏈表，其算法複雜度也是o(v+e)
• 用到的數據結構須要記錄到達的節點，以及將要到達的節點
• 設置新的數據結構Node，組成鏈表結構：是四元組<node(Integer),value(Integer),edge(Edge),next(Node)>
• 正在到達的節點arrived爲(next=null)的Node類型，將要到達的節點nextSet爲Node類型的鄰接鏈表，而且加入時按照value值遞增
• dijstra的過程以下：
  1. 初始化：nextSet=new Node(0,0,null);nextSet.add(new Node(node,0,null));
  2. 將nextSet的首節點移出設置爲arrived
  3. 遍歷arrived鏈接的全部邊並加入nextSet：for(Integer edgeHashCode: linkMap.get(arrive.getNode()))
  4. 根據arrived更新對應的最小單元圖
  5. 跳回第二步，直到nextSet爲空集
• 過後考慮到v=|node|<=120，而e=|edge|<=4000，實際上o(v^3)優於o(v(v+e))，使用floyed算法的效率要比dijstra效率高，事實也是如此，而且floyed算法要比dijstra簡便不少

（三）代碼複雜度分析

1. 依賴關係

Class	Cyclic	Dcy	Dcy*	Dpt	Dpt*
Edge	0	0	0	3	5
Main	2	2	6	2	3
MyGraph	2	3	6	1	3
MyGraphTest	0	0	0	0	0
MyPath	0	0	0	2	4
MyPathContainer	0	0	0	1	4
MyRailwaySystem	2	4	6	2	3
MyRailwaySystemTest	0	2	7	0	0
Node	0	1	1	1	4

均在正常範圍內

2. 方法複雜度（顯示超標）

Method	ev(G)	iv(G)	v(G)
MyGraph.isConnected(int,int)	4	2	5
MyGraph.nodeEdgeOk(int)	4	3	4
MyRailwaySystem.getLeast(int,int,int)	5	3	5
MyRailwaySystem.renewNodeMap(int,int)	3	13	14
Node.add(Node)	5	6	6

其中MyRailwaySystem.renewNodeMap方法，即對於單源的dijstra方法長50行，爲了兼容3個搜索，分支不少，而錯誤也正是出如今這裏。

之後任意一個方法，行數最好不要超過30行，秉承SRP（單一職責原則），只作出一個行爲，而後經過封裝和組合達到最終實現行爲的目的。

5、bug修復

（一）Edge類的hashCode錯誤

（前面已經測試過）

（二）換乘問題

• 要注意的是設有換乘，所以dijstra過程當中不可避免碰到了以下問題：
• 構造一個簡單的測試用例（前面進行了測試）
  
  若是嚴格按照以前的過程，會出現一個意想不到的問題：

1. 遍歷node=1，nextSet: (2,0,1/2)
2. 遍歷node=2, nextSet: (3,0,2/3)->(4,1,2/4)
3. 遍歷node=3, nextSet: (5,1,3/5)->(4,1,2/4)
4. 遍歷node=5, nextSet: (4,1,2/4)->(6,2,5/6) //->(4,2,4/5)
5. 遍歷node=4, nextSet: (6,2,5/6) //->(5,1,4/5)
6. 遍歷node=6, nextSet: null

最後發現node=6處value爲2，實際上value應該爲1

• 解決方式：
  • 在第4步，發現將要加入的(4,2,4/5)與(4,1,2/4)衝突（同node，同path，不一樣egde）時，加入較大者的新節點(5,1,4/5)，獲得nextSet: (5,1,4/5)->(4,1,2/4)->(6,2,5/6)
  • 第5步：遍歷node=5, nextSet: (4,1,2/4)->(6,1,5/6) （第二次遍歷，注意更新）
  • 第六、7步：同上五、6

（三）null指針

在HashMap數據結構中，若是訪問的key值不在其中，函數會返回null，而不是拋出異常，然後對null調用函數會報錯NullPointerException。所以在這裏經常出現詭異的bug，之後使用get時要當心，更好的方式是使用getOrDefault，沒有key值就給出默認的數據。

此外，對於HashMap套HashMap現象，連續使用兩次get()，會形成意想不到的錯誤，不如先將亂序節點經過一個HashMap映射到從1開始的正整數上，而後直接使用二維靜態數組。

6、心得體會

JML是一種先進的契約式設計模式，將設計和實現不可跨越的鴻溝大幅減少。大致上解決問題分爲從需求到設計，從設計到實現兩個過程。而JML規範地描述了代碼須要執行的約束條件，能夠說是一種LLR(Low-Level Request)。

實際上，我的感受JML更偏向於需求，而非設計。由於不論是你須要具體的數據結構，仍是算法，都須要我的親自去定義。而且爲了描述一個需求，用大段大段的代碼去規範和描述也不是一個簡單的任務。極可能須要多層抽象，甚至有時根本找不出一個描述需求的嚴格的表達方式。寫規格自己都要比實現一個需求難上許多。

可是比較受用的是自動測試生成JUnit，對類中的某一個具體的函數進行測試。雖然直接在控制檯輸入輸出也頗有效，但那樣測完一次就結束了，沒有辦法對測試集進行管理。也沒有辦法在擴展修改了類之後保證類的兼容性。

總之，這一個單元是至關革新的，業界缺少成熟的代碼規格化設計方式，網絡上對契約式設計也鮮有聽聞，可是之後可能會日漸成熟。

---恢復內容結束---