BUAA_OO第三單元作業總結——JML

單元任務

? ? ? ? 本單元的主要內容是熟悉JML相關的理論知識，能夠根據JML規格實現對應方法，通過一步步實現地鐵系統來熟悉JML規格。

一、JML語言的理論基礎、應用工具鏈

1.?JML語言的理論基礎

? ? ? ? JML(Java Modeling Language)是用于對Java程序進行規格化設計的一種表示語言。JML是一種行為接口規格語言（Behavior Interface Specification Language，BISL），基于Larch方法構建。BISL提供了對方法和類型的規格定義手段。所謂接口即一個方法或類型外部可見的內容。JML主要由Leavens教授在Larch上的工作，并融入了BetrandMeyer， John Guttag等人關于Design by Contract的研究成果。近年來，JML持續受到關注，為嚴格的程序設計提供了一套行之有效的方法。通過JML及其支持工具，不僅可以基于規格自動構造測試用例，并整合了SMT Solver等工具以靜態方式來檢查代碼實現對規格的滿足情況。

一般而言，JML有兩種主要的用法：

• 開展規格化設計。這樣交給代碼實現人員的將不是可能帶有內在模糊性的自然語言描述，而是邏輯嚴格的規格。
• 針對已有的代碼實現，書寫其對應的規格，從而提高代碼的可維護性。這在遺留代碼的維護方面具有特別重要的意義。

1.1 原子表達式

• \result表達式：表示一個非void 類型的方法執行所獲得的結果，即方法執行后的返回值。
• \old( expr )表達式：用來表示一個表達式expr 在相應方法執行前的取值。

1.2 量化表達式

• \forall表達式：全稱量詞修飾的表達式，表示對于給定范圍內的元素，每個元素都滿足相應的約束。
• \exists表達式：存在量詞修飾的表達式，表示對于給定范圍內的元素，存在某個元素滿足相應的約束。
• \sum表達式：返回給定范圍內的表達式的和。
• \max表達式：返回給定范圍內的表達式的最大值。
• \min表達式：返回給定范圍內的表達式的最小值。

1.3 集合表達式

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

1.4 操作符

• 子類型關系操作符：E1<:E2，如果類型E1是類型E2的子類型(sub type)，則該表達式的結果為真，否則為假。
• 等價關系操作符：b_expr1<==>b_expr2或者b_expr1<=!=>b_expr2，其中b_expr1和b_expr2都是布爾表達式，這兩個表達式的意思是b_expr1==b_expr2或者b_expr1!=b_expr2。
• 推理操作符：b_expr1==>b_expr2或者b_expr2<==b_expr1。對于表達式b_expr1==>b_expr2而言，當b_expr1==false，或者b_expr1==true且b_expr2==true時，整個表達式的值為true。
• \nothing指示一個空集；\everything指示一個全集，即包括當前作用域下能夠訪問到的所有變量。

1.5 方法規格

• 前置條件通過requires子句來表示： requires P; 。其中requires是JML關鍵詞，表達的意思是“要求調用者確保P為真”。
• 后置條件通過ensures子句來表示： ensures P; 。其中ensures是JML關鍵詞，表達的意思是“方法實現者確保方法執行返回結果一定滿足謂詞P的要求，即確保P為真”。
• 副作用指方法在執行過程中會修改對象的屬性數據或者類的靜態成員數據，從而給后續方法的執行帶來影響。使用關鍵詞assignable或者modifiable。
• 為了有效的區分方法的正常功能行為和異常行為，public normal_behavior 表示接下來的部分對方法的正常功能給出規格，public exceptional_behavior表示對異常功能給出規格。
• signals子句的結構為signals (***Exception e) b_expr，意思是當b_expr為true時，方法會拋出括號中給出的相應異常e。

1.6 類型規格

• 不變式（invariant）是要求在所有可見狀態下都必須滿足的特性，語法上定義invariant P，其中invariant 為關鍵詞，P為謂詞。
• 狀態變化約束constraint對前序可見狀態和當前可見狀態的關系進行約束。

該部分內容摘自JML Level 0手冊。

?

2.?應用工具鏈

Java可以用來指定Java模塊的行為（如DBC協議中的設計）。它有許多工具來進行斷言檢查、文檔生成、單元測試、靜態檢查、驗證等。

下面是通用JML工具版本中每個工具的Unix樣式手冊頁。手冊的每一頁都有一些關于如何使用該工具的信息，并指定了它們的選項和參數。

