用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”就表示违反了规格中的限定。