OO第三單元總結——JML規格

1、JML簡介

1.JML語言的理論基礎

• JML(Java Modeling Language)是用於對Java程序進行規格化設計的一種表示語言。JML是一種行爲接口規格語言 （Behavior Interface Specification Language，BISL），基於Larch方法構建。BISL提供了對方法和類型的規格定義手段。

• 通常而言，JML有兩種主要的用法：

　　（1）開展規格化設計。這樣交給代碼實現人員的將不是可能帶有內在模糊性的天然語言描述，而是邏輯嚴格的規格。

　　（2）針對已有的代碼實現，書寫其對應的規格，從而提升代碼的可維護性。這在遺留代碼的維護方面具備特別重要的意義

　基本語言：

　1.註釋結構

　　　　行註釋的表示方式 爲 //@annotation ，塊註釋的方式爲 /* @ annotation @*/ 。

　2.JML表達式

        2.1 原子表達式

         　　\result表達式、\old( expr )表達式、\not_assigned(x,y,...)表達式、\not_modified(x,y,...)表達式、\nonnullelements( container )表達式、\type(type)表達式、\typeof(expr)表達式……

　　 2.2 量化表達式

　　　　\forall表達式、\exists表達式、\sum表達式、\product表達式、\max表達式、\min表達式、\num_of表達式……

　　 2.3 集合表達式

　　　　集合構造表達式：能夠在JML規格中構造一個局部的集合（容器），明確集合中能夠包含的元素。 

　　 2.4 操做符

　　　　(1) 子類型關係操做符： E1<:E2

　　　　(2) 等價關係操做符： b_expr1<==>b_expr2

　　　　(3) 推理操做符： b_expr1==>b_expr2

　　　　(4) 變量引用操做符

　3. 方法規格

　　　　(1) 前置條件(pre-condition)  ： requires P; 。

　　　　(2) 後置條件(post-condition)  ： ensures P; 。

　　　　(3) 反作用範圍限定(side-effects) : assignable 或者 modifiable 。

　4. 類型規格

　　JML針對類型規格定義了多種限制規則，從課程的角度，咱們主要涉及兩類，不變式限制(invariant)和約束限制 (constraints)。不管哪種，類型規格都是針對類型中定義的數據成員所定義的限制規則，一旦違反限制規則，就稱 相應的狀態有錯。

2.工具鏈

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所涵蓋。

 

2、部署SMT Solver進行驗證

略（選作）

3、部署JMLUnitNG並針對Graph接口的實現進行測試

• JMLUnitNG的部署方法仰仗倫佬。

• 如下是測試結果

  [TestNG] Running:
    Command line suite
  
  Passed: racEnabled()
  Passed: constructor MyGraph()
  Passed: <<homework.MyGraph@18ef96>>.addPath(null)
  Passed: <<homework.MyGraph@ba4d54>>.containsEdge(-2147483648, -2147483648)
  Passed: <<homework.MyGraph@de0a01f>>.containsEdge(0, -2147483648)
  Passed: <<homework.MyGraph@4c75cab9>>.containsEdge(2147483647, -2147483648)
  Passed: <<homework.MyGraph@1ef7fe8e>>.containsEdge(-2147483648, 0)
  Passed: <<homework.MyGraph@6f79caec>>.containsEdge(0, 0)
  Passed: <<homework.MyGraph@67117f44>>.containsEdge(2147483647, 0)
  Passed: <<homework.MyGraph@5d3411d>>.containsEdge(-2147483648, 2147483647)
  Passed: <<homework.MyGraph@2471cca7>>.containsEdge(0, 2147483647)
  Passed: <<homework.MyGraph@5fe5c6f>>.containsEdge(2147483647, 2147483647)
  Passed: <<homework.MyGraph@6979e8cb>>.containsNode(-2147483648)
  Passed: <<homework.MyGraph@763d9750>>.containsNode(0)
  Passed: <<homework.MyGraph@2be94b0f>>.containsNode(2147483647)
  Passed: <<homework.MyGraph@d70c109>>.containsPathId(-2147483648)
  Passed: <<homework.MyGraph@17ed40e0>>.containsPathId(0)
  Passed: <<homework.MyGraph@50675690>>.containsPathId(2147483647)
  Skipped: <<homework.MyGraph@31b7dea0>>.containsPath(null)
  Passed: <<homework.MyGraph@3ac42916>>.getDist()
  Passed: <<homework.MyGraph@47d384ee>>.getDistinctNodeCount()
  Passed: <<homework.MyGraph@2d6a9952>>.getGraph()
  Failed: <<homework.MyGraph@22a71081>>.getPathById(-2147483648)
  Failed: <<homework.MyGraph@3930015a>>.getPathById(0)
  Failed: <<homework.MyGraph@629f0666>>.getPathById(2147483647)
  Failed: <<homework.MyGraph@1bc6a36e>>.getPathId(null)
  Failed: <<homework.MyGraph@1ff8b8f>>.getShortestPathLength(-2147483648, -2147483648)
  Failed: <<homework.MyGraph@387c703b>>.getShortestPathLength(0, -2147483648)
  Failed: <<homework.MyGraph@224aed64>>.getShortestPathLength(2147483647, -2147483648)
  Failed: <<homework.MyGraph@c39f790>>.getShortestPathLength(-2147483648, 0)
  Failed: <<homework.MyGraph@71e7a66b>>.getShortestPathLength(0, 0)
  Failed: <<homework.MyGraph@2ac1fdc4>>.getShortestPathLength(2147483647, 0)
  Failed: <<homework.MyGraph@5f150435>>.getShortestPathLength(-2147483648, 2147483647)
  Failed: <<homework.MyGraph@1c53fd30>>.getShortestPathLength(0, 2147483647)
  Failed: <<homework.MyGraph@50cbc42f>>.getShortestPathLength(2147483647, 2147483647)
  Passed: <<homework.MyGraph@75412c2f>>.getUpdateDist()
  Failed: <<homework.MyGraph@282ba1e>>.isConnected(-2147483648, -2147483648)
  Failed: <<homework.MyGraph@13b6d03>>.isConnected(0, -2147483648)
  Failed: <<homework.MyGraph@f5f2bb7>>.isConnected(2147483647, -2147483648)
  Failed: <<homework.MyGraph@73035e27>>.isConnected(-2147483648, 0)
  Failed: <<homework.MyGraph@64c64813>>.isConnected(0, 0)
  Failed: <<homework.MyGraph@3ecf72fd>>.isConnected(2147483647, 0)
  Failed: <<homework.MyGraph@483bf400>>.isConnected(-2147483648, 2147483647)
  Failed: <<homework.MyGraph@21a06946>>.isConnected(0, 2147483647)
  Failed: <<homework.MyGraph@77f03bb1>>.isConnected(2147483647, 2147483647)
  Failed: <<homework.MyGraph@326de728>>.removePathById(-2147483648)
  Failed: <<homework.MyGraph@25618e91>>.removePathById(0)
  Failed: <<homework.MyGraph@7a92922>>.removePathById(2147483647)
  Failed: <<homework.MyGraph@71f2a7d5>>.removePath(null)
  Passed: <<homework.MyGraph@2cfb4a64>>.size()
  
  ===============================================
  Command line suite
  Total tests run: 50, Failures: 26, Skips: 1
  ===============================================

   

