BUAA-OO-第三單元做業-JML之圖論

時間 2019-11-12

標籤 buaa 第三單元 jml 圖論简体版

原文原文鏈接

OO第三單元JML規格之圖論應用

1、JML語言說明

基礎語法

1.requires子句定義該方法的前置條件(precondition)，方法執行前須要知足的條件；node

2.反作用範圍限定，assignable列出這個方法可以修改的類成員屬性，\nothing是個關鍵詞，表示這個方法不對任何成員屬性進行修改，因此是一個pure方法。程序員

3.ensures子句定義了後置條件，方法執行後須要知足這條語句的條件。算法

表達式

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

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

3.\sum表達式：返回給定範圍內的表達式的和。數據結構

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

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

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

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

8.new JMLObjectSet {Integer i | s.contains(i) && 0 < i.intValue() } 表示構造一個JMLObjectSet對象

操做符

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指示一個全集.

5.關鍵詞 also ，它的意思是除了正常功能規格外，還有一個異常功能規格.signals子句的結構爲

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

類規格

### 數據抽象規格

數據抽象的內容、抽象操做描述
自定義數據結構，提升封裝程度
數據抽象操做：

　　構造、更新、觀察、生成

### 不變式與可變式

類規格應該保證對象操做有效
方法執行過程當中有可能會修改爲員變量（更新操做），即對象的不變式有可能不知足，則該過程必須爲不可見狀態；類規格強調任意可見狀態下都要知足不變式。

繼承往下的本質擴充和擴展
繼承往上的本質隱藏和通常化

ps:繼承具備嚴格的數據抽象層次約束，而接口能夠自由跨越多個數據抽象層次

- 子類數據抽象=繼承父類+本身新增的

- 子類數據規格=繼承+擴展+新增

- 子類方法規格=繼承+重寫+新增

## 類型層次下規格關係

- 子類重寫父類方法能夠減弱規定的requre，或者增強ensure

## 規格設計的知足，類正確

- 基類

- 子類對象有效性

- 子類重寫方法

## 集合元素的迭代訪問

## 規格模式

約束類別：

　　相對約束、絕對約束

不變式在當前狀況下式子成立條件不會改變、可變式

應用工具鏈

OpenJML

自動check JML規格文檔並生成報告。

Junit自動測試類

2、JMLUnitNG測試類

Graph接口測試類

 1 1 public void before() throws Exception {
 2  2     int[] p1 = {1, 2, 3};
 3  3     int[] p2 = {1, 2, 3};
 4  4     int[] p3 = {1, 2, 3, 4, 5};
 5  5     path1 = new MyPath(p1);
 6  6     path2 = new MyPath(p2);
 7  7     path3 = new MyPath(p3);
 8  8     graph.addPath(path1);
 9  9     graph.addPath(path2);
10 10     graph.addPath(path3);
11 11 }
12 12 
13 13 @After
14 14 public void after() throws Exception {
15 15 }
16 16 
17 17 @Test
18 18 public void testAddPath() {
19 19     Assert.assertEquals(1, graph.addPath(path1), 1);
20 20     Assert.assertEquals(1, graph.addPath(path3), 1);
21 21 }
22 22 
23 23 @Test
24 24 public void testContainsNode() {
25 25     Assert.assertEquals(1, graph.addPath(path1), 1);
26 26     Assert.assertEquals(1, graph.addPath(path2), 1);
27 27     Assert.assertTrue(path3.containsNode(1));
28 28     Assert.assertTrue(graph.containsNode(5));
29 29     Assert.assertEquals(1, graph.addPath(path3), 1);
30 30     Assert.assertTrue(graph.containsNode(5));
31 31 }
32 32 
33 33 @Test
34 34 public void testRemovePath() {
35 35     Assert.assertEquals(1, graph.addPath(path1), 1);
36 36     Assert.assertEquals(1, graph.addPath(path3), 1);
37 37     Assert.assertEquals(1, graph.addPath(path1), 1);
38 38     Assert.assertEquals(1, graph.addPath(path3), 1);
39 39 }

View Code

　　測試三個方法，ContainsNode, addPath, RomovePath.

　　利用斷言添加預期結果和實際運行結果的判斷，以及真假表達式。

報告結果

3、架構設計

