目錄

• 梳理JML語言的理論基礎、應用工具鏈情況
• 部署JMLUnitNG/JMLUnit
• 按照作業梳理自己的架構設計，并特別分析迭代中對架構的重構
• 按照作業分析代碼實現的bug和修復情況
• 闡述對規格撰寫和理解上的心得體會

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

面向對象編程思想中有一個重要原則就是盡量推遲過程性的思考。在實現一個程序時，首先考慮的不是先做什么后做什么，而是以具體的事物為單位，考慮它的屬性和行為動作。就像先把主人公和主人公做的事情放進故事中，然后再填充人物之間的對話和交往。

JML語言理論基礎

JML是一種規范java語言的程序，使用前置、后置和不變量等等約束，形成一種契約式設計。JML作為java的注釋可以寫入源文件，并且可以使用openJML進行檢查。通過JML的規約來檢查代碼靜態、動態時候的正確性。
語法
requires 定義了一個先決條件
ensures 定義了一個后置條件
signals 定義了后續方法拋異常時的后置條件
assignable 定義了允許繼續執行了后面方法的條件
pure 聲明一個方法是沒有副作用的
invariant 定義了一個方法的不變的屬性
\result 定義了返回值需要滿足的要求
\old(expression) 用于表示進入方法之前表達式的值
(\forall <decl>; <range-exp>; <body-exp>) 全稱量詞
(\exists <decl>; <range-exp>; <body-exp>) 存在量詞
a==>b a推出b
a<==b a隱含b
a<==>b a當且僅當b
以及，JML注釋可以訪問Java對象，方法和運算符。對象和方法對于JML有一定的可見性，同樣可以通過關鍵字例如spec_public來規定。

各種工具支持

有很多應用工具能夠提供給JML編譯和檢查的支持。比如lowa State JML工具提供了一個斷言檢查編譯器jmlc，將JML注釋轉換為運行時的斷言，一個文檔生成器jmldoc，用于生成Javadoc文檔，增加了來自JML注釋的額外信息。以及一個單元測試生成器jmlunit，它可以從JML注釋中生成JUnit測試代碼。

部署JMLUnitNG/JMLUnit

針對Graph接口的實現自動生成測試用例， 并結合規格對生成的測試用例和數據進行簡要分析。

OpenJML的檢查

由于我的代碼和標程給的JML有點不同，從命名到實現上。所以報錯非常多。

JMLUnitNG的部署。

在Jar包的導入部分經常會出問題。可能是mac系統的緣故。運行JMLUniting，會生成很多個測試類，之后，在idea里可以運行帶有main函數的Main_JML_Test類，利用JML對各個方法進行測試。

按照作業梳理自己的架構設計，并特別分析迭代中對架構的重構

架構設計

本次作業主要填充其中的幾個核心的類，所以不需要考慮前后輸入輸出的問題，大大簡化了細節的設計與思考。三次作業通過迭代，逐漸寫成了一個初步的地鐵線路查詢無向圖。主要分為幾個類：

• 作業一的
  Path 單條路徑
  PathContainer 一個路徑的容器類，像一個玻璃瓶子，能看到里面所有的路徑的情況，而不對路徑進行進一步處理和計算，只負責增減和查詢工作。

• 作業二的
  Graph 圖類，這個類繼承了PathContainer，并在此基礎上增加無向圖的一些概念，點、邊、連通、最短路徑。
  RailwaySystem 地鐵系統，這個類繼承了Graph，并在此基礎上增加了最少票價、最少換乘、最低不滿意度、連通塊。這些需求實際上是對離散數學中的帶權無向圖的一個改進版，所以實際上是一個問題，可以用相同的思路解決。后續會詳細說明。
  在上述的這些類中，分別定義了每一次迭代新增的需求。老師在上課的時候也有提到，在產品迭代更新的時候盡量不去修改原有的那些代碼，即使他是不完善的，應該是再打一個補丁似的在外圍添加。正如這單元的作業。
  因此實際上在迭代的過程中并沒有對之前的架構進行重構，確保每一次迭代時，都用了性能較好的方法，那么在后續增加新需求的時候，只需要在外圍進行擴展，不需要對之前的已經實現的代碼進行改動。

  關于數據結構

  Hashmap中的Hashcode和equals的重寫
  本次作業用到了Java中的Hashmap，和C語言中的類似，只是調用起來更加方便。在研討課上，有同學也分享了他對Hashmap和treemap的理解。關于Hashcode和equals的重寫比較重要。在比較key的時候，Java會先比較Hashcode是否一致，若一致再比較equals。而對于一個對象，它的Hashcode是基于它在內存中的地址計算得到的，因此，如果hashmap的key是一個自定義類，想要自定義他們等同的條件，需要重寫Hashcode和equals方法。對于Hashcode的重寫，通常只將想要作為比較條件的部分寫入，equals也是一樣。比如：

