第三單元JML地鐵系統博客 By Wazaki

時間 2019-11-19

標籤第三單元 jml 地鐵系統博客 wazaki 简体版

原文原文鏈接

第三單元JML地鐵系統博客

第三單元JML地鐵系統博客寫在前面1、JML基礎理論2、設計思路與架構第一次做業第二次做業第三次做業架構總結3、測試與bug狀況Junit單元測試嘗試使用OpenJML與JMLuniting進行自動測試關於debug4、總結與體會html

寫在前面

　　在近三週，咱們進入了面向對象程序設計第三單元（根據JML編寫地鐵系統）。在本單元，咱們首次接觸了基於JML的規格模式的編程。規格化編程的核心是抽象，規格化的抽象是將用戶的需求（函數功能）抽象出來，隱藏具體的實現細節。這是一種很是工程化的編程思想和方法，方便進行形式化的驗證。node

　　第三單元做業圍繞Path相關的容器，從PathContainer 到 Graph 到 RailwaySystem，增量式設計，很是考驗代碼的構架好壞，而且對數據結構要求很高，須要咱們進行數據結構的抽象，運用繼承與接口實現代碼的擴展，而且使用相關工具測試進行驗證。下面我將梳理JML語言的基礎理論，再介紹中的思路與代碼架構，再介紹本單元JMLUnit進行測試狀況，最後總結心得體會。web

1、JML基礎理論

　　JML是一種行爲接口規範語言，可用於指定Java模塊的行爲。它是結合了契約方法設計和Larch系列接口規範語言的規範方法。經過使用JML，咱們能夠進行規格化的設計，代碼實現人員的將不是可能帶有內在模糊性的天然語言描述，而是邏輯嚴格的規格。能夠提升代碼的可維護性，使用各類工具進行自動測試及檢測。算法

　　使用JML進行規格化設計，是以類爲基本單位的，即用戶通常把類做爲一個總體來使用或重用。類的規格由數據規格與方法規格構成。數據規格規定了類所管理的數據內容，及其有效性條件；方法規格規定了類所提供的操做。開發人員必須確保實現數據內容始終有效，而且任何方法都知足方法自己所定義的規約且不能破壞數據的有效性。編程

　　對於數據來講，只需給出類所管理數據的最簡單表達，並知足有效性條件，其中包括invariant：任什麼時候刻數據內容都必須知足的約束條件；constraint：任什麼時候刻對數據內容的修改都必須知足的約束條件。windows

　　對於方法來講，用戶有義務保證提供有效的輸入以及有效的對象狀態，通過方法的執行用戶可以得到知足肯定條件的輸出結果。方法執行過程當中可能會修改用戶對象的狀態。對於方法的實現者來講規約由前置條件+後置條件+反作用組成。前置條件（requires）是實現者可依賴的初始條件，後置條件（ensures）是實現者要提供知足要求的結果，反作用（assignable）是方法執行過程當中可能帶來的變化。設計模式

　　對於類來講，對於JML的契約，類提供者信任使用者可以確保全部方法的前置條件都能被知足；類使用者信任設計者可以有效管理相應的數據和訪問安全。任何一個類都要可以存儲和管理規格所定義的數據，始終保持對象的有效性。類能夠拒絕爲選擇本身的表示對象而不受外部約束，拒絕爲不知足前置條件的輸入提供服務。緩存

　　從用戶的角度來看，一個設計優良的類應保證操做的完整性（構造、更新、查詢和生成），不提供與所管理數據無關的操做行爲。而且可以以簡單的方式訪問和更新所管理的數據，保證數據（線程）安全，最重要的是類的實現與JML規定徹底一致。安全

　　這種規格化的設計，致力於保證程序正確性的方法，即在規定的輸入範疇內給出知足規定要求的輸出。其基礎就是規格知足需求，實現知足規格。爲此咱們使用基於JML 的規格模式，以規約邏輯對數據進行條件約束，不關心具體數據結構和實現方式。普遍採用層次化設計和組合機制，其核心是數據的抽象。數據結構

