【BUAA OO Unit3】史上最全OpenJML摸索实录

史上最全OpenJML摸索实录

本文为笔者OpenJML的安装配置及使用，以及用JunitNG进行自动测试的探索实录。OpenJML及JunitNG这两个工具非常古早，网上资料奇少，与IDEA配适度极差，难用程度令人发指。但是课程博客又不得不用，于是参考17级学长学姐们的教程，结合笔者自己的摸索经验，在这里整理成博客，以方便学弟学妹。

一. OpenJML的安装

  OpenJML是一个检查JML语法，验证代码规格的工具。

  可以通过OpenJML官网(http://www.openjml.org/)进行下载。

二. OpenJML的使用

 2.1 JML语法检查(JML type-checking)

  OpenJML最基础的功能就是对JML的语法进行检查。

java -jar $OPENJML /openjml.jar <options> <files>

较高的Java版本运行OpenJML会出现如下的报错。

  该报错出现的原因是OpenJML开发时的java版本较低，依赖类版本较低的包，因此和名称功能功能一样但是版本较高的包发生的冲突，通过将本地java版本换成JDK8就可以解决。

  每次都通过命令行调用openjml.jar来运行有点麻烦，我们可以通过自定义命令行指令来简化一下操作。

MacOS

  命令行中输入如下指令：

vim ~/.bash_profile

  在.bash_profile中输入：

alias openjml='java -jar YOUR_OPENJML_PATH/openjml.jar'

  运用.bash_profile文件：

source ~/.bash_profile

Linux

# filename : openjml
#!/bin/bash
java -jar YOUR_OPENJML_PATH/openjml.jar "$@"

Windows

::openjml.bat
@echo off

set java=java -jar "%~dp0openjml.jar" -noPurityCheck
set prove=-prover cvc4 -exec "%~dp0Solvers-windowscvc4-1.6.exe"
set runtime=-cp %~dp0jmlruntime.jar;

set allparam=
set rac=

:param
set str=%1
if "%str%"=="" (
    goto end
)
if "%str%"=="-rac" (
	set rac=rac
)
if "%str%"=="-prove" (
	set str=%prove%
)
set allparam=%allparam% %str%
shift /0
goto param

:end
if "%allparam%"=="" (
    goto eof
)

rem remove left right blank
:intercept_left
if "%allparam:~0,1%"==" " set "allparam=%allparam:~1%"&goto intercept_left

:intercept_right
if "%allparam:~-1%"==" " set "allparam=%allparam:~0,-1%"&goto intercept_right

:eof
%java% %allparam%
set filename=
if "%rac%"=="rac" (
	:input
	set /p filename=Input file name:
	if "%filename%"=="" (
		goto input
	)
	java %runtime% %filename%
)


pause

  Linux和Windos用户可以将上述代码拷贝到解压后的文件夹中，然后将该文件夹加入环境变量，参考博客https://www.cnblogs.com/lutingwang/p/openjml_basic.html。

  这样，我们就可以通过openjml命令来运行OpenJML了。

openjml <options> <files>

 2.2 路径参数

• classpath：用于指定openjml.jar的路径，缺省时为当前路径。
• sourcepath：用于指定外部引用文件的路径，缺省时为classpath。
• specspath：用于指定规格文件(.jml文件)的路径，缺省时为sourcepath。

 2.3 静态检查(Extended Static Checking)

  Type-checking仅对JML的语法进行检查，对于规格内容和代码是否符合规格要求时不加检查的，如果需要检查规格内容，就需要用到静态检查(Extended Static Checking)和运行时检查(Runtime Assertion Checking)。

  SMT solver

  SMT是一款基于数理逻辑的用于自动化验证函数正确性的工具，其支持多平台的SMT解释器(SMT-Solver)，其中应用最广泛的平台之一是微软所研发的 z3。

  从官方下载的OpenJML文件夹下已经为我们提供了不同平台不同版本的SMT solver。因为SMT solver并不属于OpenJML的一部分，因此在进行静态检查的时候我们需要告知OpenJML需要使用的solver名称以及路径。

openjml -esc -prover provername -exec solver_path <options> <files>

  参数

• -esc：对规格内容进行检查。
• -prover：指定solver的名称。
• -exec：指定solver的绝对路径。
• -method <methodlist>：对指定的方法列表中的方法进行检查。
• -exclude <methodlist>：不对指定的方法列表中的方法进行检查。
• escMaxWarning int：限定每个方法抛出的最大警告数量。
• -progress -verboseness：输出验证的过程信息。

 2.4 运行时检查(Runtime Assertion Checking)

  执行运行时检查的时候，首先会将被检查的代码编译成可RAC的.class文件，然后运行程序观察是否断言有冲突。

  MacOS

openjml -rac <options> <files>
java -cp FILE_PATH:$OPENJML/jmlruntime.jar <.class>

  Windows

  在windows系统中需要用“;”替换“:”

openjml -rac <options> <files>
java -cp FILE_PATH;$OPENJML/jmlruntime.jar <.class>

  参数

• -racCheckAssumptions：运行时检查时，假设与断言都检查。在运行时检查时，对于一个方法，在其调用和被调用的时候都会进行检查。在默认情况下，会在调用的时候检查前置条件，在被调用的时候检查后置条件。当设置了该参数之后，不管调用还是被调用，都会对前置条件和后置条件进行检查。

  例如对于如下代码：

public class Main {
    public static void main(String[] args) {
        int i=0;
        test1(i);
        test2(i);
    }

    //@ requires i == 1;
    //@ ensures 
esult == 20;
    public static int test1(int i) {
        return 10;
    }

    //@ requires i == 0;
    //@ ensures 
esult == 20;
    public static int test2(int i) {
        return 10;
    }
}

  在不设置racCheckAssumptions参数时的输出如下：

Main.java:4: 警告: JML precondition is false
        test1(i);
             ^
Main.java:10: 警告: Associated declaration: Main.java:4: 注: 
    public static int test1(int i) {
                      ^
Main.java:16: 警告: JML postcondition is false
    public static int test2(int i) {
                      ^
Main.java:15: 警告: Associated declaration: Main.java:16: 注: 
    //@ ensures 
esult == 20;
        ^

  在设置了racCheckAssumptions参数之后的输出入下：

Main.java:4: 警告: JML precondition is false
        test1(i);
             ^
Main.java:10: 警告: Associated declaration: Main.java:4: 注: 
    public static int test1(int i) {
                      ^
Main.java:8: 警告: JML precondition is false
    //@ requires i == 1;
        ^
Main.java:16: 警告: JML postcondition is false
    public static int test2(int i) {
                      ^
Main.java:15: 警告: Associated declaration: Main.java:16: 注: 
    //@ ensures 
esult == 20;
        ^
Main.java:5: 警告: JML postcondition is false
        test2(i);
             ^
Main.java:15: 警告: Associated declaration: Main.java:5: 注: 
    //@ ensures 
esult == 20;
        ^

• -racJavaChecks：当设置了该参数之后，会检查java语句。

  例如如下代码：

public class A {
	public static void main(String ... args) {
    int i = args.length;
		int j = i/(i-i);
	} 
}

  在设置了该参数之后，会输出除零报错:

A.java:5: JML Division by zero 
  int j = i/(i-i);
					 ^
Exception in thread "main" java.lang.ArithmeticException: / by zero at A.main(A.java:5)

2.5 在IDEA中配置OpenJML工具

使用external tools教程(win/linux)

https://www.jianshu.com/p/da29cc50eaf4

使用external tools教程(mac)

http://hyuga.top/2018/09/07/idea-external-tools/

三. OpenJML与JunitNG联合进行自动单元测试

 3.1 JMLUnitNG的安装

  JMLUnitNG是基于OpenJML的以以JML语言规格描述作为指导的自动生成单元测试工具。

  下载传送门

http://insttech.secretninjaformalmethods.org/software/jmlunitng/release_history.html

3.2 一个简单的JMLUnitNG自动生成测试样例的例子

  先准备一个简单的测试代码

public class Adder {
    /*@ public normal_behaviour
      @ ensures 
esult == a + b;
    */
    public static int add(int a, int b) {
        return a + b;
    }
}

  运行JMLUnitNG.jar

java -jar jmlunitng-1_4.jar Adder.java

  编译当前目录下的所有.java文件

javac -cp jmlunitng-1_4.jar *.java
openjml -rac Adder.java

  运行生成的测试代码

java -cp jmlunitng-1_4.jar Adder_JML_Test

  得到如下的结果：

[TestNG] Running:
  Command line suite

Passed: racEnabled()
Passed: constructor Adder()
Failed: static add(-2147483648, -2147483648)
Passed: static add(0, -2147483648)
Passed: static add(2147483647, -2147483648)
Passed: static add(-2147483648, 0)
Passed: static add(0, 0)
Passed: static add(2147483647, 0)
Passed: static add(-2147483648, 2147483647)
Passed: static add(0, 2147483647)
Failed: static add(2147483647, 2147483647)

===============================================
Command line suite
Total tests run: 11, Failures: 2, Skips: 0
===============================================

  可以看到检测出来算数溢出的问题。

 3.3 在本次作业中尝试使用JMLUnitNG

• 在使用JMLUnitNG先用OpenJML对JML进行检查，确保能够进行运行时检查。
• 如果出现HashMap ArrayList等报错，需要把代码补充完整

ArrayList<Person> acquaintance = new ArrayList<Person>();

从JMLUnitNG生成的测试样例来看，大多测试的都是边界数据。因此JMLUnitNG可以作为一个提醒程序员考虑数据边界的辅助测试工具，但是程序正确性的保证，还是需要JUnit进行单元测试以及考虑自动或手动构造更多的测试样例。

四. OpenJML的webapp

  OpenJML的官网还提供了一个OpenJML WebApp(https://www.rise4fun.com/OpenJMLESC/)，可以把代码提交上去进行检查。