for(int node: nodes)hash = 31 * hash + node;

采用31的原因是加快計算過程，31是1<<5-1，是計算機比較擅長的移位和減法運算。而且31是質數，不同對象的hashcode重合度比較低。

Hashmap與數組的選擇
在PathContainer中用的Hashmap存放路徑和id，訪問時間復雜度是O(1)，是我能想到的最好的方式。之后在無向圖的Floyd或者Dijkstra的計算中，用的是二維數組，雖然二者復雜度都是O(1)，但是對數組的訪問要比Hashmap快很多，而且數組的書寫簡便，不需要考慮太多語法上的問題，可以使得思考重點放在算法上而非語法，思路更清晰。但是在部分實現上還是用Hashmap更好，尤其是那些不需要頻繁訪問，但每次訪問如果不用hashmap就只能遍歷查詢的。比如node2Index和index2Node。兩兩為一組亂序存放，Hashmap很擅長做這種事情。

算法實現設計

總的來說用了Floyd和Dijkstra算法，來計算帶權連通圖的最短路徑、最小票價、最少換乘次數和最小不滿意度。

最短路徑Floyd算法

首先都要準備一個鄰接表。

• 先構造邊的集合。
  為了簡化圖結構變更之后初始化鄰接表的過程，我將鄰接表用一個Hashmap存儲，其中key是Pair類型的，是一條邊的兩個點，value是這條邊出現的次數，記錄次數是為了能夠在增加邊和刪除邊的時候能夠直接對這條路徑上的數目進行操作，而非從所有路徑開始重新繪制一遍鄰接表，當路徑中節點數交多少時，可能這一步會消耗大量的時間。
  需要注意的是，為了節省Hashmap的開支，最好在邊數變成0的時候把這個key刪掉。簡化的代碼如下：

// pair表示這一對點 if (neighborTable.get(pair) == 0) {neighborTable.remove(pair); }

• 在邊集構造完畢之后，可以開始構造二維數組鄰接表：