　　同時基於JML規格的設計也爲咱們提供了不少工具，好比使用OpenJML檢查JML規範；使用JMLuniting進行自動測試等等一系列方法，是咱們驗證代碼的有力武器。

2、設計思路與架構

　　經過閱讀JML 規格能夠發現本單元做業是在經過path（路徑）創建graph（圖），在實現基本操做（增、刪、改、查）的基礎上，進而進行不一樣應用（RailwaySystem地鐵系統，帶權最短路徑查詢）

　　本單元做業從PathContainer 到 Graph 到 RailwaySystem逐漸繼承，須要良好的構架以支持增量式設計，下面我將介紹我在三次做業中構架的遞進過程。

第一次做業

　　第一次做業中，PathContainer是對路徑集合Path的封裝容器，主要進行Path的增長與刪除操做，每一條Path與一個固定的PathId對應，而且要記錄PathContainer中的全部結點。因此咱們須要創建Path與PathID之間的映射，存儲存儲全部節點。爲此我構造瞭如下兩個數據結構。

　　Dmap，裏面存儲了兩個map，分別爲PathId到Path和Path到PathId的映射。

1 private Map<K, Way> kmap = new HashMap<>();
2 private Map<V, Way> vmap = new HashMap<>();

　　CountSet是一個有引用計數的Set，裏面存儲全部節點號及引用次數（在多少條Path中出現）

 1 public class CountSet {
 2 
 3     private Map<Integer, Integer> nodeSet = new HashMap<>();
 4 
 5     public int size() {
 6         return nodeSet.size();
 7     }
 8 
 9     public void add(int node) {
10         if (nodeSet.containsKey(node)) {
11             int count = nodeSet.get(node);
12             nodeSet.remove(node);
13             nodeSet.put(node, ++count);
14         } else {
15             nodeSet.put(node, 1);
16         }
17     }
18 
19     public void remove(int node) {
20         int count = nodeSet.get(node);
21         if (count > 1) {
22             count--;
23             nodeSet.remove(node);
24             nodeSet.put(node, count);
25         } else if (count == 1) {
26             nodeSet.remove(node);
27         }
28     }
29 
30 }

第二次做業

　　第二次做業中，Graph是一個圖結構，要進行圖中結點和邊是否存在，結點是否相連，節點間最短路徑的計算。

　　我第二次做業中MyGraph類繼承於第一次做業中的MyPathContainer，並實現Graph接口

　　其中包含一個UndirGraph類的實例，這個類是無向圖結構，存儲全部與圖有關的信息，其中具備LinkMat和disMat這兩個實例，分別對應鄰接矩陣和距離矩陣。包含的主要方法是實現對節點和邊的增、刪、改、查與連通性、最短路徑的計算。linkMat存儲着圖的連通管理，disMat存儲着圖節點與節點間的最短路徑長度（緩存，O(1)查詢）

　　linkMat和disMat是Matrix類的實例，Matrix類當中封裝了一個雙HaspMap的結構，即Map<Integer,Map<Integer,Integer>>，並實現對此結構的相關操做。

　　第二次做業中，最複雜的一個方法是對最短路徑的計算。因爲是無權圖，因此我選擇了BFS算法（雖然起名字叫Dijk）進行實現，比較簡潔。

 1 private Map<Integer, Integer> singleDijk(int source) {
 2         Map<Integer, Integer> map = new HashMap<>();
 3         for (Integer i : linkMat.getEleList()) {
 4             map.put(i, max);
 5         }
 6         Queue<Integer> queue = new LinkedList<>();
 7         map.put(source, 0);
 8         queue.offer(source);
 9         while (!queue.isEmpty()) {
10             Integer top = queue.poll();
11             for (Integer t : linkMat.getListOfA(top)) {
12                 if (map.get(t) == max) {
13                     map.put(t, map.get(top) + 1);
14                     queue.offer(t);
15                 }
16             }
17         }
18         return map;
19     }

第三次做業

　　第三次做業中，要實現一個RailwaySystem地鐵系統，要支持多種標準（LeastTicketPrice、LeastTransferCount、LeastUnpleasantValue）的最短線路查詢。分析這次做業，地鐵系統實質上仍是圖結構，而且是有權圖，對於每種查詢標準，給予不一樣的不一樣的權值，進行有權最短路徑的計算。