第一次：

設計思考

　　1.本次做業咱們知道，經過繼承Path、PathContainer兩個官方提供的接口，來實現本身的MyPath、MyPathContainer容器；本題有添加、刪除、查詢路徑，查詢節點，查詢路徑id，求不一樣節點數等操做。對這些功能咱們看起是很熟悉的，也知道不涉及高級數據結構，經過閱讀JML文檔也知道，只需實現便可，後續再考慮時間複雜度的優化。首先讀懂JML規格文檔，能夠按照JML文檔所表達的意思構建代碼，能夠保證正確性，但不必定保證是最優的（每每這種狀況只是爲了簡明解釋該方法的功能，而忽略其性能，性能是程序員須要考慮的）。

　　2.路徑結構想到的是利用Arraylist容器進行存儲節點數組，和路徑數組，而後方便遍歷和查找，有jdk已有的方法，只需調用便可。後來發現，Arraylist容器底層的操做，遍歷查找都是經過for循環逐個查找的，效率顯然是底下的。所以會考慮到HashMap或者Hashset,LinkedHashset,我選擇了後兩個。

架構層次

基礎層

　　MyPath
　　MyPathContainer實現官方接口的類

數據結構層

　　對容器進行添加、刪除Path，計算容器內不一樣節點數；
　　對每一個Path進行查找節點，計算不一樣節點數

緩存計算層

　　對不一樣節點數求解能夠緩存，每次增長或刪除Path時從新計算

應用層

　　PathContainer

第二次：

設計思考

　　1.繼承Path、Graph兩個官方提供的接口，經過設計實現本身的Path、Graph容器，來知足接口對應的規格。

　　2.Graph容器繼承了上次做業的PathContainer接口，爲其拓展了一些本次做業新增的功能，實際上，MyPath類和MyPathContainer類能夠保持不變，而後讓MyGraph實現便可。

　　3.增長一些指令和功能：容器中是否存在某一條邊、兩個結點是否連通、兩個結點之間的最短路徑。此題須要構建圖的數據結構，而後進行相應功能的計算。

架構層次

基礎層

　　MyPath
　　MyPathContainer實現官方接口的類
　　MyGraph類

數據結構層

　　Struct圖結構類:用於存儲圖，判斷節點連通性，求解最短路

緩存計算層

　　對不一樣節點數求解、節點連通性、最短路能夠緩存，每次增長或刪除Path時從新計算

圖建模層

　　經過Map<idPath, path>映射關係，以及節點nodeId map <nodeId, nodeNum>映射關係創建圖結構。

應用層

　　MyGraph中的各類功能

第三次：

設計思考

　　1.繼承Path、RailwaySystem兩個官方提供的接口，經過設計實現本身的Path、RailwaySystem容器，來知足接口對應的規格。

　　2.同Path類能夠複用以前的實現，只需增長RailwaySystem新增的接口功能便可

　　3.新增指令，整個圖中的連通塊數量、兩個結點之間的最低票價、兩個結點之間的最少換乘次數、兩個結點之間的最少不滿意度簡單來講，對於同一個圖，須要有四種功能，四種求解。通常狀況下，是將四種功能單獨開來，構建四個類建圖管理。

架構層次

基礎層

　　MyPath
　　MyPathContainer實現官方接口的類
　　MyGraph類
　　MyRailwaySystem

數據結構層

　　ShortestPath：最短路求解類
　　ConnectB：聯通塊求解類
　　LeastTrans：最少換乘類
　　LeastPrice ：最低票價類
　　LeastUnp：最低不滿意度類

緩存計算層

　　同第二次做業，每種功能計算均可以利用數組進行緩存，只有當add,remove指令時更新

圖建模層

　　四個類，四種圖建模，同一種圖映射關係。

應用層

　　MyRailwaySystem

4、總結分析

第一次Path、PathContainer類實現

任務

閱讀JML規格編寫相應的類和方法從而實現接口。
指令功能：添加路徑、刪除路徑、根據路徑id刪除路徑、查詢路徑id、根據路徑id得到路徑、得到容器內總路徑數、根據路徑id得到其大小、根據徑id獲取其不一樣的結點個數、根據結點序列判斷容器是否包含路徑、根據路徑id判斷容器是否包含路徑、容器內不一樣結點個數、輸入指令格式：DISTINCT_NODE_COUNT、根據字典序比較兩個路徑的大小關係、路徑中是否包含某個結點

