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 estjava文件夹下，将测试和源代码分开。
如果单元测试中有对多个类的测试文件，只需要按照下面图中的步骤添加一个跑所有单元测试的配置便能一键运行所有测试：
导入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”就表示违反了规格中的限定。