　　本次做業，個人MyRailwaySystem繼承上次做業的MyGraph，進一步再創建三種不一樣標準的有權圖。

　　由於要考慮換乘問題，因此在不一樣地鐵線路上的同名結點可看作不一樣結點。因此每一個結點應包括結點id和路徑id兩個信息。因此我封裝了Node（只有nodeid）和RailwayNode（nodeid和pathid）兩個類代替以前的Integer（nodeid信息）

　　我構建RailwayGraph類繼承無權圖UndirGraph類，實現對地鐵圖的構建（改造），由於拆點的緣由，咱們須要在地鐵圖中重寫addPath和removePath創建同名節點的聯繫，而且創建虛擬入口與出口，再實現帶全路徑的計算。

　　三種不一樣標準的地鐵圖，繼承RailwayGraph類，並重寫其中的路徑權重和換乘權重，以下圖所示。

　　最後考慮最短路徑的算法，我使用了堆優化的迪傑斯特拉算法，以下圖所示。

 1 public void calSingleShortPathLengthOfGraph(Node source) {
 2         disMat.setLine(source, singleDijk(source));
 3         modified.remove(source);
 4     }
 5 
 6     private Map<Node, Integer> singleDijk(Node source) {
 7         Map<Node, Integer> map = new HashMap<>();
 8         Set<Node> visited = new HashSet<>();
 9         class NodeDistance implements Comparable<NodeDistance> {
10 
11             private final Node node;
12             private final int distance;
13 
14             private NodeDistance(Node node, int distance) {
15                 this.node = node;
16                 this.distance = distance;
17             }
18 
19             @Override
20             public int compareTo(NodeDistance o) {
21                 return Integer.compare(this.distance, o.distance);
22             }
23 
24             public Node getNode() {
25                 return this.node;
26             }
27 
28         }
29 
30         for (Node i : nodeList) {
31             map.put(i, max);
32         }
33         PriorityQueue<NodeDistance> queue = new PriorityQueue<>();
34         map.put(source, 0);
35         queue.offer(new NodeDistance(source, map.get(source)));
36         while (!queue.isEmpty()) {
37             Node top = queue.poll().getNode();
38             if (visited.contains(top)) {
39                 continue;
40             }
41             visited.add(top);
42             if (top instanceof RailwayNode) {
43                 if (((RailwayNode) top).getPathid() == Integer.MAX_VALUE) {
44                     continue;
45                 }
46             }
47             for (Node t : linkMat.getListOfA(top)) {
48                 if (!visited.contains(t) &&
49                         map.get(t) > map.get(top) + weightMat.get(top, t)) {
50                     map.put(t, map.get(top) + weightMat.get(top, t));
51                     if (!visited.contains(t)) {
52                         queue.offer(new NodeDistance(t, map.get(t)));
53                     }
54                 }
55             }
56         }
57         return map;
58     }

架構總結

　　整體來講，個人三次做業基本知足增量式的設計模式，不斷擴展與繼承。PathContainer <-- Graph <-- RailwaySystem，UndirGraph<--RailwayGraph<--priceGraph/transferGraph/satisfactionGraph。而且我對一些數據結構（Dmap，CountSet，Matrix）進行了封裝，使每一個類的功能更加明確，架構更爲清晰。

　　可是我每次在架構的設計當中，是存在考慮不足的問題，好比設計爲無向圖而非有向圖，一開始沒考慮權重，最短路徑算法的選擇等等都是等下一次做業的需求出現才作更改的，沒有預先設計好。而且，個人擴展比較硬性，沒有運用不少能夠複用的中間變量，好比說最後一次做業中的三個新圖的鄰接矩陣應該是相同的，只有權重矩陣不一樣，但我構建了三遍，形成了一些冗雜，拖慢了一些運行的效率。我認爲通過OO面向對象課程的學習，我面向對象的思想和代碼構架能力有了必定的提升，但考慮還不夠全面，須要進一步提升和細節上的優化。下面是我整個單元做業的價格UML圖。