• 我還按倫佬的流程，實際操做了一遍。菜菜的我須要反覆練習……

•  

4、梳理框架設計

第一次做業：

老老實實按照官方提供的接口寫的。

 

第二次做業：（下圖是我debug以後的代碼框架。與以前的代碼相比，框架是相同的，只是部分存儲的數據結構不一樣）

做業框架基本和接口同樣。第二次做業主要在MyPathContaineri的基礎上增長了幾個接口，我沒有選擇繼承，而是直接Ctrl C 、Ctrl V了（捂臉）。

第三次做業：

難度提高，這一次的框架仍是按照官方給的接口來寫的。不過我將對圖的操做以及floyd算法的操做封裝成了一個類MyMap類。

這三次做業個人框架是沒變的，第二次和第三次我用的都是鄰接矩陣初始化距離矩陣，利用floyd算法來求最小權重的路徑。不過在第二次做業TLE以後，我發現hashmap在這種算法下遠不如靜態數據運算快，因此第三次做業是用的靜態數組來完成的算法。

 

5、分析代碼實現的bug和修復狀況

第一次做業：

此次做業實現難度不大，關鍵在於複雜度的控制。在此次做業中，我利用了已有的容器(如 hashmap 、hashset等）來減小我本身寫的代碼量。當初想着，這些已經有的容器的算法確定比我寫得強多了，卻沒真正深刻探究容器自身實現的複雜度。

Mypath類中，當須要getDistinctNodeCount時，我都會new一個hashset來統計。這對path這個類來講，確實是比較簡單且複雜度低的方法。

可是我在MyPathContainer 類裏偷懶，依然用的是這個方法。然而MyPathContainer類裏會頻繁地add和remove，致使每當getDistinctNodeCount時，我都會重頭統計，複雜度是O（n）。這一問題讓我在強測中TLE了。

bug修復時，我經過增長一個HashMap存儲當前某個節點出現了多少次，將複雜度分散到add和remove操做中，getDistinctNodeCount時只需輸出當前hashmap的size便可，複雜度降到了O（1）。

 第二次做業：

對於第二次做業新增的方法，我運用的是Floyd算法來完成的。考慮到add和remove的指令佔比很小，選擇Floyd算法是很是合適的，第2、三做業的結果也證明了這一點。

不過此次我仍是TLE了，我入了hashmap的坑。我本想，第二次做業是個稀疏矩陣，用hashmap存儲會更節儉一點。卻萬萬沒想到，在有下標索引的狀況下，靜態數組查詢、更新等的實現速度是遠遠快於hashmap 的。今後，我對hashmap的蜜汁好感產生了動搖……

第三次做業：

這一次做業我機智地沒有選擇拆點法（據說拆點法很難寫並且運行時間過久……）

我選擇了另外一種主流思想，每一條Path連成一個徹底圖存入MyMap中。當初作抉擇的時候，考慮到拆點法是在刪增Path的時候需與圖中幾乎所有的信息比對來動態改變每一個節點的個數，而徹底圖的方法的任何一個操做都是對一個Path獨立的（加是加一個徹底圖，刪是刪一個徹底圖），並不須要與其餘Path進行比較。基於這一點，我以爲徹底圖這種簡單的構圖方式比較適合我。

我估計是對TLE產生了內心陰影，此次我是在我能力範圍內儘量地優化複雜度，結果把本身給優化死了……此次求最少換乘次數、最短路徑（最少票價）、最小不滿意度，都是同一張圖，可是賦三種權值。

由算法的實現可知，每條邊的權值都要是這條邊在它所屬的全部path中權值最小的。我爲每條邊存儲了一個他所屬的Path的id和在這個Path中它的權值的棧。add和remove的時候，給距離矩陣初始化的時候，就會從每一個邊的棧中找到最小的權值給它附上。但是我在我這些優化的時候，由於一些筆誤致使我更新遺漏，強測wa了。

 

6、對規格撰寫和理解上的心得體會

感受規格專業很像離散數學中的謂詞邏輯，因此理解起來並非很難。

主要的體會是：

　　規格只是對結果的描述，卻沒有限定實現的具體方法；

      規格定義中只能調用pure方法，描述的是狀態而非動態過程。