• jml-launcher：圖形用戶界面工具的啟動程序。
• jml和jml-gui：檢查器。
• jmlc和jml-gui：編譯用于運行時斷言檢查。
• jmldoc和jmldoc-gui：包含JML規范信息的JavaDoc版本。
• jmle：為執行或原型化規范而編譯。
• jmlrac：Java版本，VM，包括類路徑中的BI/JMLRunTime.JAR文件，用于運行用JMLC編譯的文件。
• jmlre：Java版本，VM，包括執行規范所需的運行時支持，用于運行用JMLE編譯的文件。
• jmlspec和jmlspec-gui：從Java源文件生成骨架規范文件。
• jmlunit和jmlunit gui：生成用于JUnit的單元測試代碼存根。
• jtest：結合jmlc和jmlunit的工作。
• jml-junit：JUnit的Swing用戶界面的一個版本，包括類路徑中的bin/jmluntime.jar和bin/jmljunitruntime.jar文件，用于對用jmlc編譯的文件和jmlunit生成的測試用例運行基于jml和junit的測試。

該部分內容摘自http://www.eecs.ucf.edu/~leavens/JML/documentation.shtml

?

二、部署SMT Solver

在部署OpenJML上花了兩天時間，試了各種方法，最后也不知道自己到底是不是部署成功了，在測試的過程中出現了各種問題。

因為第二次和第三次作業中都有自己定義的類，每次檢查到自己定義的類時，就會出現找不到符號的錯誤，因此只好測試第一次作業中的代碼。

測試GjxPath中的equals()方法

推測可能是因為接口Path聲明中不包含nodes，因此找不到符號。

因為GjxPath沒有通過檢查，所以無法進行靜態分析。因此，我使用Demo1.java來嘗試靜態分析，該段代碼來自第九次作業討論區。

package demo;public class Demo1 {/*@@ public normal_behaviour@ requires lhs>0 && rhs<0;*/public static int compare(int lhs, int rhs) {return lhs - rhs;}public static void main(String[] args) {compare(114514, 1919810);} }

靜態分析的結果如下：

第一個警告是因為減法可能會產生越界，后面的警告還沒有搞清楚。

?

三、部署JMLUnitNG/JMLUnit

因為三次作業的代碼在openJML檢查中都沒有通過，因此無法實現自動生成測試用例，此處依舊是通過上文中的Demo1.java來進行嘗試。

依次輸入以下指令

