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

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

因此我们使用TestNG测试。

得到如上结果。

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

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

本单元的作业

结构

以下是三次作业的横向对比：

第一次：

第二次：

可以看到，我前两次作业的结构比较简单，基本只是使用简单的方法实现了题目要求。

每次也是基本复制了前一次代码。

第三次

第三次作业，我进行较大的改动。

以下是类图：

首先，我将算法封装了起来，封装成了一个ShortestPathAlgorithm类，里面有静态的方法，通过传入图，进行计算。

然后，我是写了Calculator抽象类，这个抽象类要负责对图进行储存，实时计算最短路，并缓存。

我分别实现了两种Calculator，分别是Mapped和Normal，其中Mapped是为了我在拆点的时候，给点编号使用了Map，因此单独实现了。

之后，我实现了一个工厂类GraphBuilder负责建图。在建图的时候，需要传入一个Engine,这个Engine要负责计算每条边的长度。（即，不同的需求，只需要更改和重写engine即可）

由此我实现了代码的服用和解耦。

bug 和 测试

很不幸，我在第一次作业中写出了bug，得了60分。

我在维护每个点点出现的个数这个map的时候，我在如果加入一个已经存在的Path时，我可能重复加入，虽然只是一行代码的问题，但是这可带来的巨大的bug。

因此，在之后的实验中，我吸取了教训，进行了较多的测试，并写了自动化的测试。

以下是我的datamaker

https://github.com/login256/BUAAOO-homework11-datamaker

心得

关于这三次作业的结构

OO的目的是什么？这是我经常思考的问题。除了结构上的容易理解、好看，我觉得，或许在最初提出的时候，还有一个重要的目的，就是代码的封装和复用。

对，代码复用。仔细想想之前我每次的设计架构，除了符合面向对象的标准，我考虑的最多的就是：这样好不好写，或者说，这样的代码会不会写出大量的冗杂？

在这次OO作业中，我渐渐明白了，人们为什么要提出一个又一个新的设计方法，从面向过程，到面向对象，再到函数式...人们其实就是想让代码“好看”、“美妙”。所谓好看，就是美观，大家容易读懂，容易配合，所谓美妙，就是简洁，就是没有冗杂的代码。

我也希望自已以后能写出NB的代码！

关于JML

在写隔壁那门OS课的时候，我们有时也需要根据每个函数的注释的规格（写了前置条件，后置条件等等），来补全每个函数。然而，我们经常遇见这样一种情况：这个注释写的太模糊了！根本读不懂！

当时，我就在想，有没有办法，让规格可以少一些歧义。

终于，在OO这门课中，我学到了JML这门语言！

形式化->可以准确描述/没有歧义。

形式化->可以被程序读取！

这样，不仅写代码的人可以准确读懂需求，测试人员还可以直接根据JML自动生成测试数据！

这是多么厉害的一件事情啊。

因此，我在这次作业中，明白了什么叫做实现细节和行为描述分隔开来，明白了这样的好处，也明白了形式化的语言的好处。在使用JML工具的时候，我也进行了各种探索感受到了探索的乐趣！

最后，祝OO这门课越来越好，祝计算机学院的学生们得到更好的锻炼！