　　　　值得注意的是：程序的最大運行cpu時間爲10s。所以不僅是簡單考慮用迭代器進行遍歷查找，應該考慮更高效的查找方法。

本題思路

　　本次做業高級算法應該說是沒有的，低級算法也說不上有，只是一些簡單的路徑操做，另外，本單元知識和圖論數據結構相似，至關於從新用了一邊圖論，本身創建數據結構，再進行遍歷算法。

　　本題有添加，刪除，查詢路徑，查詢節點，查詢路徑id，求不一樣節點數等操做。

　　1.首先讀懂JML規格文檔，能夠按照JML文檔所表達的意思構建代碼，能夠保證正確性，但不必定保證是最優的（每每這種狀況只是爲了簡明解釋該方法的功能，而忽略其性能，性能是程序員須要考慮的）。

　　2.路徑結構想到的是利用Arraylist容器進行存儲節點數組，和路徑數組，而後方便遍歷和查找，有jdk已有的方法，只需調用便可。後來發現，Arraylist容器底層的操做，遍歷查找都是經過for循環逐個查找的，效率顯然是底下的。

　　所以會考慮到HashMap或者Hashset,LinkedHashset,我選擇了後兩個。

　　Hashset和LinkedHashset可以去除容器中的重複元素，構成集合，惟一區別就是，LinkedHashset保持了元素鏈接關係，也就是保持了順序。在去重這一應用上，此題的複雜度下降了很多，在實際生活中，對大量數據的處理也頗有用。

　　查找某一節點是否存在於路徑中，也即該路徑是否包含這個節點，我也運用Hashset去重，大大下降了複雜度，另外HashSet的contains方法是利用key-value來映射查找的，所以比for循環更快。

1 public boolean containsNode(int node) {
2     HashSet<Integer> arr = new HashSet<>(nodes);
3     if (arr.contains(node)) {
4         return true;
5     }
6     return false;
7 }

　　求解路徑不一樣節點數，也是相似方法，建立一個Hashset容器，往容器裏添加每條路徑的節點數組，自動去重，最後只需返回該容器的大小便可。

1 private void distinctNodeCount() {
2     HashSet<Integer> arr = new HashSet<>();
3     for (Path it : paList) {
4        HashSet<Integer> nodes = new HashSet<>(((MyPath) it).getMyPath());
5        arr.addAll(nodes);
6     }
7     count = arr.size();
8 }

　　對於本題和後兩道題，還有一個能夠考慮優化的點，就是不須要每次查找從新計算不一樣節點數，而是每次改變路徑的時候，增長或者刪除，纔去計算，因此能夠利用變量進行存儲當前計算結果，訪問的時候直接返回便可。

3.Main類和方法

1 public class Main {
2     public static void main(String[] args) throws Exception {
3         AppRunner runner = AppRunner.newInstance(
4                 MyPath.class, MyPathContainer.class);
5         runner.run(args);
6     }
7 }

4.對於Path類要求實現的還有兩個東西，一個是迭代器，一個是比較器。

迭代器直接利用

 1 return nodes.iterator();
 2 
 3 比較器本身寫了一個相似於字符串比較的代碼
 4 
 5 public int compareTo(Path o) {
 6     int len = nodes.size();
 7     if (nodes.size() > o.size()) {
 8         len = o.size();
 9     }
10     for (int i = 0; i < len; i++) {
11         if (this.getNode(i) != o.getNode(i)) {
12             return Integer.compare(this.getNode(i), o.getNode(i));
13         }
14     }
15     return Integer.compare(this.size(), o.size()); // equal
16 }

Debug

　　本次做業比較簡單，沒有找到你們的bug，基本上都是時間複雜度沒有仔細考慮而超時，我本身也是一個例子，第一次寫根本沒有優化。以後才考慮優化的。

　　可是，在Hashset處理的時候也有可能會出現一點問題，HashSet是不保證元素順序的，它每次都會根據hash值來進行排序，因此會形成影響，所以用LinkedHashset。

　　還須要注意的是增長和刪除路徑，對於和其餘路徑節點重複的節點不該該刪除。

