目錄

目錄一、JML語言的理論基礎二、應用工具鏈三、部署SMT Solver四、部署JMLUnitNG/JMLUnit五、三次作業分析第一次作業第二次作業第三次作業六、總結與心得體會

一、JML語言的理論基礎

　　JML（Java Modeling Language）是一種形式化的、面向Java的行為接口規格語言（Behavior Interface Specification Language，BISL），基于Larch方法構建。BLSL提供了對方法和類型的規格定義手段。它允許在規格中混合使用Java語法成分和JML引入的語法成分。JML使用Javadoc的注釋方式，通過一些符號描述方法的預期功能，而不管它如何實現。JML將過程性的思考延伸到方法設計中，從而擴展了面向對象設計的這個原則。

　　JML引入了大量描述行為的結構，如前置條件、后置條件、模型域、正常行為、異常行為等，這些結構使得JML非常強大。更多JML行為結構參考JML Level0手冊。

　　下面列舉常用JML語法。

• Precondition

  • /@ requires P; @/

• Postcondition

  • /@ ensures P; @/

• Side-Effects

  • /@ assignable list;@/

• Exception

  • /@ signal (Exception e) P;@/

• Invariant

  • /@ invariant P; @/

• Constraint

  • /@ constraint P; @/

• method result reference

  • \result

• Previous expression value

  • \old(E)

• Using private fields in specifications

  • private /@ spec_public @/ Type property;

• Fields not null

  • Private /@ not_null @/ Type property;

• Declare spec variable

  • //@ public model Type x;

• Quantifiers

  • Iterating over all variables

    • (\forall T x; R(x); P(x))

  • Verifying if exist variables

    • (\exists T x; R(x); P(x))

  • Num of elements

    • (\num_of T x; R(x); P(x))

  • Sum of expression

    • (\sum T x; R(x); E)

　　

二、應用工具鏈

• OpenJML使用SMT Solver規格驗證

• JMLUnitNG生成TestNG測試用例進行測試

• ...

  ?

三、部署SMT Solver

　　本節openjml的學習參考了倫佬的貼子：OpenJML 基本使用，采用的SMT Solver為z4-4.7.1。

?

• 符合規格但代碼中存在漏洞

  如下是一份符合規格但含有減法溢出的代碼

  　　運行靜態檢查結果如下

  　　成功檢測出了減法溢出錯誤

  ?

• 不符合規格的檢測

  如下代碼邏輯與規格不符

  　　檢測結果如下

  ?

• 符合規格要求且無漏洞的檢測

  　　檢測結果如下（沒有結果就是好的結果

  ?

四、部署JMLUnitNG/JMLUnit

　　本節參考了倫佬的貼子：使用 JMLUnitNG 生成 TestNG 測試樣例

　　以第十次作業為例，采用maven文件結構。

• 初始文件目錄樹

?

• 使用jmlunitng生成測試文件