3、測試與bug狀況

Junit單元測試

　　在本單元，我還聯繫使用了junit進行單元測試，在每一單元對新增模塊編寫了junit單元測試數據。

嘗試使用OpenJML與JMLuniting進行自動測試

　　我寫了兩個簡單方法的JML及其實現，分別爲是計算兩個數中比基礎值大的數的個數。練習使用OpenJML與JMLuniting配合進行測試。

方法以下：

 1 /*@ public normal_behaviour
 2       @ ensures (first > base) && (second > base) ==> (\result == 2);
 3       @ ensures (first > base) && (second <= base) ==> (\result == 1);
 4       @ ensures (first <= base) && (second > base) ==> (\result == 1);
 5       @ ensures (first <= base) && (second <= base) ==> (\result == 0);
 6     */
 7     public static int countBigger(int base, int first, int second) {
 8         int result = 0;
 9         if (first > base) {
10             result++;
11         }
12         if (second > base) {
13             result++;
14         }
15         return result;
16     }
17 
18     /*@ public normal_behaviour
19       @ ensures (first >= base) && (second >= base) ==> (\result == 0);
20       @ ensures (first >= base) && (second < base) ==> (\result == 1);
21       @ ensures (first < base) && (second >= base) ==> (\result == 1);
22       @ ensures (first < base) && (second < base) ==> (\result == 2);
23     */
24     public static int countSmaller(int base, int first, int second) {
25         int result = 0;
26         if (first < base) {
27             result++;
28         }
29         if (second < base) {
30             result++;
31         }
32         return result;
33     }

測試結果以下：

 1 [TestNG] Running:
 2   Command line suite
 3 
 4 Failed: racEnabled()
 5 Passed: constructor Demo()
 6 Passed: static countBigger(-2147483648, -2147483648, -2147483648)
 7 Passed: static countBigger(0, -2147483648, -2147483648)
 8 Passed: static countBigger(2147483647, -2147483648, -2147483648)
 9 Passed: static countBigger(-2147483648, 0, -2147483648)
10 Passed: static countBigger(0, 0, -2147483648)
11 Passed: static countBigger(2147483647, 0, -2147483648)
12 Passed: static countBigger(-2147483648, 2147483647, -2147483648)
13 Passed: static countBigger(0, 2147483647, -2147483648)
14 Passed: static countBigger(2147483647, 2147483647, -2147483648)
15 Passed: static countBigger(-2147483648, -2147483648, 0)
16 Passed: static countBigger(0, -2147483648, 0)
17 Passed: static countBigger(2147483647, -2147483648, 0)
18 Passed: static countBigger(-2147483648, 0, 0)
19 Passed: static countBigger(0, 0, 0)
20 Passed: static countBigger(2147483647, 0, 0)
21 Passed: static countBigger(-2147483648, 2147483647, 0)
22 Passed: static countBigger(0, 2147483647, 0)
23 Passed: static countBigger(2147483647, 2147483647, 0)
24 Passed: static countBigger(-2147483648, -2147483648, 2147483647)
25 Passed: static countBigger(0, -2147483648, 2147483647)
26 Passed: static countBigger(2147483647, -2147483648, 2147483647)
27 Passed: static countBigger(-2147483648, 0, 2147483647)
28 Passed: static countBigger(0, 0, 2147483647)
29 Passed: static countBigger(2147483647, 0, 2147483647)
30 Passed: static countBigger(-2147483648, 2147483647, 2147483647)
31 Passed: static countBigger(0, 2147483647, 2147483647)
32 Passed: static countBigger(2147483647, 2147483647, 2147483647)
33 Passed: static countSmaller(-2147483648, -2147483648, -2147483648)
34 Passed: static countSmaller(0, -2147483648, -2147483648)
35 Passed: static countSmaller(2147483647, -2147483648, -2147483648)
36 Passed: static countSmaller(-2147483648, 0, -2147483648)
37 Passed: static countSmaller(0, 0, -2147483648)
38 Passed: static countSmaller(2147483647, 0, -2147483648)
39 Passed: static countSmaller(-2147483648, 2147483647, -2147483648)
40 Passed: static countSmaller(0, 2147483647, -2147483648)
41 Passed: static countSmaller(2147483647, 2147483647, -2147483648)
42 Passed: static countSmaller(-2147483648, -2147483648, 0)
43 Passed: static countSmaller(0, -2147483648, 0)
44 Passed: static countSmaller(2147483647, -2147483648, 0)
45 Passed: static countSmaller(-2147483648, 0, 0)
46 Passed: static countSmaller(0, 0, 0)
47 Passed: static countSmaller(2147483647, 0, 0)
48 Passed: static countSmaller(-2147483648, 2147483647, 0)
49 Passed: static countSmaller(0, 2147483647, 0)
50 Passed: static countSmaller(2147483647, 2147483647, 0)
51 Passed: static countSmaller(-2147483648, -2147483648, 2147483647)
52 Passed: static countSmaller(0, -2147483648, 2147483647)
53 Passed: static countSmaller(2147483647, -2147483648, 2147483647)
54 Passed: static countSmaller(-2147483648, 0, 2147483647)
55 Passed: static countSmaller(0, 0, 2147483647)
56 Passed: static countSmaller(2147483647, 0, 2147483647)
57 Passed: static countSmaller(-2147483648, 2147483647, 2147483647)
58 Passed: static countSmaller(0, 2147483647, 2147483647)
59 Passed: static countSmaller(2147483647, 2147483647, 2147483647)
60 Passed: static main(null)
61 Passed: static main({})
62 
63 ===============================================
64 Command line suite
65 Total tests run: 58, Failures: 1, Skips: 0
66 ===============================================

