OO第三单元——JML的使用与地铁系统

梳理JML语言的理论基础、应用工具链情况

JML

The Java Modeling Language (JML) is a specification language for Java programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as Java annotation comments to the source files, which hence can be compiled with any Java compiler.

——https://en.wikipedia.org/wiki/Java_Modeling_Language

jml，简单来说，就是在每个方法之前，类似于Javadoc，用注释的形式写出这个方法的效果。和其他规格化是设计不同的是，它可以算是使用了形式化的语言——这样，我们就可以使用程序来解读他，同时他也没有了歧义性。

他的基础如下：

• 使用注释结构
• 由表达式构成
  1. 原子表达式
     • 即各种特殊“符号（Symbol）”
     • 如 \result
  2. 量化表达式
     • 如\forall \exists等
     • 基本格式类似于java中for的写法，(\exist; condition; condition)可以在里面进行限制，约束。
     • 类似于 谓词逻辑（离散数学）
  3. 集合表达式
  4. 操作符
• 方法规格
  • 前置条件 (requires)
  • 后置条件 (ensure)
  • 副作用范围限定 (assignable modifiable)
• 类型规格

参考：

​ https://en.wikipedia.org/wiki/Java_Modeling_Language

​ 《JML Level 0手册》

以上构成了jml的基础

JML工具链

A variety of tools provide functionality based on JML annotations. The Iowa State JML tools provide an assertion checking compiler jmlc which converts JML annotations into runtime assertions, a documentation generator jmldoc which produces Javadoc documentation augmented with extra information from JML annotations, and a unit test generator jmlunit which generates JUnit test code from JML annotations.

——https://en.wikipedia.org/wiki/Java_Modeling_Language

jml 需要支持一个编译器jmlc，一个文档生成器 jmldoc，一个单元测试程序jmlunit

以下团队在做jml相关内容

• ESC/Java2 [1], an extended static checker which uses JML annotations to perform more rigorous static checking than is otherwise possible.
• OpenJML declares itself the successor of ESC/Java2.
• Daikon, a dynamic invariant generator.
• KeY, which provides an open source theorem prover with a JML front-end and an Eclipse plug-in (JML Editing) with support for syntax highlighting of JML.
• Krakatoa, a static verification tool based on the Why verification platform and using the Coq proof assistant.
• JMLEclipse, a plugin for the Eclipse integrated development environment with support for JML syntax and interfaces to various tools that make use of JML annotations.
• Sireum/Kiasan, a symbolic execution based static analyzer which supports JML as a contract language.
• JMLUnit, a tool to generate files for running JUnit tests on JML annotated Java files.
• TACO, an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.
• VerCors verifier

在Github和Gitlib搜索JML，大致获得了一下比较完善的项目实现：

• OpenJML, 包含了编译器等
• JmlUnitNG，单元测试

JMLUnitNG 尝试

这里尝试使用了一个较为简单的类

（有错误）

public class Alu {
    /*@
      @ ensures (a <= b) ==> (\result == a);
      @ ensures (a > b) ==> (\result == b);
      @*/
    public static int min(int a, int b) {
        return Integer.min(a, b);
    }
    /*@
      @ ensures (a >= b) ==> (\result == a);
      @ ensures (a < b) ==> (\result == b);
      @*/
    public static int max(int a, int b) {
        return Integer.min(a, b);
    }
}

分别运行

java -jar jmlunitng.jar Alu.java

javac -cp jmlunitng.jar *.java
java -jar openjml.jar -rac Alu.java

(注意这里jmlunitng和openjml都只支持java8)

然后查看生成的文件

.
├── Alu.class
├── Alu.java
├── Alu_ClassStrategy_int.class
├── Alu_ClassStrategy_int.java
├── Alu_InstanceStrategy.class
├── Alu_InstanceStrategy.java
├── Alu_JML_Test.class
├── Alu_JML_Test.java
├── Alu_max__int_a__int_b__0__a.java
├── Alu_max__int_a__int_b__0__b.java
├── Alu_min__int_a__int_b__0__a.class
├── Alu_min__int_a__int_b__0__a.java
├── Alu_min__int_a__int_b__0__b.class
├── Alu_min__int_a__int_b__0__b.java
├── PackageStrategy_int.class
├── PackageStrategy_int.java
├── PackageStrategy_java_lang_String.class
├── PackageStrategy_java_lang_String.java
├── PackageStrategy_java_lang_String1DArray.class
├── PackageStrategy_java_lang_String1DArray.java
├── SlowPriorityQueue.class
├── SlowPriorityQueue.java
├── Try.class
├── Try.java
├── Try_ClassStrategy_java_lang_String.class
├── Try_ClassStrategy_java_lang_String.java
├── Try_ClassStrategy_java_lang_String1DArray.class
├── Try_ClassStrategy_java_lang_String1DArray.java
├── Try_InstanceStrategy.class
├── Try_InstanceStrategy.java
├── Try_JML_Test.class
├── Try_JML_Test.java
├── Try_main__String1DArray_args__10__args.class
└── Try_main__String1DArray_args__10__args.java

这里阅读这些文件，可以注意到Jmlunitng生成的单元测试文件是使用TestNG测试的。

因此我们使用TestNG测试。

得到如上结果。

可以看到有的test Failed了，这就说明我们写错了，这时候，就可以去查找对应的错误了。

（仔细查找，可以发现是我Max里面返回的是min（故意写错的（笑）））