jmlunitng -cp specs-homework-2-1.2-raw-jar-with-dependencies.jar -d test/java/ main/java/*.java

　　生成測試文件后的文件目錄樹如下（由于生成的文件比較多，只展示部分）

?

• 在IDEA中創建TestNG運行配置并運行測試

　　測試結果如下（居然沒有一個類完全pass。。。）。以及對于第一行的報錯信息，參考倫佬的解釋：“測試結果的第一行是 racEnabled 的測試，意在檢測我們的主文件是否帶有 JML 的運行時檢查。”

?

• 部分測試結果分析

　　以下提取MyGraph的測試結果進行分析。

　　第一個被檢測出的錯誤是addPath()方法傳入空Path時的錯誤

　　本人的MyGraph.addPath()源代碼如下

　　該方法調用了父類（本人的MyGraph類繼承了第一次作業中的MyPathContainer類）的addPath方法，本以為考慮了path為null的情況，卻忘記MyPathContainer.addPath()在path為null時返回的是0，而path為null并沒有終止MyGraph.addPath()的行為，故有可能產生錯誤。

　　　之后還有一排齊刷刷的報錯，但實際上不是getShortestPath()模塊中的錯誤，而是由于按照JML要求拋出了相關異常被捕獲報的錯（isConnected()方法調用了getShortestPath()，有是否有最短路判斷是否連通，故也有報錯）。由于Jmlunitng產生的測試用例是單元測試用例，捕捉到異常會報錯，而不經過課程提供的I/O接口，所以才會出現這些讓人看了極度不適卻又無可奈何的報錯。

?

• 小結

　　Jmluning是個十分得力的助手，或許由于沒有深入挖掘，看法可能還比較片面。

　　Jmlunitng生成的都是一些邊緣數據，如int的邊界值，null等，對于程序中一些微小的、無法察覺的bug爆破還是有十分可觀的作用的。但對于復雜邏輯、模塊間依賴的檢測，也許就幫不上什么大忙，甚至是幫倒忙（比如上述getShortestPath()抓到本應該拋出的NodeIdNotFound異常，卻直接給我Test failed了。。。也許之后隨著使用的深入，能夠發現它更多的優點，或者是成為改進它的一員。

?

五、三次作業分析

第一次作業

1. 架構設計

　　第一次作業較為簡單，但由于沒有充分考慮數據結構對時間復雜度的影響，因此在陰溝里翻了船。 　　第一次作業在MyPath類中用兩個ArrayList分別存儲路徑中所有的結點和不同的結點，在MyPathContainer中采用雙HashMap的形式存儲路徑Map與路徑IdMap，并用一個distinctNodeNum域存儲不同的結點數，在每次增刪時更新（由于更新時采用ArrayList作為存儲中間結果的數據結構，導致了TLE，詳細分分析在下文敘述）。

?

2. 類圖

3. 經典OO度量

?ev(G)iv(G)v(G)

Total	36	35	47

? ? ?其中MyPath.compareTo和MyPath.equals方法復雜度較高，原因是在其中使用了許多條件判斷語句判斷路徑等價或大小，后兩次作業由于保留了MyPath類，故也保留了這兩個高復雜度的方法。

?

4. Bug修復

　　本次作業中強測CTLE了一半的數據，原因是MyPathContainer.countDistinctNodes()方法中使用了不合理的中間數據結構存儲不同的結點。

　　在該方法中采用ArrayList來臨時存儲路徑中不同的結點，遍歷了MyPathContainer中所有的路徑，并遍歷路徑中所有的結點，用ArrayList.contains()方法判斷是否已有該點，沒有則加入。而問題就出在contains()方法上，它需要遍歷ArrayList中的所有元素。總共三層循環，導致了cpu時間的爆炸

　　改進方法是將存儲中間結果的數據結構改為HashSet，它的contains()方法是O(1)的，且其實不需要調用contains()，HashSet.add()會排除重復元素，最終只需兩層循環（遍歷路徑與遍歷結點）即可完成distinctNode的計數。

?

第二次作業

1. 架構設計

　　第二次作業為了能夠滿足課程教學中類型層次迭代的設計，沒有選擇重構，而是在修復第一次作業的Bug的基礎上采用繼承的方式實現MyGraph。

　　在MyGraph類中配置了圖計算類MyGraphCalc的對象進行相關圖類運算，以及boolean型成員latest記錄圖計算對象中數據的更新狀態。MyGraph中增刪路徑時對圖計算類做相應的更新，獲取圖相關數據（最短路徑、連通狀態等）時，先判斷數據是否是最新狀態，若沒有則更新圖計算對象，后再從中獲取數據。

　　MyGraphCalc圖計算類采用HashMap<Integer, HashMap<Integer, Integer>>的雙層HashMap形式存儲圖的鄰接矩陣、最短路徑矩陣，并配置更新、訪問方法。考慮到圖更新指令數遠小于圖訪問指令數，最短路徑的算法選擇了Floyd，一勞永逸。

?

2. 類圖

3. 經典OO度量

?ev(G)iv(G)v(G)

Total	60	63	86

?

4. Bug修復

　　強測中雖然有幸沒有TLE，但有幾組數據居然跑到了15s+的驚人CPU時間，得知HashMap的增刪可能比較耗時，遂在MyGraphCalc中采用靜態數組存儲數據，并配置一個HashMap做下標轉換，在Bug修復中預覽測試后發現，那幾組差點跑崩的數據的CPU時間都減少到了5s左右。

?

第三次作業

1. 架構設計

　　第三次作業依靠討論區大神給出的不拆點的方法完成（貼子)，并使用了Maven創建項目。

　　文件目錄樹如下：

?

　　本次需實現的MyRailwaySystem仍采用繼承的方式，在第二次作業的基礎上繼續填充。在MyRailwaySystem類中仍配置得力助手MyRailwayCalc負責地鐵相關數據的存儲與運算，他們的協同方式仍如第二次作業一樣，MyRailwaySystem接受Path，并提交給MyRailwayCalc進行存儲與運算，在申請數據時從MyRailwayCalc中獲取。區別在于，本次作業將數據更新狀態交由MyRailwayCalc維護，而MyRailwaySystem只行駛領導的職責，分配任務，而不必管工作進度。

　　由于本次作業有4種主要數據需要計算，即ConnectBlock, LeastTicketPrice, LeastTransfer, LeastUnpleasant，故將這4種數據抽象為類，并統一繼承抽象類RailData。抽象類RailData制定了地鐵數據的行為綱領：初始化與更新策略。

　　連通塊數的運算采用路徑壓縮的并查集算法實現，三種最短路都采用Floyd最短路算法（Floyd作為靜態方法封裝在MyGraphCalc中），且都需要在路徑內建圖獲取單條路徑內的最短路。對于最少換乘，路徑內建圖只需將路徑變為完全圖；對于最少票數，路徑內建圖邊權為最短路，故采用第二次作業已實現的MyGraphCalc進行路徑內建圖；對于最少不滿意度，由于邊權運算較復雜，故開了一個新類MyGraphCalcWithWeight繼承MyGraphCalc，進行最少不滿意度的路徑內建圖。三個最短路問題都采用靜態數組存儲數據，并統一使用MYGraphCalc中的下標轉換方法進行轉換。

?

2. 類圖

• 總類圖

• calculator包

?

• container包

• raildata包

?

3. 經典OO度量

?ev(G)iv(G)v(G)

Total	129	145	182

?

4. Bug修復

　　本次作業強測與互測均未被發現Bug。

　　本次嘗試了Junit單元測試，在強測前達到了96%的代碼覆蓋率，剩余未覆蓋代碼為邏輯無法到達的地帶，或是無需實現的方法。

?

六、總結與心得體會

　　本單元的三次作業都是在給定規格的基礎上，實現代碼的填充。總的來說，擁有JML所規約的框架之后，無論是設計的合理性還是正確性的保證，都不會有太大的偏差。

　　但是實現JML規格的過程中也面臨了一個問題，也就是個人對方法功能的實現與規格規約之間的矛盾。規格采用某種數據結構來描述行為，但是個人實現方法時采用另一種實現功能的邏輯，雖然沒有按照規格的邏輯，但完成了相同的功能，此時就無法按照規格的邏輯去檢驗正確性，使用外部工具（如openjml）也會瘋狂報錯，這也就失去了規格通過邏輯檢驗代碼正確性的初衷。

　　其次，由于需要通過數理邏輯去描述一個模塊的功能，在復雜程序設計的過程中，JML規格就變成了一種“加密“，設計者花費心力描述大段規格，實現者也要花費同等甚至更多的時間精力去”解密“這些規格，最后得出這個模塊的功能，無疑增加了項目完成的時間成本。對于本人而言，第三次作業的四個大問題更多的是參照指導書給出的解釋完成模塊的功能，時間與個人能力不允許我去完整閱讀所有規格代碼之后再去動手實現。

　　以上的看法還是比較片面，僅是一個JML初學者的觀點。也許在深入學習之后，會發現JML的更多不可思議的強大之處。

轉載于:https://www.cnblogs.com/kingkongk/p/10905473.html

總結

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

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