關於debug

　　在本單元，咱們使用了JML規格方法，嚴格按照JML規格，進行單元測試及自動測試能夠避免不少錯誤。在課下，我還使用datamaker生成數據並進行計時對拍。

　　但本單元容易出錯的地方還有時間，我在三次強測中未出現錯誤，但在第三次互測中，被一個數據hack了CTLE，主要仍是由於使用了拆點的方法使圖巨大，每次跑所有的節點消耗時間過多。debug時選擇用了lazy的方法，並進行一些優化。

4、總結與體會

　　本單元做業中，初次接觸基於JML的規格化設計。咱們第一次經歷了根據JML所規定的規格，實現相應接口的工做模式。本單元中，須要咱們閱讀，理解JML所規定的規格，這除了須要咱們對JML基本語法的理解，更須要的是創建起規格化設計的思想。

　　JML規格只是規定對輸入的前置約束和對輸出的後置約束，而對於咱們具體運用何種數據結構，如何實現沒有明確要求。因此，咱們的具體實現，還要考慮不少方面。由於咱們有大量的查詢指令，要保證不CTLE，須要相應結構緩存計算層，使查詢爲O(1)複雜度。而且，由於三次做業的增量式遞增，因此架構的可擴展性很是重要。

　　通過前兩個單元的聯繫，我認爲我在OO面相對象的思想有了必定的提升。本次做業中，我基本上是進行增量式重構，架構有了必定的可擴展性。而且我學習封裝了一系列數據結構，使類的功能性更加集中，代碼架構更加加清晰。這從複雜度測試中能夠看出，本單元做業的CK複雜度和方法複雜度測試顯示都處於一個良好的狀態。這也從另外一方面讓我體會到JML規格化設計的好處。由於我根據JML的規約進行設計與擴展，實現接口PathContainer <-- Graph <-- RailwaySystem逐步遞進，讓個人代碼的架構天然具備了必定的擴展性。

　　使用JML規格化設計的另外一方面的優點就在於測試與驗證上。在本單元我還體驗了幾種不同的測試方法，如Junit單元測試，OpenJML和JMLuniting的自動測試。基於JML還有不少測試手段和方法能夠進一步探究。

　　但願能在從此的代碼生涯中，更好的運用面向對象、抽象、規格化的思想。設計好的構架，寫好的代碼，實現好的性能。

相關標籤/搜索

每日一句

每一个你不满意的现在，都有一个你没有努力的曾经。