度量分析

類圖

除去官方接口本身寫的只有三個類：Main,MyPath,MyPathContainer

MyPath實現Path接口，MyPathContainer實現Container接口：

代碼行數

複雜度

　　這次代碼長度不長，另外有了JML規格文檔，對代碼規範要求程度上升，其實你們寫的都相似於規格文檔所規定的。從此次做業開始，我逐漸模仿規格文檔和官方接口裏的範例寫方法功能註釋，類註釋，接口註釋等信息。

第二次Graph類實現

任務

　　繼承Path、Graph兩個官方提供的接口，經過設計實現本身的Path、Graph容器，來知足接口對應的規格。Graph容器繼承了上次做業的PathContainer接口，爲其拓展了一些本次做業新增的功能，實際上，MyPath類和MyPathContainer類能夠保持不變，而後讓MyGraph實現便可。
　　增長一些指令：容器中是否存在某一條邊、兩個結點是否連通、兩個結點之間的最短路徑。

　　值得注意的是:任意時刻容器中全部的節點數不超過250，而不是一次測試中全部節點數不超過250。

解題思路

　　　　我複用了第一次做業已優化且調試正確度高的代碼，這次只增長了Graph接口裏新增的方法功能，如新增指令描述。

顯然，此次是一個圖的數據結構，有求解兩個節點之間的最短路徑，判斷兩個節點是否連通以及判斷是否存在一條邊。

　　考慮到圖結構，固然須要建圖，已知任什麼時候可已存在的圖節點數不超過250，因此咱們是否能夠開一個250*250的graph[][]數組呢？繼續看，節點id符合整型，意味着節點能夠是很大（123456789）或者很小（-12345678）的數，此時再單純地用二維數組是不夠的。咱們須要考慮對節點的映射，將存入的節點映射到[0,249]這個區間內，由於時刻保證不會超出這個範圍。（固然稍微大一點255也能夠畢竟250很差聽）。

　　說到映射，這個確定是運用HashMap來進行映射，本次做業也屢次用到HashMap來查找，從而減小時間複雜度。

　　圖結構的存儲及映射關係以下：

/* <idPath, path> */
private static HashMap<Integer, Path> map = new HashMap<>();

　　節點映射關係以及一些定義以下：

1 /* nodeId map <nodeId, nodeNum>*/
2 private static HashMap<Integer, Integer> nodeMap = new HashMap<>();
3 
4 private static int idPath = 0; // unique path id
5 private static int count = 0; // store all distinct nodes
6 private static int nodeNum = 0; // nodeNum of map nodeId

　　idPath是路徑id，count用來存儲當前時刻不一樣節點數，nodeNum就是用來計算更新當前容器中全部的節點，方便映射。

　　3.最短路求解我直接採用floyd算法，對整個圖進行搜索，而後順便標記連通矩陣（便可達性矩陣），只要dis[][]非最大，即存在邊。

　　4.這是此次新增的爲了方便計算圖結構的類，計算最短路和判斷連通性一塊兒實現的：

 1 private StructGraph struct = new StructGraph();
 2 
 3 /**
 4  * 圖結構類
 5  * 說明：
 6  * 計算連通性，用可達性矩陣存儲
 7  * 計算最短路徑，Floyd算法
 8  * PS:這兩個操做能夠一塊兒執行，都是在寫入指令後從新計算
 9  */
10 
11 相關定義：
12 
13 /* map nodeId to graph */
14 private boolean[][] graph = new boolean[MAX_Node][MAX_Node];
15 private int[][] dis = new int[MAX_Node][MAX_Node]; // shortest dis
16 /* connected */
17 private boolean[][] connected = new boolean[MAX_Node][MAX_Node];
18 
19 每次經過節點映射關係取得數組下標：
20 
21 int nodeU = nodeMap.get(nodes.get(i));
22 int nodeV = nodeMap.get(nodes.get(i + 1));

Debug

　　任意時刻容器中全部的節點數不超過250，而不是一次測試中全部節點數不超過250。

　　我由於理解錯這句話，致使我強側只有15分，而後de完bug快速AC了。一不當心沒注意到，釀成大禍。後來花了一天時間寫了評測器、對拍器，而後沒有用上。除了這個bug其餘問題就是求最短路的問題，我直接使用floyd算法bug很少。固然時間複雜度稍微高一點。

