前言
相比於前兩個單元，這個單元對於測試能力的需求有了進一步的提升。對於所給的規格，我首先需要看懂，並且要使用比較好的方法進行實現。這也帶來了一個問題，我必須能夠編寫測試集來測試自己寫的數據結構。還有一個問題，就是即使我每個方法可能符合規格，但是整個程序在總體上會有bug怎么辦。所以，這個單元既需要我們從方法級別進行考慮，又需要從工程級別進行量化。下面我將開始分享我的學習心得，請多多指教! \(O~O)/
JML知識梳理
第一次接觸JML，我的反應是：這也太瘋狂了吧，架構師不就是幫程序員把程序實現用偽代碼描述了么！這種思想是完全錯誤的，首先規格化描述寫的不是“方法流程”，另外按照給的數據結構來整只有死路一條。
這么優雅的過程，實現后可能就6個for循環連環套吧
那么JML(Java Modeling Language)到底是什么呢？“在面向對象編程中，一個重要原則就是盡可能地推遲對於“過程”的思考。”在每次編寫程序后，想好了整體架構，搭建好了類和接口，之后面對的就是每一個方法。這個時候，我們思考的是這個方法能給我帶來什么預期結果，之后再考慮如何實現。比如對於getLeastUnpleasantValue方法（上圖），它帶給我的結果是一個path，按照這個path走，我能最“滿意”。JML在代碼中增加了一些符號，這些符號只表述一個方法干什么，並不關系它的實現過程。使用JML，我們就可以描述對於某一個方法的預期功能，卻不管實現過程，JML可以把過程性的思考延遲到方法設計中，這點完全符合了“面向對象”。
-
JML的理論基礎
JML非常強大，其有大量用於描述行為的結構（正常、異常行為；模型域、量詞……）。JML可以寫的很清晰、有層次。JML用這種“抽象”的數據結構去描述，帶來了兩個好處：首先，JML是獨立的，不會因為實現代碼結構的改變而被迫變化，這樣這個方法的數據結構和整體程序的數據結構是相互獨立的；其次，在有代碼實現之前，就可以寫JML。在實際設計中，JML可以在實現前對設計的規格進行精確傳達，也可以幫助梳理自己實現的代碼。
-
JML的工具鏈
JML也擁有很多很好用的工具，可以提供JML規范檢查，或者是隨機測試數據生成測試。我對幾種工具了解的不是很多，如果有什么好用的請大家補充。
- 使用OpenJml的-check檢查JML規范性
- 使用SMT Solver檢查代碼等價性
- 使用JMLUnitNG生成數據測試代碼
- ……
我將下發的JML指導書進行總結，鏈接在此：https://blog.csdn.net/weixin_41412192/article/details/89527142
JMLUnit和JUNIT測試
JUnit測試
雖然沒有要求寫這部分內容，但是我還是願意分享這個過程。在對Graph的任何方法進行測試之前，首先要初始化整個圖。這個過程我們沒必要在每個test函數都進行一次，所以使用@BeforeClass。
接下來我詳細根據JML介紹我的測試思路。
-
containsNode(int nodeId)
//@ ensures \result == (\exists Path path; path.isValid() && containsPath(path); path.containsNode(nodeId));
從輸入上看，此方法輸入的是一個int類型是數；從結果上看，此方法返回的是一個boolean類型的常量。於是這個測試思路就很好想了，只需要檢測“有”和“沒有”的點就可以。我也加入了對於負數點的檢測，擴充測試范圍。
-
containsEdge(int fromNodeId, int toNodeId)
/*@ ensures \result == (\exists Path path; path.isValid() && containsPath(path); @ (\exists int i; 0 <= i && i < path.size() - 1; (path.getNode(i) == fromNodeId && path.getNode(i + 1) == toNodeId) || @ (path.getNode(i) == toNodeId && path.getNode(i + 1) == fromNodeId))); @*/
從輸入上看，輸入的是任意兩個int類型數據；從輸出上看，得到的是一個boolean。這塊需要注意的是，當輸入的點不在圖中時，直接輸出false，而不能拋異常；自己和自己在containsEdge中沒有特殊情況。另外，有些同學可能是用HashMap做的，當遇到（x,x）這種邊的時候，可能會“加兩次”。這樣也會導致出錯。所以，我將測試用例划分成了7類：
- 兩點都在圖中，並且邊存在
- 兩點都在圖中，但邊不存在
- from點不在圖中，to點在
- from點在圖中，to不在
- 兩點都不在圖中
- from == to且有這條邊
- from == to但是沒有這條邊
try_catch部分是對（x,x）這種數據的特殊測試
-
isConnected(int fromNodeId, int toNodeId) throws NodeIdNotFoundException
/*@ normal_behavior @ requires (\exists Path path; path.isValid() && containsPath(path); path.containsNode(fromNodeId)) && @ (\exists Path path; path.isValid() && containsPath(path); path.containsNode(toNodeId)); @ assignable \nothing; @ ensures (fromNodeId != toNodeId) ==> \result == (\exists int[] npath; npath.length >= 2 && npath[0] == fromNodeId && npath[npath.length - 1] == toNodeId; @ (\forall int i; 0 <= i && (i < npath.length - 1); containsEdge(npath[i], npath[i + 1]))); @ ensures (fromNodeId == toNodeId) ==> \result == true; @ also @ exceptional_behavior @ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(fromNodeId)); @ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(toNodeId)); @*/
這個方法與之前的containsEdge類似。從輸入上看，輸入的是任意兩個int類型數據；從輸出上看，得到的是一個boolean。這塊需要注意的是，當輸入的點不在圖中時，直接輸出false，而不能拋異常；自己和自己在isconnected中是一定為1的。在編寫測試數據時，注意不僅要測試兩個不是相鄰的點，更要測試相鄰的兩個點。還有，要注意“換乘”的情況。所以，我將測試用例划分成了8類：
- 兩個點都在圖中，（直接|間接）相連，不相鄰
- 兩個點都在圖中，相連，相鄰
- 兩個點都在圖中，不相連
- from == to，相連
- from == to，不相連
- from不在圖中（異常）
- to不在圖中（異常）
- from和to都不在圖中（異常）
我嘗試使用ExpectedException類來分析拋出的異常情況，但是總是報錯，現在也沒有解決。
這兩個分明是一樣的，但是會報錯
-
getShortestPathLength(int fromNodeId, int toNodeId) throws NodeIdNotFoundException, NodeNotConnectedException
/*@ normal_behavior @ requires (\exists Path path; path.isValid() && containsPath(path); path.containsNode(fromNodeId)) && @ (\exists Path path; path.isValid() && containsPath(path); path.containsNode(toNodeId)); @ assignable \nothing; @ ensures (fromNodeId != toNodeId) ==> (\exists int[] spath; spath.length >= 2 && spath[0] == fromNodeId && spath[spath.length - 1] == toNodeId; @ (\forall int i; 0 <= i && (i < spath.length - 1); containsEdge(spath[i], spath[i + 1])) && @ (\forall Path p; p.isValid() && p.getNode(0) == fromNodeId && p.getNode(p.size() - 1) == toNodeId && @ (\forall int i; 0 <= i && (i < p.size() - 1); containsEdge(p.getNode(i), p.getNode(i + 1))); p.size() >= spath.length) && @ (\result == spath.length - 1)); @ ensures (fromNodeId == toNodeId) ==> \result == 0; @ also @ exceptional_behavior @ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(fromNodeId)); @ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(toNodeId)); @ signals (NodeNotConnectedException e) !(\exists int[] npath; npath.length >= 2 && npath[0] == fromNodeId && npath[npath.length - 1] == toNodeId; @ (\forall int i; 0 <= i && (i < npath.length - 1); containsEdge(npath[i], npath[i + 1]))); @*/
這個函數算是這次作業中的難度巔峰了，但是測試起來一點也不難！這里面要注意的是幾種異常情況的拋出，from == to怎么辦。我將測試分為 類：
- 兩個點都在圖中，相連
- 兩個點都在圖中，不相連（異常）
- from == to，相連
- from == to，不相連
- from不在圖中（異常）
- to不在圖中（異常）
- from和to都不在圖中（異常）
由於我沒解決對異常拋出的正確性判定，我代碼中先不測試了。
JMLUnit測試
這塊我弄了很長時間，前期一直出現無法導入，正確的命令行是這樣的：
java -jar jmlunit-1_4/jmlunitng-1_4.jar -cp Project10_marven/specs-homework-2-1.2-raw-jar-with-dependencies.jar Project10_marven/src/main/java/MyGraph.java
然后就生成了無比多的.java，點擊我選中的test文件就可以測試了。測試結果巨長我就只放一小部分了。
在這一長串中我發現getpathid和所有remove都是錯的，而且都是那種很神奇的數據，比如null、0、maxInt。我覺得可能是因為這些數據沒有找到點，就跑出來異常，然后測試就fail了。（因為其他沒有throw exception的方法都沒有出錯）。不過我不知道這樣怎么解決，所以先把問題留在這里。
觀察發現，隨機生成的數據實際上不隨機，都是一些邊界數據。我發現：
- 對於int型的變量，數據都為0，-2147483648，2147483647（maxInt）
- 對於Object的，使用null
所以我認為我不太理解這個玩意的意義，這些數據並不能檢測出我大部分的bug。
架構分析
必須承認，我這回三次作業都是一鍋粥的狀況。一方面是時間不太夠我去調整結構了，另一方面是我也不太會寫標程那種優雅的結構。在分析標程之前，我先回顧一下自己的程序。
在三次作業中，我都使用了ThreadMXBean包來測量CPU時間。但是這個時間並不精准，只有一部分的參考性。
-
第一次作業
先從MyPath說起。我使用了ArrayList數據結構，因為它是動態數組，容量可以自由改變，並且各種操作（即使實現上都是O(n)）非常方便。但是ArrayList相比於靜態數組，時間是它最大的弱點。不過我認為，這一點節省的時間對於我們的作業來講微不足道。
之后看一下MyPathContainer，我使用了HashMap創造了一種來回的映射關系，“pathId到Path”和“Path到pathId”。這樣做的好處有許多：
- 查詢的時候，可以利用HashMap的hashcode優勢，速度極快
- 動態結構HashMap增刪很容易
並且，我建立了mapId這個HashMap，來存儲不同的點有多少個。這樣，我將時間復雜度全都放在了add和remove中，查詢的時候都只是O(1)。
Iterator itNode = path.iterator(); while (itNode.hasNext()) { int a = (Integer) itNode.next(); if (mapId.containsKey(a)) { mapId.put(a,mapId.get(a) + 1); } else { mapId.put(a,1); } }
-
第二次作業
為了計算最短路徑，必須生成鄰接矩陣，那么也就需要記錄邊與邊之間的連接關系。我把這個“記錄”行為放在了add和remove中，平坦時間復雜度。由於一條邊可能出現多次，所以還需要記錄這條邊的個數。因而結構體是HashMap<Integer,HashMap<Integer,Integer>>。
// add方法內“標記”邊
private void markPath(Path path) { int size = path.size(); for (int i = 0;i < size - 1;i++) { int a = path.getNode(i); int b = path.getNode(i + 1); markEdge(a,b); if (a != b) { markEdge(b,a); } } }
在初始化鄰接矩陣時，會遇到這種情況：需要知道所有點中的第i個點的nodeId；需要知道nodeId是所有點中的第幾個點。因而我創建了兩個映射專用HashMap，建立這種映射關系。由於會出現add和remove，這種關系經常會被破壞，而緩存機制又過於復雜，所以我選擇在初始化鄰接矩陣時更新這兩個HashMap。
private void initDistanceMap() { Iterator<Integer> it = adjacentMap.keySet().iterator(); int im = 0; nodeLink = new HashMap(); nodeReverseLink = new HashMap(); while (it.hasNext()) { int key = it.next(); nodeLink.put(key,im); nodeReverseLink.put(im,key); im++; } int size = nodeLink.size(); distanceMap = new int[size][size]; for (int i = 0; i < size;i++) { for (int j = i; j < size;j++) { if (i == j) { distanceMap[i][i] = 0; continue; } if (containsEdge(nodeReverseLink.get(i), nodeReverseLink.get(j))) { distanceMap[i][j] = 1; distanceMap[j][i] = 1; } else { distanceMap[i][j] = inf; distanceMap[j][i] = inf; } } } }
HashMap對於映射關系使用起來非常的方便，但是一個巨大的缺點就是它遍歷起來非常耗費時間。所以要注意盡量不用HashMap本身進行遍歷，盡量利用hashcode。
-
第三次作業
挺好的我這幾次作業都是“一類到底”……
由於我不太會使用工廠模式，我干脆直接建立了一個“倉庫”類（Storage），存儲所有的映射關系。除了上次作業中我建立的所有點和標號之間的映射關系，我還建立了針對每一個path之內的這種映射關系。這次作業我的算法主旨是“只改變算法的權值矩陣“。在init函數中，需要遍歷每個path。所以我把這個步驟也放在了add和remove中。
public void addPathWeight(Path path) { int count = path.getDistinctNodeCount(); int size = path.size(); int[][][] weight = new int[3][count][count]; // price: 0 unple: 1 change: 2 for (int i = 0;i < count;i++) { for (int j = i;j < count;j++) { if (i == j) { weight[0][i][j] = 0; weight[1][i][j] = 0; weight[2][i][j] = 0; } weight[0][i][j] = inf; weight[0][j][i] = inf; weight[1][i][j] = inf; weight[1][j][i] = inf; weight[2][i][j] = inf; weight[2][j][i] = inf; } } HashMap<Integer,Integer> pathNodeLink = Storage.getPathNodeLink().get(path); for (int i = 0;i < size;i++) { for (int j = i;j < size;j++) { int n1 = pathNodeLink.get(path.getNode(i)); int n2 = pathNodeLink.get(path.getNode(j)); if (j - i < weight[0][n1][n2] || j - i < weight[0][n2][n1]) { weight[0][n1][n2] = j - i; weight[0][n2][n1] = j - i; } int val = getFakeUnpleasantValue(path,i,j); // System.out.println(n1 + " " + n2 + " " + val); if (val < weight[1][n1][n2] || val < weight[1][n2][n1]) { weight[1][n1][n2] = val; weight[1][n2][n1] = val; } weight[2][n1][n2] = 1; weight[2][n2][n1] = 1; } } // 由於有環的情況，所以得對每個path先Floyd一次。 for (int k = 0;k < count;k++) { for (int i = 0; i < count;i++) { for (int j = 0; j < count;j++) { for (int l = 0;l < 2;l++) { int sum = weight[l][i][k] + weight[l][k][j]; if (weight[l][i][j] > sum) { weight[l][i][j] = sum; weight[l][j][i] = sum; } } } } } HashMap<Path,int[][][]> weightMap = Storage.getWeightMap(); weightMap.put(path,weight); Storage.setWeightMap(weightMap); }
-
標程分析
我的圖從來沒有畫的這么整齊過……
Graph和Map方法的核心都在幾個core類中。那addEdge舉例，core類中存放的是比較”底層“的方法，而在MyGraph類中則調用core的方法，因而很清晰。假如未來的作業中變成了有向圖，改動也不是很大。
我一直不明白的是這次作業怎么建立工廠，看了標程有一點明白了。首先建立一個factory接口，之后建立針對不同種圖的幾種工廠。在這幾個工廠中，都有構造方法、init方法、權重方法、計算方法和更新方法。這樣做的好處是可以應付各種圖的需求。
bug情況
這幾次作業我都沒有被強測或者在互測中測出bug。\(O_-)/而且由於組內同學太強了，我也沒有找到他們的bug……但是我還是有一些心得可以分享。
這次測試我采用的是黑盒測試（隨機測試）+白盒測試（定點測試）的方式。我首先對寫的每一個方法使用Junit進行測試，之后從整個工程的方面進行測試。
Junit測試
前文提到了，在此不贅述。(0_0)
黑盒測試
純隨機數據，生成各種意想不到的情況。感謝默默同學寫的隨即數據生成器，由於我沒有版權，不放代碼啦！真的是很棒！
白盒測試
白盒測試分為兩個階段，分別針對可能發生的不同種情況。我將拿第三次作業舉例。
-
第一階段：針對於實現方法的具體測試。
// 這是初始化一種映射關系的方法
protected void initLink() { HashMap<Integer,HashMap<Integer,Integer>> adjacentMap = Storage.getAdjacentMap(); Iterator<Integer> it = adjacentMap.keySet().iterator();
// 每次初始化的適合，必須new新的 HashMap<Integer,Integer> nodeLink = new HashMap<>(); HashMap<Integer,Integer> nodeReverseLink = new HashMap<>(); int im = 0; while (it.hasNext()) { int key = it.next(); nodeLink.put(key,im); nodeReverseLink.put(im,key); im++; } Storage.setNodeLink(nodeLink); Storage.setReverseNodeLink(nodeReverseLink); }
測試上面的方法，需要有幾種測試數據。比如既要有add 1 2 3 remove 3這種，也要有add 1 2 3 remove 2這種能夠創造出{1 x 3}的數據。如果在代碼段中我標注的部分沒有new，那么就會報錯。
-
第二階段：針對總體架構的測試
在測試了單個方法之后，需要創造數據來測試方法之間是否能夠成功協作。創造數據時，改變查詢順序或者查詢次數，能獲得一致的查詢結果。
改變查詢順序：
PATH_ADD 1 2 3 4 5 6 2
PATH_ADD 3 2 8 9 1 2
第一組：
{GET_SHORTEST_PATH_LENGTH 3 6
GET_LEAST_UNPLESENT_VALUE 3 6
GET_LEAST_TICKET_PRICE 3 6
GET_LEAST_CHANGE_COUNT 3 6}
第二組：
{GET_LEAST_UNPLESENT_VALUE 3 6
GET_LEAST_TICKET_PRICE 3 6
GET_LEAST_CHANGE_COUNT 3 6
GET_SHORTEST_PATH_LENGTH 3 6}
……
改變查詢次數：
PATH_ADD 1 2 3 4 5 6 2
PATH_ADD 3 2 8 9 1 2
GET_LEAST_UNPLESENT_VALUE 3 6
GET_LEAST_UNPLESENT_VALUE 3 6
GET_LEAST_UNPLESENT_VALUE 3 6
GET_LEAST_UNPLESENT_VALUE 3 6
需要特別注意的一點是連通塊的方法。由於我的連通塊使用的是dfs不是權值矩陣，所以這個方法調用時也會更新所有map之后計算。這里的flag標志位就有可能產生問題。比如我的代碼如果先計算連通塊，再進行其他的查詢，我就會陷入無盡的更新循環之中。在測試中用我寫的方法，是可以測試出來問題的。但是隨即數據就不一定了！
心得體會
對JML的思考
這幾次雖然很認真地學習了JML規格，但是實際上自己寫的時候並不能很好地將JML與代碼進行結合，有些地方沒有認真注意：
- 嚴格保證方法結果，不能私加內容
- 可以利用規格生成隨即數據進行測試（JMLUnitNG）
但是我也學到了很多，比如：
- 先查看先行條件；再查看結果保證
- 查看修改的變量，思考其是不是需要維護
- 規格不束縛自己的實現方式
- 規格書寫：只能調用pure方法；有許多能簡化書寫內容的結構（exists | forall）；……
對數據結構的思考
需要的是性能 + 方便使用結合。所以我自認為這回我寫的映射機制是很好的。另外對於一些容器，一定要去看底層代碼，因為有些時候自己覺得是O(1)的方法，可能不是！詳見ArrayList。
總結
這個單元非常有意思，經常是自己擔心的事情沒有發生，而沒去考慮的卻導致WA聲一片。比如第三次作業，我先開始使用的是Dijstra+部分緩存，后來離作業截至前兩三個小時才發現自己的緩存功能有問題！后來全都改成了Floyd。但是更加戲劇化的是，我的Floyd的三層循環順序給寫反了！這個錯誤，還不是每次都能夠顯現出來，是需要一個比較大的測試集的。這些問題，都是我沒思考過的。而我最擔心的時間問題，最后發現強測中我最長CPU時間也只有6s左右。難怪助教說WA比TLE容易的多！
最后感謝同學們在討論區各種發言，我受益匪淺！我們一起征戰最后的一單元！