java -jar jmlunitng.jar src/demo/Demo1.java javac -cp jmlunitng.jar src/demo/Demo1_JML_Data/*.java src/demo/*.java

生成以下文件

在idea中運行Demo1_JML_Test.java文件，得到運行結果

可以看出對于整數型參數，主要是通過邊界數據，如-2147483647和2147483647，以及特殊數據0，來測試程序是否正確執行。

?

四、架構設計

1. 第一次作業

本次作業的結構沒有什么可說的，只是完成了基本要求的Path類和PathContainer類。ArrayList結構負責進行遍歷，HashSet結構負責統計不同節點的個數。

? ? ? ?需要注意的是，因為這個單元的作業都有嚴格限制CPU運行時間，所以像distinctNodeCount()方法，如果每次都去遍歷一遍，極有可能會超時，因此通過參考討論區大佬們的討論，添加了HashSet結構來進行節點數量的統計，避免每次遍歷，將時間復雜度分攤在構造函數和addPath()和removePath()方法中。

?

2. 第二次作業

本次作業在架構上與上次作業差不多，只添加了一個類便于統計邊。

本次作業在上次作業的基礎上添加了計算距離和連通性的功能，我的實現方法是建立鄰接矩陣，通過鄰接矩陣計算距離矩陣。

距離矩陣是通過可達矩陣得來的，設可達矩陣為R，鄰接矩陣為A，則有

R=binary(I+A+A²+A³+…+Aⁿ)

對于矩陣A^k，A^k[i][j]表示從節點i到節點j長度為k的路徑數量，因此對于距離矩陣D，當A^k[i][j]第一次出現非0元素時，D[i][j]即為該次方數k。

? ? ? ?在代碼實現的過程中，鄰接矩陣和距離矩陣是通過int型二維數組存儲的，每次添加和移除邊的時候需要重新計算一次距離矩陣。因為沒有使用HashMap結構進行映射，導致我每次都需要通過遍歷來查找nodeId對應的index，造成了很多時間上的浪費。同時，因為沒有進行映射，每次移除節點的時候還需要對鄰接矩陣和距離矩陣進行移位。

? ? ? ?這次作業原本應該是通過集成上次的PathContainer類來實現Graph類，但為了節省時間，選擇了直接復制的方式，沒有進行重構，只是添加了幾個方法，重寫了上一次的addPath()、removePath()和removePathById()方法。

3. 第三次作業

? ? ? ?通過類圖可以看出這次作業明顯復雜了，但程序結構依舊與上兩次類似。雖然在發現GjxRailwaySystem類超過500行之后，嘗試使用繼承的方式，但因為實現起來比較復雜，最后還是放棄了，將幾個參數相對少的方法新建了一個類，以此減少GjxRailwaySystem類的行數。

因此，三次作業在架構上沒有什么區別，也沒有進行重構，每次只是在上一次的基礎上重寫和添加一些方法，以實現新的功能。

? ? ? ?這次作業因為涉及最少票價、最少換乘次數、最少乘客不滿意度，每條邊上的權值都各不相同，在看過討論區大佬們的探討后，選擇采取拆點的方法，每個點拆為起點、終點、每條邊上的點，邊上的點根據不同的圖帶有不同的權值，每條邊上的點到終點的權值為0，終點找起點的權值為換乘一個的取值，起點帶每條邊上的點的權值為0，形成拆點之后的四張帶有權值的圖，通過四個矩陣進行存儲。對每張圖執行最短路徑算法，可以求得在不同權值下的最短路徑，即最少票價、最少換乘次數和最少乘客不滿意度。

? ? ? ?吸取了上次超時的教訓，這次在結構上采取了HashMap的結構存儲映射關系，另外創建一個ArrayList來存儲可以使用的index，每次添加點的時候移除第一個，移除點的時候將index添加到ArrayList的末尾處。

? ? ? ?在計算最小結果的時候采取的是Floyd算法（類圖中的dijkstra方法是因為我后來嘗試了一下dijkstra方法，但最后沒有提交，提交的最終版是Floyd算法），但因為拆點導致節點數大量增加，最終CPU還是超時了。

? ? ? ?在計算連通塊個數時，選擇的是并差集的方法，最初每個節點是一個集合，如果兩個點連通，就將兩個集合合并成一個集合，最終統計集合的個數，即為連通塊的個數。

? ? ? ?每次在有添加邊和移除邊的操作時，都需要重新計算連通塊個數以及每張圖的最短路徑。

? ? ? ?在這次和上次作業中都涉及到需要構造自己寫的類的集合，因此需要重寫創建的類的equals()方法。在運行之后，我發現只重寫equals()方法是不夠的，因為集合在判斷兩個元素是否相等的時候，是先判斷兩者的HashCode是否相等，如果HashCode相等再通過equals()方法判斷，因此還需要重寫hashCode()方法。

通過上網查詢得到hashCode()方法可以重寫為下面的形式

public int hashCode() {int result = hashCode;if (result == 0) {result = 17;result = 31 * result + nodeId;result = 31 * result + pathId;hashCode = result;}return result;}

至于為什么最初是17，之后每次乘31，我并沒有查到答案，貌似是一種規定。

?

五、bug分析和修復

• 第一次作業強測沒有bug，也沒有超時。

• 第二次作業出現了兩個邏輯上的bug，主要還是因為在映射上沒有使用類似HashMap的結構，導致在移除邊的時候需要對矩陣進行行的移動和列的移動，在第三次作業中通過使用HashMap結構解決了這個問題。這次作業還出現了CPU運行時間過長的問題，主要原因還是因為沒有使用HashMap結構來存儲映射關系，導致每次都是遍歷查詢，浪費了許多時間，其次，因為使用的是鄰接矩陣和可達矩陣的算法，每次都需要進行矩陣乘法，每次矩陣乘法都是O(n²)的時間復雜度，從時間復雜度角度上是沒有Dijkstra算法快的。

• 第三次作業出現了RUNTIME_ERROR的錯誤，有的是因為拋出了異常，因為空指針的問題，有的完全沒有返回信息，因此到現在還沒搞懂是為什么。超時的問題主要還是因為拆點之后導致節點數急劇增多，每次添加和移除都需要花費大量時間，不知道討論區的大佬究竟是怎么實現的可以把時間縮得那么短。

?

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

? ? ? ?規格在工程上具有很重要的意義，因為規格規定好一個方法的輸入和輸出，對于方法使用者而言，不需要關心方法的具體實現，只需要按照前置條件輸入參數，按照后置條件使用返回值即可。而對于方法實現者而言，不需要關心其他方法的實現，只需要實現規格中規定的功能即可。規格的存在使得團隊分工合作十分便捷，統一接口，實現高內聚低耦合。

? ? ? ?起初以為規格的撰寫十分簡單，就是將文字敘述轉換為邏輯語言，但當真正開始讀和寫JML的時候才發現遠沒有那么簡單。雖然JML和邏輯語言很像，但實際上還是比邏輯語言復雜很多，因為需要描述各個變量在方法執行完之后的結果，邏輯會變得十分復雜。同時因為規格不是程序執行過程的描述，所以在根據程序撰寫規格時需要轉換思維，從執行前和執行后的差別上著手。

? ? ? ?這個單元原本以為按照規格完成代碼會比較簡單，但事實上難點在于圖論方面知識的實現。同時，這個單元的作業都是根據規格寫代碼，在撰寫規格方面還需要練習。

轉載于:https://www.cnblogs.com/gaojiaxuan1998/p/10907620.html

總結

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

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