用Maven+IDEA+Eclipse組合得到最好的OpenJML體驗

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」就表示違反了規格中的限定。