度量分析

類圖

這次代碼增長了管理圖結構的類StructGraph，其他的符合接口要求。

代碼行數

複雜度

　　在圖結構上增長了功能，且運用了數據結構的算法，這次做業的代碼量整體還能夠，算法都學過能較快寫出來，主要是轉化思路的問題。

第三次Path、RailwaySystem類實現

任務

　　繼承Path、RailwaySystem兩個官方提供的接口，經過設計實現本身的Path、RailwaySystem容器，來知足接口對應的規格。
　　一樣Path類能夠複用以前的實現，只需增長RailwaySystem新增的接口功能便可（正如助教所說的OOP思想）。
　　新增指令:整個圖中的連通塊數量、兩個結點之間的最低票價、兩個結點之間的最少換乘次數、兩個結點之間的最少不滿意度。

解題思路

　　　　1.形如第二次做業，新增四個類方便管理這四種功能，單獨求解。

/* Railway class */
// blockCount
private static int blockCount; // block count
private ConnectB block = new ConnectB(); // connected block
private static boolean firstAdd = true; // addPath weather first
// transCount
private LeastTrans trans = new LeastTrans();
// UnpleasentCount
private LeastUnp unPleasent = new LeastUnp();
// Price
private LeastPrice price = new LeastPrice();

View Code

　　2.最容易實現的功能是求解連通塊數，利用並查集（外加壓縮路徑算法）輕鬆判斷；而後就是換乘求解，邊權設置爲0，對每一個path連通更新邊權（此狀況不用更新），最後每條聯通的邊權值都+1，求最短便可，後面的相似。

 1 /**
 2  * 最低不滿意度
 3  * F(u) = (int)(u % 5 + 5) % 5, H(u) = pow(4, F(u))
 4  * 邊E(u,v)的不滿意度 UE = max(H(u), H(v))
 5  * 每進行一次換乘會產生 UnP = 32 點不滿意度
 6  * 對於一條路徑，UPath = sum(UE) + y * Unp, y爲換乘次數
 7  * 存儲邊權值，權值即爲該邊的不滿意度 UE + 32，將該path構造爲徹底圖
 8  * 用Floyd算法求帶權圖最短路
 9  */
10 
11 /**
12  * 最低票價
13  * x爲通過的邊數，y爲換乘次數，票價PPath = x + 2 * y
14  * 存儲邊權值，權值爲該邊的票價，即 1 + 2，將該path構造爲徹底圖
15  * 用Floyd算法求帶權圖最短路
16  */
17 
18 /**
19  * 連通塊數
20  * 並查集，addPath能夠增長，但每次remove須要重算 afresh
21  * 添加 unio(x, y), (x, y) <==> (nodeMap.get(x), nodeMap.get(y))
22  * 考慮路徑壓縮find
23  */
24 
25 /**
26  * 基本圖結構類
27  * 說明：
28  * 計算連通性，用可達性矩陣存儲
29  * 計算最短路徑，Floyd算法
30  * PS:這兩個操做能夠一塊兒執行，都是在remove指令後從新計算
31  */
32 
33 /**
34  * 最少換乘
35  * 存儲每一個node所在路線號,並存儲邊權，權值初始化爲INFINITY
36  * 對於每條path內，邊權值初始化爲1，即不須要換乘，將該path構造爲徹底圖
37  * Floyd算法求最短路，(weight求和 - 1)爲最少換乘次數
38  */

View Code

　　3.並查集路徑壓縮算法：

　　判斷該節點是不是根節點，若是不是，則找到它的根節點，而後依次將它以及它的祖先節點（但非根節點的節點）都標記爲根節點的兒子節點，最終的結果也就是一個根節點下其他的都是兄弟節點，而沒有父子關係了。

 1 protected int pressedFind(int x) {
 2     int parent = father.get(x);
 3     while (parent != father.get(parent)) {
 4         parent = father.get(parent);
 5     }
 6     int pre;
 7     int cur = x;
 8     while (cur != father.get(cur)) {
 9         pre = father.get(cur);
10         father.put(cur, parent);
11         cur = pre;
12     }
13     return parent;
14 }