1、JML簡介
1.1 JML與契約式設計
提及JML，就不得不提到契約式設計（Design by Contract）。這種設計模式的始祖是1986年的Eiffel語言。它是一種限定了軟件中每一個元素所必需的責任與義務的開發模式，程序設計中的每一個元素都須要用規範的語言精準地限定其前置條件（Preconditions）、後置條件（Postconditions）和不變式（Invariants）。經過這三項限定，咱們能夠清晰地得到對一個函數功能的刻畫，從而達成設計與實現的分離，便於優化、測試和生成文檔。html
契約式設計的理論基礎是形式驗證、形式規約和霍爾邏輯。在我看來，契約式設計正是形式規約的工程化實現方式，也正是由於有了規範的契約，形式驗證纔可能得以成立。相比於測試驅動編程（Test-Driven Development），契約式設計能經過定理證實器經過形式驗證的方式證實程序的正確性，從而更加可靠。java
契約式設計在不少語言中都有自帶支持，例如Fortress、Perl和Java的新近親Kotlin，其中不少語言都是經過相似於assert斷言的方法進行契約限定的。Java並無自帶的契約式設計模塊，JML做爲仍處於活躍開發中的第三方Java契約式設計模塊能夠填補這一方面的空白。node
JML是一種行爲接口規格語言，能夠藉由一套標準化的帶註解的註釋實現對Java代碼語法接口（即函數名、返回類型、可拋出異常等）和行爲的規範。JML將Eiffel等契約式設計語言的操做性和Java等現代語言的可讀性相結合，利用Java表達式進行規格書寫，並對其進行了必定的擴展，增長了量詞方便規格書寫。git
1.2 JML工具鏈
JML的一大優點就在於其豐富的外圍工具，它們都被羅列在了http://www.eecs.ucf.edu/~leavens/JML//download.shtml上。其中比較重要的幾個以下：程序員
- OpenJML：首選的JML相關工具，以提供全面且支持最新Java標準的JML相關支持爲目標，可以進行靜態規格檢查（ESC，Extended Static Cheking）、運行時規格檢查（RAC，Runtime Assertion Checking）和形式化驗證等一系列功能。OpenJML提供了自帶的命令行版本和Eclipse插件版本。
- JML Editing：官方的Eclipse插件，提供了JML規格的代碼高亮及代碼補全。
- JMLUnitNG：JMLUnit的替代工具，可以根據JML規格自動生成基於測試庫TestNG的單元測試集。
- jmldoc：可以經過JML生成javadoc的工具。現已合併入OpenJML中。
JML還有一系列其餘工具，可是這些工具大都是從不一樣角度根據規格進行代碼測試的，這些功能已被OpenJML所涵蓋。github
2、SMT Solver的使用
利用SMT Solver進行形式化驗證是OpenJML提供的功能之一。該工具備兩種使用方式：使用命令行版本（或經過IDEA的OpenJML/ESC插件間接調用該工具）或使用OpenJML的Eclipse插件。算法
在個人前一篇博客中，我介紹瞭如何利用Maven項目在IDEA和Eclipse間進行項目互通以方便地使用Eclipse插件進行形式化驗證，所以在此省略操做部分。編程
然而，OpenJML存在一些謎同樣的問題，會致使代碼被錯誤地判爲invalid。許多人遇到的size在形式驗證中返回值爲真實值-1的錯誤至今依然讓我感到疑惑，甚至MyPath一樣的代碼和規格，在第9次做業中所有爲valid，然而複製粘貼到第10次做業中就出現了錯判。這也許和OpenJML對JML語法的支持尚不徹底有關，不過我在寫上一篇博客時意外地留下了一張運行無誤的截圖，在此能夠對它進行一下粗略的分析。windows
這是對個人第9次做業全部文件的形式驗證結果，驗證配置爲OpenJML 0.8.42 + z3 Prover 4.7.1。從左下角一片綠色的驗證結果能夠看出，此次做業中MyPath和MyPathContainer兩個類中除了個別方法被判爲invalid外（實際上這些錯誤大部分是由於整數自增溢出），其他方法都可以完美地經過形式化驗證。在這其中，出現錯誤最多也最典型的一個函數是MyPathContainer.addPath()。從代碼中的高亮能夠看到，該函數中存在4處錯誤。這四處錯誤分別爲：設計模式
- 54行：
++currentPid中，因爲currentPid爲int型，故自增可能致使溢出。 - 55行、56行：我在
MyPathContainer的實現中爲了提升id和Path互查的效率，採用了雙HashMap的結構，所以在addPath()中須要對pathToId和idToPath兩個HashMap均進行put()操做。此處報出的兩個錯均爲InvariantLeaveCaller，代表調用一個外部函數時不知足不變式。這一結果出乎意料地正確，由於在調用單個put()操做的中間，因爲已經調用了外部函數，故屬於可見狀態，而在此期間兩個HashMap並未完成統一，因此不變式未達成。不過HashMap.put()做爲jdk自帶方法，這樣的報錯也許是多餘的。 - 58行：在這裏雖然採用了java 8的雙冒號寫法，但內涵依然是
int遞增，仍然可能致使溢出。
因而可知，利用SMT Solver在不出現沒法解釋的所有判錯現象時是很是可靠的，能夠認爲一旦經過了該測試就徹底符合了規格要求，是保險性最高的測試。
3、JMLUnitNG的使用
此處首先感謝討論區倫dalao的分享。
JMLUnitNG雖然是JMLUnit的替代版，但它的功能還沒有開發徹底，使用起來很是複雜，稍有不慎就會讓人完全崩潰。我在使用過程當中遇到了許多難題：
- 該工具的最後一次更新是在2014年，甚至在java 1.8更新前。因爲JMLUnitNG包中自帶了其所有依賴庫，因此其自帶的過舊的OpenJML庫依賴使得其沒法正常分析使用了java 1.8及以後版本的語法，這給測試形成了第一道困難。爲此，我將其依賴的OpenJML工具替換成了截至2019年5月的最新版本0.8.42並從新打了包，感興趣的能夠從個人github上下載：https://github.com/sheryc/JMLUnitNG/releases/tag/v1_5
- 該工具分四步操做：生成測試→編譯→執行rac→測試。在第一步生成測試中，須要添加-cp參數添加庫依賴。根據JMLUnitNG的官方doc，classpath參數的寫法遵循javac寫法，然而實際上在添加多個依賴目錄時，JMLUnitNG採用了對windows系統極爲不友好的冒號分隔方式。這致使以盤符加冒號（如D:\）開頭的絕對路徑沒法做爲JMLUnitNG的-cp參數被傳入。爲了解決這個問題，須要將依賴庫所有放入項目文件夾中。
- JMLUnitNG不容許所分析的文件中帶有GBK字符，而官方接口中每一個函數都有用中文寫的javadoc，刪除註釋的工做量巨大。最終無可奈何轉成了對並不依賴過多官方文件的
MyPath類進行測試。 - 當依賴.jar文件包時，JMLUnitNG沒法檢測到JML規格。爲此我將JML規格複製到了本身的文件中。
- 因爲對OpenJML的依賴，因此OpenJML存在的對一部份量詞沒法驗證的問題天然也繼承到了JMLUnitNG中。爲此須要對規格進行改寫。須要刪去model，在本身的實現中添加
spec_public標識，並改寫或刪除會報錯的\exists和\forall規格。 - 即便解決了以上問題，還會存在JMLUnitNG對於一部分寫法不能識別的問題。在一開始，我在進行rac步驟時會報出一個其餘人都不會報出的錯誤：A catastrophic JML internal error occurred. Please report the bug with as much information as you can. Reason: Mismatch in number of arguments in accumulateTypeInstantiations。通過一段時間控制變量式的探索後，我發現錯誤根源竟在於
Path.equals()中採用的以下for-each循環：
Iterator<Integer> objIter = ((MyPath) obj).iterator();
for (Integer integer : this) {
if (!objIter.next().equals(integer)) {
return false;
}
}
該循環自己寫法並無錯，而且支持了java 1.8語法後應該對for-each循環的判別沒有問題。然而這樣的循環居然會致使OpenJML的內部錯誤，這很是不可理喻。這樣一個錯誤花費了我很長的時間，從第9次做業貫穿到本次總結的寫做，甚至我拜託了幾名同窗幫我進行測試，卻怎麼也沒想到錯誤是因爲OpenJML自己的bug致使的所謂「Catastrophic internal error」。最終我將for-each循環改成了hasNext()循環，解決了這個問題。
最終的測試結果以下：
鼓搗了半天，最後竟然報了構造方法出錯，並且彷佛由於構造器沒法經過測試而跳過了後續的測試？可是MyPath的構造器實際上構造很是簡單，因爲時間緊迫，我也沒有進一步探尋如何修復報出的莫須有的錯誤。不過從後續的測試數據中能夠發現，JMLUnitNG即便在檢測到了JML規格的狀況下，所作的也只有邊界測試，測試覆蓋性極其有限，而且其生成單元測試的依據彷佛不是JML規格，而是函數簽名。
雖然自動生成單元測試的功能很方便，但對於JMLUnitNG這一款工具而言着實雞肋：其高昂的學習代價，漏洞百出的執行過程，毫無體驗感的使用流程，對JML規格並不夠好的支持，以及最終生成的覆蓋度差的測試用例，都不值得讓用戶使用這樣一款半成品工具，也難怪早在5年前這一項目就中止了活躍開發。相比之下，閱讀規格並本身設計單元測試會更加可靠且更加方便。在自行設計單元測試時，咱們能夠仿照JMLUnitNG的測試思路，在覆蓋全部運行分支的基礎上，多設計一些邊界測試和無效測試，而這些在SMT Prover的形式驗證中也經常成爲測試的反例。
4、JUnit的使用
在這幾回做業中，JUnit若是使用到位是能夠對程序驗證起到很是大的幫助的。在此以本身第9次做業的單元測試爲例。經過對測試執行「Run with Coverage」指令，能夠得到單元測試對代碼中全部執行路徑的覆蓋程度：
從右邊的Coverage能夠看出，個人測試對於MyPath和MyPathContainer的代碼覆蓋度分別達到了81%和100%，已經能夠幾乎覆蓋到全部執行分支。而實際上，個人單元測試是在寫代碼前就已經寫好的（很有一種Test-Driven Develop的感受），因此能夠作到測試和代碼的分離。
在設計測試時，須要將不一樣運行分支分在不一樣的方法中進行測試，這也是爲什麼個人函數後面會帶有Normal、Exceptional和編號，這樣能夠在一次執行中最大化發現的問題數量。
單元測試是最底層的測試，在個人理解中，它的做用與方法規格是相輔相成的，都是爲了測試一個函數是否可以知足對該函數的全部要求。恰好在這次做業中每一個函數的功能幾乎是分離的，因此一個覆蓋性好的單元測試對正確性的保證是僅次於形式驗證的。
5、三次做業總結
5.1 第九次做業
5.1.1 實現方案
本次做業須要實現的是Path和PathContainer。
對於Path類，其存在的操做僅爲查詢。對根據下標查詢的操做，選用基於數組的ArrayList能夠達到O(1)複雜度；對查詢節點是否存在/不重複節點個數的操做，選用HashSet能夠達到一次生成後每次查詢都爲O(1)複雜度的目標。
對於外部函數能夠經過iterator()返回的迭代器修改Path的問題，在這裏我記錄了每一次ArrayList的hash碼，當進行HashSet相關查詢操做時，首先比較當前ArrayList的hash碼是否與先前保存的hash碼，若相等則能夠認爲很大機率該Path未通過修改，不然從新構建HashSet。
我在其中使用了一些提升效率的小trick，好比HashSet的構建只有在進行相關查操做時纔開始，這樣能夠省去一些進行無用且耗時的HashMap構建操做的時間。
對於PathContainer類，進行的是少許的增刪操做和大量的查操做。爲此，須要將查操做盡量優化到O(1)複雜度。我採用了idToPath，pathToId雙HashMap以優化兩者之間的雙向查找；與此同時，使用一個單獨的HashMap記錄每一個節點的出現次數，這樣在查詢不重複節點時只需返回該HashMap的size便可。
本次做業的UML類圖以下：
5.1.2 出錯分析
本次做業強測滿分。高工不參加互測。
5.2 第十次做業
5.2.1 實現方案
本次做業中將PathContainer升級爲了須要計算節點間路徑長度的Graph。本來Path和PathContainer的操做依然保持不變。
在本次做業中我本應讓MyGraph繼承上次的MyPathContainer的，但當時我對於繼承時private字段的處理方式理解不到位，因此沒有用這種方式，而是直接將MyPathContainer的代碼複製了過來。如今想來實在是很是不該該。
新增的操做所有是基於兩點間最短距離的，因此計算最短路徑成爲了本次做業的核心。爲此我新建了兩個輔助類：用於壓縮記錄每兩個節點間距離的DistMap和應用圖算法的GraphUtils。
在DistMap中，我將每對節點的距離記錄在了一個HashMap<AbstractMap.SimpleEntry<Node, Node> Integer>的數據結構中（此處Node其實是Integer，這樣寫是爲了理解方便；此外AbstractMap.SimpleEntry是java.util中自帶的Pair類型）。因爲須要存儲的圖是無向圖，其距離矩陣應爲對稱陣，故爲了節約存儲空間 ，存入和查詢時的SimpleEntry都應保證其key<=value，這樣能夠將距離矩陣壓縮一半。
在GraphUtils中，採用基於優先隊列的堆優化的Dijkstra算法。爲此須要在該類中維護一個鄰接矩陣HashMap<Node, HashMap<Node, Integer>>（此處Node其實是Integer，這樣寫是爲了理解方便），其中內層的Integer爲這兩個Node的鄰接次數，這樣能夠在一些刪除重複邊的狀況下忽略其影響。
在使用優先隊列時，實際上能夠用一種更簡單的方式進行初始化。個人優先隊列中存儲的均爲AbstractMap.SimpleEntry<Node, Distance>的形式，故堆的比較依據爲該SimpleEntry的value。此處可使用Java 1.8中新增的雙冒號寫法以簡化代碼：
PriorityQueue<SimpleEntry<Integer, Integer>> remainDist = new PriorityQueue<>(Comparator.comparingInt(SimpleEntry::getValue));
計算全部的距離後，全部新增的查操做均可以經過判斷兩點之間距離的方式達成。須要注意的一點是，有些結點可能存在自環，因此對這樣的結點判斷本身和本身間是否存在邊時應返回true。所以，須要維護一個記錄存在自環的結點的數據結構。
本次做業的UML類圖以下：
5.2.2 出錯分析
本次做業強測滿分。高工不參加互測。
值得一提的是，因爲做業中須要進行n次SSSP計算全圖距離，因此本來的想法是創建一個線程池，多線程運行這些Dijkstra算法。然而，線程池所有線程運行結束的判斷比較複雜，再加上須要優化的並不是實際運行時間而是CPU時間，因此在發現錯誤以後果斷地迴歸了單線程模式。
5.3 第十一次做業
5.3.1 實現方案
本次做業中將Graph升級爲了須要計算換乘距離/連通份量個數的RailwaySystem。本來``Path和Graph`的操做依然保持不變。本次做業我依然錯誤地沒有使用繼承，反省反省。
本次做業新增了三種須要考慮線路換乘的距離計算問題，這三種問題實質上使用的是同一種算法，不同的只有邊權和換乘權重。所以，我將先前的圖計算類GraphUtils改造爲了一個抽象類，保留了Dijkstra算法，而邊權和換乘權重變爲了兩個抽象方法normalCost()和transferCost()，而不一樣的距離計算只須要新建不一樣的圖計算子類override這兩個方法便可。
爲了解決線路換乘的判斷問題，我採用了拆點法，將不一樣線路上的相同節點視爲不一樣結點，這樣每一個點的鄰接點被分爲兩類：在同一條Path上的相鄰點和在不一樣Path上的相同點。爲此，須要：
- 對點進行擴展編號，在其中保存點編號和線路號兩重信息；
- 對每一個點記錄其所在的Path集合方便遍歷；
- 鄰接表中存儲的均爲點的擴展編號，只有在同一Path上相鄰的點纔在鄰接表中進行記錄。
對於擴展編號，我採用了一些小trick。因爲增刪Path的指令最多隻有50個，所以，不須要創建複雜的數據結構，只須要經過一個最低三位記錄線路號，高位記錄節點號的long類型數便可。我創建了靜態類ExtendedNode，經過(long) nodeId * 100 + pathId的方法得到擴展編號；從擴展編號逆推原來的點編號和路徑號時，只需進行除100或模100操做便可，省去了不少IO時間。
相比於上一次做業每作一次增刪路徑操做都從新計算全圖的全部距離，本次我採用了查一個算一個的策略，發現所查詢距離沒有時則跑一次對應圖的SSSP，也能夠節省一些時間。
對於連通份量個數，採用帶路徑壓縮的並查集完成。在刪除結點後，須要從新對並查集進行計算。
本次做業的UML類圖以下：
5.3.2 出錯分析
本次做業強測滿分。高工不參加互測。出乎意料的是此次做業竟然是弱測帶強測一次過，或許是這種清晰的繼承結構帶來的方便吧。
6、感想
在第一單元時，我就聽聞單元測試對於程序驗證的重要性，然而單元測試從何開始設計一直都是個人困惑。在接觸了規格以後，這一問題獲得瞭解決：單元測試應該是面向一個模塊應該完成的全部工做的，而規格恰好爲測試的設計提供了依據。有了規格以後，不管是單元測試仍是場景測試都能很快地定位到出錯位置。
此外，規格還能成爲頂層設計與底層實現之間的橋樑。在開發大型項目時，設計架構事後須要將任務分攤到每一個不一樣的模塊中，撰寫代碼規格有助於理清每一個模塊所需實現的功能，從而更好地耦合；而程序員則不須要考慮模塊與模塊之間的調用邏輯，只須要想辦法完整實現規格便可。
同時，在我看來規格也是依賴反轉的體現之一。實際上方法的調用者須要的是一個被調方法的功能，而不關心其背後的具體實現，這有點相似於接口的用處。有了規格以後，背後的實現方式的更新或是算法的優化都有了不出錯的保證（其實是根據規格所撰寫的完整的單元測試保證了這樣的改寫依然有效）。
在本次做業中，因爲指導書的描述和函數名已經給予了足夠清晰的函數功能定義，因此實際上並不須要徹底理解規格的內涵就能夠完成任務，這樣看來應該是程序文檔對程序員的幫助更大一些，畢竟天然語言更貼合人的思惟。然而，規格的規範性可以讓程序設計者明確一些邊界狀況應該如何處理，以及多數狀況下規格自己就是一個方法功能的最簡單實現，有了文檔和規格的雙重保證才能讓程序設計者可以更快更好地實現功能。
規格的撰寫的確是一大難事，有很大一部分緣由是JML規格並無提供代碼高亮和自動補全，而JML Editing插件也是在寫本次總結的時候才瞭解到的，因此每敲一下鍵盤都要懷疑本身寫的對不對，甚至括號匹配都會成一個大問題。不過JML的優點在於其貼近Java的語法，因此抱着用最淺顯的算法去實現功能的想法反而能很容易地寫出規格。
最後須要吐槽一下JML的工具鏈：除了OpenJML依然在持續更新外，其餘工具都已經徹底跟不上時代了，甚至還有JMLUnitNG這種歷史悠久的半成品直接發佈出來讓人用，實在是體驗極差。此次博客的撰寫比以前任何一次代碼做業都讓人崩潰，其中數次想要放棄，但依然堅持住跑完了全部工具，實屬不易。~~（在這裏感謝湊あくあ等國際友人在這些天裏提供的精神支持）~~或許這說明了契約式設計並非當前的主流設計模式，諸如利用assert進行契約規範或是TTD等模式要比撰寫複雜而不易懂的規範來的簡單直接的多。
最後感謝這次討論區的各位算法dalao提供的算法思路，此次因爲沒對問題分析透徹的緣故，在討論區提供了一個錯誤的算法，還好及時發現了錯誤。這樣的探究在當下仍是有意義的，讓我對SSSP問題有了更清晰的認識。同時也感謝這次提供了各類JML相關工具的dalao，沒有大家這篇博客也就不會是這個樣子了。