OpenJML+SMTSolver的形式化驗證想必大家都已經嘗試過了。大家或許體驗的更多的是IDEA上命令行輸出版本的OpenJML插件，但真正得到官方支持的完全版OpenJML是它的Eclipse版插件。Eclipse上的OpenJML可以輕松輸出驗證錯誤信息，提供問題代碼高亮，提供全推導過程，甚至能夠在代碼中給出對有問題的代碼的反例。下面的圖片中均為win10系統OpenJML+z3 4.7.1的輸出結果，左側IDEA的結果只有命令行輸出，而右側Eclipse的結果中左下角為每個函數是否通過驗證的大綱視圖，右下角為單個函數的推導過程，而代碼中光標所在位置則給出了可能有問題的代碼的反例，此處標出currentPid可能會在自增過程中溢出，反例為currentPid等於2147483647時出現錯誤。
雖然Eclipse的OpenJML插件極為好用，但是IDEA方便的代碼編輯又不值得我們為此更換IDE。為了同時使用兩個IDE的方便之處，又免去重復設置項目的煩惱，我們可以使用它們共同識別的項目類型。為此，我們可以使用一種新的項目類型：Maven項目來管理我們的程序。
Maven是什么？
Maven是一個利用項目對象模型（POM）的項目管理工具。它有如下好處：
- 設置簡單：創建、使用一個Maven項目和一個普通Java項目並沒有什么區別。基本的操作都是一致的。
- 它定義了一種標准的目錄結構，源代碼和測試代碼都有默認的路徑，不需要我們手動設置test文件夾。
- 它能方便地定義項目之間的依賴關系，相比於傳統項目通過jar包添加依賴，我們可以直接依賴於某個特定的項目本身，所依賴項目的更新不需要再替換jar包，只需一次git pull。
- 課程中所依賴的課程組庫項目會成為我們項目中的一部分。在項目管理器Project選項卡中除了我們的代碼以外也能看到課程組提供的代碼，讓你在一個編輯器中完成所有操作。
- 它能夠被IDEA、Eclipse等主流IDE自帶支持。一次配置，全部可用。
Maven還有其他很多好處，例如可以幫助維護項目開發周期等等，不過上面這幾個好處就已經足夠我們使用它了。
創建Maven項目
以下步驟均為IDEA內的操作。依然是往常一樣File→New→Project，在New Project中選擇Maven。選好需要的jdk版本，不需要選擇archetype，直接下一步。
下一步中，GroupId可以隨意設置，一般設置為多段的形式，例如“cn.sheryc”；ArtifactId為項目名。設置好這兩項之后next→finish即可。
添加項目依賴
第一次創建Maven項目后需要等待一段時間，耐心等待下方的后台任務條走完即可。創建好項目后，右下角可能會出現Maven projects need to be imported，選擇Enable Auto-Import就好。
在創建好的項目中，我們能看到根目錄下有一個pom.xml文件，那是Maven項目的標志，一個Maven項目正是通過該文件進行管理的。下面我們需要在其中添加課程組給的庫作為依賴。如果你細心的話，會發現課程組在gitlab上不斷更新的庫中也有一個pom.xml，表示它同樣是一個Maven項目，這使得我們添加這個庫變得更加方便。
首先我們需要將課程組的庫導入進系統的.m2目錄下，IDEA的Maven支持能幫我們簡化這個過程。.m2目錄存放了Maven能識別和導入的所有項目，我的理解是它類似於python的pip安裝的目標目錄。將課程組在gitlab上提供的庫git clone到本地任意位置。接着，在IDEA右側的選項卡中找到Maven，點擊，在上面的按鈕中找到“Add Maven Projects”，將課程組提供的庫的pom.xml選中。導入后，我們能看到自己的Project界面多出了課程組提供的庫。
接着我們需要在我們的項目中添加課程組提供庫的依賴。首先在課程組庫的pom.xml下查看該庫的groupId、artifactId和version，它們是導入項目的坐標。將寫有這三項信息的部分復制下來，在自己的pom.xml的<project>標簽內部添加如下代碼（中間一塊是從課程組的pom.xml復制來的）：
<dependencies>
<dependency>
<groupId>oo-course-2019</groupId>
<artifactId>specs-homework-1</artifactId>
<version>1.1-edu</version>
</dependency>
</dependencies>
至此，我們的項目就可以依賴課程組庫中的代碼了。當課程組更新代碼時，我們不需要再通過替換jar的方式跟着替換，而是只需要在課程組庫的文件夾里git pull保持最新狀態即可。當課程組更新了版本號時，也只需同步更改pom.xml中依賴庫的版本號即可。更強大的是，由於我們依賴的是整個庫，所以不需要進行任何改動，OpenJML就能檢測到源代碼中的代碼規格。
當然，我們自己查看助教提供的代碼規格也很簡單：課程組的項目庫已經被添加到了我們的Project中，在我們的Project選項卡中就能看到課程組庫項目中的所有文件了。
創建單元測試
Junit4是課程組推薦的單元測試模塊。IDEA對Junit有着很好的原生支持，所以不需要進行任何配置即可開始使用JUnit。
在希望添加單元測試的類的類名上按alt+enter，選擇create test，testing library選擇Junit4，勾選上需要測試的方法，按需勾選@before和@after，即可生成測試文件。Maven項目中，所有的測試文件都會被自動生成到%PROJECT%\src\test\java文件夾下，將測試和源代碼分開。
如果單元測試中有對多個類的測試文件，只需要按照下面圖中的步驟添加一個跑所有單元測試的配置便能一鍵運行所有測試：
導入Eclipse
Eclipse對Maven同樣有着很好的支持，所以我們直接導入在IDEA中寫好的項目即可完成在兩個IDE中對同一個項目的共享。
在Eclipse中，選擇File→Import...，在Maven中選擇Existing Maven Projects，在彈出的對話框的Root Directory選擇我們項目的根目錄，Eclipse即可自動檢測到pom.xml文件。點擊finish完成導入。在Eclipse中導入項目可能會匪夷所思地探測不到課程組提供的庫，即使它已經顯示在我們項目的Maven dependencies中，這時只需像導入自己的項目一樣再導入一下課程組的Maven項目即可。
導入結束后，就可以愉快地在Eclipse中安裝OpenJML插件，設置好Solver，享受官方親兒子版本的OpenJML檢測啦~
對於OpenJML中的報錯，可以從https://www.openjml.org/documentation/checks.shtml中找到對應解釋。一般“無法建立assertion”就表示違反了規格中的限定。