OO第三单元——规格化设计与地铁系统——总结

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这门课愈来愈好，祝计算机学院的学生们获得更好的锻炼！