private void initMap() {for (int i = 0; i < distinct.size(); i++) {for (int j = 0; j <= i; j++) {if (i == j) {map[i][j] = 0;} else {int nodei = indexNode.get(i); // index 2 nodeint nodej = indexNode.get(j); // 是一種從數組索引到實際節點編號的映射if (containsEdge(nodei, nodej)) { // 鄰接map[i][j] = 1;map[j][i] = 1;} else { // 不鄰接，則為無窮大，這里選擇250是因為不可能會有兩個點的最短路徑大于點數-1map[i][j] = 250; map[j][i] = 250;}}}}}

Floyd算法或者Dijkstra算法
本身理解起來比較簡單，就是把兩個點之間新增一個中轉站之后能比原來的路徑更長，如果有比已經存下的路徑更短的就更新最短路徑。
關鍵點在于幾個可以優化的地方。首先，一個完整的Floyd本身的復雜度是O(n^3)，但是由于題目的簡化，實際上我們可以把它的復雜度的常系數減小。見注釋。

private void Floyd() {for (int mid = 0; mid < distinct.size(); mid++) {for (int i = 0; i < distinct.size(); i++) {// 第一處，j<i，可以借助無向圖的矩陣對稱性來將復雜度的常系數減小一半。for (int j = 0; j < i; j++) {// 第二處，如果兩個點之間的距離已經是1，即他們通過一條邊相連，那么就不存在有一個點，能夠滿足floyd優化條件。所以直接跳過 if (map[i][j] == 1) {continue;}// 第三處，如果這個中間點無法到達這兩個待優化的點，那么這個中間點一定不能優化這一條路徑。所以直接跳過if (map[i][mid] < 250 && map[mid][j] < 250) {if (map[i][j] > map[i][mid] + map[mid][j]) {// 此處也是利用了矩陣的對稱性，所以要同時改變對稱的兩個元素。map[i][j] = map[i][mid] + map[mid][j];map[j][i] = map[i][mid] + map[mid][j];}}}}}}

雖然縮小了常系數到原先的一半以內，但是他的復雜度還是O(n^3)，還是非常可觀的。

最低票價、最少換乘、最小不滿意度

這三個我用的是同樣的方法cal()，只是改變了其中的變量所表示的帶權圖和換乘時候的代價。
在調用這個方法的時候，必須指定指令，type是一個枚舉類型。

enum Type {TRANSFER, TICKET, UNPLEASANT }

在計算這三條指令的時候我用的是Dijkstra算法。它的復雜度實際上和Floyd差不多。計算單點最優是O(n^2)。所以當查詢數目少的時候，會比Floyd浪費的計算量更少一些。
只需要在計算之前詢問，以該點為起始點的該指令的最優是否已經被計算過，并且沒有圖結構的更改。如果圖結構沒有更改，并且這個點為起始點的Dij已經計算過，那么就不必進行重復計算，可以直接輸出相應二維矩陣的結果。截取相關代碼片如下。

// 檢查圖結構是否被更改。// 如果被更改，就初始化三個帶權圖，也初始化用于標記是否已經計算過最優的標記數組。checkMapModified(); // 如果沒有計算過以這個點為起點的Dijif (!counted[index1]) {// 那么就計算DijaskedMap = cal(Type.EXAMPLE, index1);// 并且把這個點標記為已計算counted[index1] = true;}// 如果已經計算過，那就輸出詢問的指令的對應結果return askedMap[index1][index2];

然后根據指令類型來選擇合適的帶權圖map，以及換乘代價w。

private int[][] cal(Type type, int index1) {// 選擇合適的二維矩陣 map 和換乘代價 wint w = 0;int[][] map = new int[1][1];if (type == Type.TRANSFER) {map = transferMap;} else if (type == Type.TICKET) {map = ticketMap;w = 2;} else if (type == Type.UNPLEASANT) {map = unpleasantMap;w = 32;}// Dijkstra 算法省略return map;}

復雜度優化

因為圖結構變更的指令數被限制，而詢問的指令數非常多，因此必須把復雜度都放在圖結構變更的指令中，盡量減少詢問的復雜度。所以在每一次add路徑的時候，就計算他們各自的三個小矩陣——單條路徑三種指令的結果。然后在詢問的時候，現將所有小矩陣的值整合進大矩陣中，作為矩陣的初始化，然后計算大矩陣中的結果。這樣可以省略大矩陣計算中，對于每條路徑、每個點的從頭的初始化，而是每條路徑已經算好各自的最低票價等等，作為一個打包好的完整的小矩陣傳遞給大矩陣，只需要注意小矩陣的nodeid和index的映射關系與大矩陣中的不同即可。而在刪除路徑的時候也是同樣，因為路徑被刪除，而小矩陣是封裝在路徑中的三個數據成員，也被同時刪除。

按照作業分析代碼實現的bug和修復情況

• 兩個對象的比較
  Pair是Java自帶的一個類。與Hashmap非常類似。它的key和value我雖然設置的是integer類型，這是int的一個包裝類，但是不能直接用等號比較數值大小，因為他會比較hashcode而不是數值本身。所以應該重寫比較，可以重寫運算符但這比較麻煩，可以利用已有的方法比如compareTo()，或者自定義一個比較的方式，僅對數值本身進行比對。
• 更新矩陣的合適時機
  由于我的圖結構變更指令和計算最短路徑之類的不在一個類里進行，所以必須通過傳信號值的方式進行交互。在查詢指令進入的時候，先詢問另一個類，是否有圖結構的變更，如果有的話就初始化計算相關的mark，如果沒有變更，就按現有的圖進行計算。
  我原來的錯誤代碼摘抄如下：

if (neighborTable.containsKey(pair)) { // 如果在鄰接表中本來就有這個邊neighborTable.put(pair, neighborTable.get(pair) + 1); // 那么就讓這個邊出現的次數+1，其實次數與鄰接表的元素是1還是0并沒有太大的關系，只是方便在圖結構變更的時候進行更新和統計 } else { // 如果在鄰接表中本來就沒有這個邊neighborTable.put(pair, 1);// 那么就把這個邊放入鄰接表中updatedThere = false;// 并且在另一個類里的計算都要重新來過 }

但是實際上在每次圖結構變更的時候都需要更新另一個類里的計算，因為關系到換乘，即路徑本身的更換，而不僅僅是鄰接邊的問題。所以在每次路徑的添加與刪除的時候都需要重新計算三個指令相關的矩陣。
所以正確的代碼應如下：

if (neighborTable.containsKey(pair)) { neighborTable.put(pair, neighborTable.get(pair) + 1); } else {neighborTable.put(pair, 1); } updatedThere = false;

• Floyd和Dij算法上出現的問題
  這個是我朋友碰到的問題，她自己并不能發現這個bug，因為整個程序是她寫的，所以他會忽視一些她自己覺得很對絕對不可能出錯的部分，但是往往這些被忽視的部分一旦出現錯誤就很難被發覺。而別人去看她的代碼的時候我會從頭開始捋一遍她的邏輯，就能很好的發現問題。
  就是在優化的時候，我們通常來說可以通過圖的對稱性來減小一半的復雜度，以及在確定已經是直接連通的邊的時候就不需要繼續計算。或者可以參考網上其他一些對Floyd、Dij的優化方案，比如利用堆排序、上三角等。
  每次都有bug但還是AC了所有強測點我覺得自己非常僥幸。其實還是對邏輯的不清晰。以后在設計各個數據成員、信號的時候，必須明確每一個信號的作用和值變化的時機，其實JML就在做這個事情。

關于JUnit測試

使用JUnit測試的時候，因為我們已經寫了JML，所以在劃分等價類的時候會更加容易一些。這樣有利于我們構造盡量覆蓋所有組合情況的測試集。

實際上，針對不同的實現思路，適合每個程序的測試類的劃分也是不同的。就我個人的數據結構而言，劃分等價類如下。

containsEdge

兩點都在圖中

• from == to
  • 邊存在
  • 邊不存在
• from != to
  • 邊存在
  • 邊不存在

有點不在圖中

因為我的做法是把所有的邊都放進一個Hashmap中，所以如果碰到from == to這種邊，會給同一個key增加兩次value，而實際上他們的邊只出現了一次。會導致出錯。

isConnected & getShortestPathLength
這個方法在實現的時候我先構造的鄰接表，然后計算了最短路徑，如果最短路徑不是無窮大那就說明是連通的。
所以測試這個方法的劃分與最短路徑可以一起。

兩點都在圖中

• 存在邊可以直接相連 - 測試鄰接表的構造
• 不存在直接相連的邊但是可達 - 測試最短路徑FLoyd的正確性

有點不在圖中。

from==to

• 可達
• 不可達

地鐵系統的三個方法
這三個有異曲同工之妙，其實用的都是同一套方法。

兩點都在圖中

• 不換乘
• 需要換乘
  • A 換乘 B 又換乘 C
  • A 換乘 B 又換乘 A

有點不在圖中

指令排列組合
實際上，測試單個方法很少出錯，最容易出錯的是指令組合之后，什么時候需要計算，什么時候需要更新的邏輯問題。

圖結構變更指令
在這里我有出現過一個bug，究其原因，是沒分清各個指令在什么時候應該重置初始化。
是否可達，以及最短路徑，以及連通塊數目，應該是在鄰接表變更的時候重新算一遍。
而其他關系到換乘的指令，應該是有路徑的增刪的時候就應該重新算一遍。
所以測試集應該這樣劃分：

add + isConnected
add + blockCount
add + getShortestPathLength

add + price
add + transfer
add + unpleasant
其中的add還應該更換成remove再檢查一遍。

在利用JUnit進行測試的時候，利用斷言來檢查各個測試用例是否正確執行。

闡述對規格撰寫和理解上的心得體會

規格很煩，但是很棒。我很喜歡這種契約式的思想，以及在編寫代碼之前就把這個方法或者這個類設計好，設計充分之后再著手思考應該用怎樣的算法去實現，避免重構。

• 首先可以將每個方法的功能劃分清楚，避免重復。
• 其次，在設計過程中，不去想如何實現的問題，不會受到具體算法過程的干擾，這樣就能把關注點傾注在功能本身，在設計的時候思路更清晰。
• 副作用清晰明確。我的其中一個bug就是在add和remove路徑的時候，除了往PathContainer里放路徑或者刪路徑，還有一些其他的附加操作，比如更新一些信號量。這些信號量的選擇性更新，對于代碼邏輯也是一個challenge。如果我在寫代碼之前，把這個信號量在什么情況下會發生變更都搞清楚的話，就不太可能會發生這種邏輯上的錯誤。
• 設計與實現分離。在設計規格的時候和代碼編寫的時候會側重不同的角度去思考問題，各有優劣。在設計的時候更考慮數據的輸入和產出，但是在寫代碼的時候可能更考慮的是每一步的正確性。
• 自動化生成程序及測試。形式化的軟件規格說明能使用特定的軟件，自動生成程序和測試集，可以大大方便寫程序這個過程。

轉載于:https://www.cnblogs.com/ffchyan/p/10899331.html

總結

以上是生活随笔為你收集整理的OO Unit 3 JML的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。