Part-1 JML总结

Section-1 理论基础

The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules.

JML是一种正则化的描述Java模块行为的描述语言。也就是说，JML的作用是对程序各模块和架构进行描述。

利用JML，我们可以做到：

1. 对模块内，架构与实现分离，JML编写者提出要求，规定程序该做什么；实现者实现要求，决定程序该怎样做。
2. 对模块外，JML作为文档，为使用者提供必要的、无二义的知识，提高代码可维护性。

方法层面上，JML通过requires关键字来声明调用方法的前置条件，对被调用方法而言，requires中的内容是可以认定为成立的；ensures关键字来声明调用方法期望达到的效果，对被主调方法而言，ensures中的内容是可以认为在调用后一定是成立的。这其实就是所谓的契约式编程。requires规定了调用方的义务和被调用方的权利，而ensures规定了被调用方的义务和调用方的权利。程序因此被分为不同的块，每一块都有对应的负责人，块与块之间的接口就是JML规格。

此外，还有signals等应对异常情况的关键字，其实可以算是一种特殊的requires，在此不再赘述，可以自行查阅JML相关教程。

类的层面上，JML通过invariant不变式规定了一个类可见时应当保持的状态，而constraint规定了一个类状态变化前后应当满足的约束。通过这些JML规定了一个类的合法状态。

JML中的条件既可以是Java中的方法，也可以使用谓词逻辑，这给了它很大的灵活性。

很显然，使用JML的开发方式可能显得比较僵硬，但是JML能有效明确需求，促进模块化思想。此外，JML有一系列实验中的工具，若是这些工具成熟，将会有效辅助代码的编写和验证。

Section-2 工具链

JML的工具链目前都处于试验阶段，离实际应用还有很远距离，部分软件已经停止开发。主要的JML工具链包括：

• JMLUnitNG：自动化单元测试工具，效果很差，只会找一些null/INT_MAX/INT_MIN塞给你
• OpenJML：形式化验证/动态assert检查工具，可以说是目前最为完善的JML工具（但是还是距离实际可用很远）。

P.S. 在目前（2020年）这个时间节点看，至少3年内JML工具链都不太可能应用于我们的OO作业的直接验证。所以学弟学妹们如果发现JML相关工具链没有太大进步的话，建议不要为难自己试图用相关工具作为验证自己作业的正确性的手段。个人认为JML作为一种“文档”的作用更重要。

Part-1.5 一些牢骚（

从这里开始以下两节内容可能包含不少yygq，因为作者当时花了七八个小时修了十几个Bug，在Linux和Windows之间转战数次。最后以一个全新的，实在超出作者（以及我觉得任何一个正常OO学生，大佬除外）能力，甚至没有任何信息的Bug收尾（就给一个NullPointerException或者Internal JML ERROR甚至开屏JNI Error我还能怎么办啊？去调试OpenJML的jar/深入JVM研究么？）。只能用浪费时间评价。希望学弟学妹们避开此雷，也恭请各位老师们亲手试验一下，将一份作业代码利用JML工具链运行一下，看看能取得怎样的效果。

引用J语：

至少我觉得，如果让程序员抛弃程序效率，抛弃程序简洁度，甚至说是抛弃程序能否满足课程组要求（算法时间之类的），去满足一个比较低下的工具，我真的觉得本末倒置。 --- J

使用JML工具链？何必自己为难自己。

Part-2 部署SMT Solver验证代码

SMT Prover，即可满足性理论求解器，就是判断一个公式是否可满足的工具。OpenJML使用SMT Prover，证明JML和程序代码的不等价是不可满足的，即一定等价。（更多详细信息可参见 用SMT solver验证程序等价 一文）

我们要做的，也就是直接使用OpenJML的静态验证。OpenJML自带三个可满足性定理求解器，z3-4.7.1.exe，z3-4.3.2.exe，cvc4-1.6.exe

当然，在使用OpenJML之前，我们需要对我们的代码做一些微小的改动：简单地说，我们要把所有的JML spec域映射到我们Java代码的域，具体映射的完成使用represent子句，大家可以去网上查找相关内容。同时我们不能让JML里的域与Java里的域重名。在HW9里我的改动如下：

MyPerson.java

    private int p_id;
    private String p_name;
    private BigInteger p_character;
    private int p_age;
    private List<Person> p_acquaintanceList;
    private List<Integer> p_valueList;

    /*@ private represents id <- p_id;
      @ private represents name <- p_name;
      @ private represents character <- p_character;
      @ private represents age <- p_age;
      @ private represents acquaintance <- getAc();
      @ private represents value <- getVal();
      @*/

    private /*@ pure helper @*/ Person[] getAc() {
        // change arrayList into array
        return p_acquaintanceList.toArray(new Person[0]);
    }

    private /*@ pure helper @*/ int[] getVal() {
        int len = p_valueList.size();
        int [] a = new int[len];
        for (int i = 0; i < len; i = i + 1) {
            a[i] = p_valueList.get(i);
        }
        return a;
    }

MyNetwork.java

    private List<Person> peopleList;

    //@ private represents people <- getArray();
    private /*@ pure helper @*/ Person[] getArray() {
        return  peopleList.toArray(new Person[0]);
    }

下面我们来看看使用这三个不同的Solver对我的Homework9的验证成果吧！（选择Homework9是因为这次作业我没有写多容器，否则我还要再写一堆invariant来约束多容器的一致性）

z3-4.7.1.exe

z3-4.3.2.exe

cvc4-1.6.exe

?

“OpenJML是多么先进的工具啊，这一定是因为Windows不适合开发工作！”

那么我们使用Linux验证一下吧！

100个警告？OpenJML真是先进啊！我代码是怎么过的测试？快让我看看到底是什么Bug。

经过我仔细分类，总共有三种警告

1. 哦我的上帝啊，快看这里，瞧瞧我发现了什么，如果我们用强迫的方法给他塞一个INT_MAX/null，他就会产生溢出/抛出异常！老伙计，这是多么可怕的事情啊
2. 非常抱歉，亲爱的朋友，我们这里暂时还没有办法对某些\not_assigned, \exists, \forall, \sum进行检测
3. 天啊，我没办法确定他们一定相等！
   --- 为什么呢？
   就是这个条件，但我也不知道为什么
   --- 给个反例？
   歪比歪比，歪比巴卜

总之，指望OpenJML对我们的OO作业进行形式化验证在3-5年内可以说是春秋大梦。建议各位后来者在JML工具链发展起来前果断选择放弃（

OpenJML形式化验证能做到什么样呢？可以去看看 https://www.rise4fun.com/OpenJMLESC/MaybeAdd 这个网站，里面有一些可以用的例子。

但是，只要我们稍微改动一点点的话...“天啊，我没办法确定他们一定相等！”

?

对于OpenJML在OO作业中的使用，我只有一句话送给学弟学妹们

快????跑

Part-3 JMLUnitNG测试

JMLUnitNG是一个针对类自动生成测试样例并进行测试的工具。

我使用JMLUnitNg测试MyGroup.java效果并不好，原因如下：

1. 使用OpenJML测试HW9时，发现rac模式，也就是运行时检查模式着实难以运行，尝试许久无果，遂计划放弃。
2. MyGroup相比HW9的MyPerson更加复杂，且依赖于MyPerson和MyNetwork，遂计划放弃。
3. 我们在MyGroup中采用了缓存机制，因此不能保证在任何时候JML的规范都得到满足
4. JMLUnitNG早就过时，奇葩Bug层出不穷实在无力，遂放弃。

编译运行

1. java -jar ../jmlunitng-1_4.jar MyGroup.java
   发现

   MyGroup.java:22: 错误: 非法的类型开始 
   this.personMap = new HashMap<>(2048);
   

   需要改为new Hashmap<Integer,Person>(2048)
   同时需要设置合理的represent

   private HashMap<Integer, Person> personMap;
   
   //@ private represents people <- getArray();
   private /*@ pure helper @*/ Person[] getArray() {
      Person[] pa = new Person[personMap.size()];
      int i = 0;
      for (Person p : personMap.values()) {
         pa[i] = p;
         i = i + 1;
      }
      return pa;
   }
   

2. javac -cp ../jmlunitng-1_4.jar *.java
   编译

3. java -jar ../openjml/openjml.jar -rac -cp . MyGroup.java
   开启OpenJML动态检查rac

   java -jar ../openjml/openjml.jar -rac MyGroup.java
   MyGroup.java:1: 错误: 程序包com.oocourse.spec3.main不存在
   

   拆掉所有包

   

   

   然而如果不开rac这本来就残缺不全的软件就彻底废了
   图：一个没开rac的程序

   

   P.S. 其实即使开了rac也只会fail一个点，因为其他的数据都不满足前置条件，这也更进一步说明它的测试很不完善。
   遂放弃

为了搞清楚JMLUnitNG到底测试了我的类的何种情况，我在rac关闭（这意味着无法发现不符合JML的问题）的情况下直接运行了JMLUnitNG的测试程序。我对类中的某些方法加上了print，输出组里现在每个人的状况。

print代码：

private void print() {
      System.out.println(personMap.size());
      for (Person p : personMap.values()) {
         System.out.println(p);
      }
   }

测试结果：

$ java -cp ../jmlunitng-1_4.jar\;. MyGroup_JML_Test
[TestNG] Running:
  Command line suite

Failed: racEnabled()
Passed: constructor MyGroup(-2147483648)
Passed: constructor MyGroup(0)
Passed: constructor MyGroup(2147483647)
0
Failed: <<MyGroup@6842775d>>.addPerson(null)
0
Failed: <<MyGroup@574caa3f>>.addPerson(null)
0
Failed: <<MyGroup@1761e840>>.addPerson(null)
0
0
Passed: <<MyGroup@6c629d6e>>.delPerson(null)
0
0
Passed: <<MyGroup@5ecddf8f>>.delPerson(null)
0
0
Passed: <<MyGroup@3f102e87>>.delPerson(null)
Passed: <<MyGroup@27abe2cd>>.equals(null)
Passed: <<MyGroup@5f5a92bb>>.equals(null)
Passed: <<MyGroup@6fdb1f78>>.equals(null)
Passed: <<MyGroup@51016012>>.equals(java.lang.Object@29444d75)
Passed: <<MyGroup@2280cdac>>.equals(java.lang.Object@1517365b)
Passed: <<MyGroup@4fccd51b>>.equals(java.lang.Object@44e81672)
Passed: <<MyGroup@60215eee>>.getAgeMean()
Passed: <<MyGroup@4ca8195f>>.getAgeMean()
Passed: <<MyGroup@61baa894>>.getAgeMean()
Passed: <<MyGroup@b065c63>>.getAgeVar()
Passed: <<MyGroup@768debd>>.getAgeVar()
Passed: <<MyGroup@490d6c15>>.getAgeVar()
Passed: <<MyGroup@7d4793a8>>.getConflictSum()
Passed: <<MyGroup@449b2d27>>.getConflictSum()
Passed: <<MyGroup@5479e3f>>.getConflictSum()
Passed: <<MyGroup@27082746>>.getGroupSize()
Passed: <<MyGroup@66133adc>>.getGroupSize()
Passed: <<MyGroup@7bfcd12c>>.getGroupSize()
Passed: <<MyGroup@24273305>>.getId()
Passed: <<MyGroup@5b1d2887>>.getId()
Passed: <<MyGroup@46f5f779>>.getId()
Passed: <<MyGroup@1c2c22f3>>.getRelationSum()
Passed: <<MyGroup@18e8568>>.getRelationSum()
Passed: <<MyGroup@33e5ccce>>.getRelationSum()
Passed: <<MyGroup@5a42bbf4>>.getValueSum()
Passed: <<MyGroup@270421f5>>.getValueSum()
Passed: <<MyGroup@52d455b8>>.getValueSum()
0
Passed: <<MyGroup@4f4a7090>>.hasPerson(null)
0
Passed: <<MyGroup@18ef96>>.hasPerson(null)
0
Passed: <<MyGroup@6956de9>>.hasPerson(null)
Passed: <<MyGroup@769c9116>>.updateRelation(-2147483648, -2147483648, -2147483648)
Passed: <<MyGroup@2471cca7>>.updateRelation(-2147483648, 0, -2147483648)
Passed: <<MyGroup@5fe5c6f>>.updateRelation(0, 0, -2147483648)
Passed: <<MyGroup@6979e8cb>>.updateRelation(0, 0, -2147483648)
Passed: <<MyGroup@763d9750>>.updateRelation(0, 0, -2147483648)
Passed: <<MyGroup@4b6995df>>.updateRelation(2147483647, 2147483647, 0)
Passed: <<MyGroup@61443d8f>>.updateRelation(-2147483648, -2147483648, 2147483647)
Passed: <<MyGroup@445b84c0>>.updateRelation(0, -2147483648, 2147483647)
Passed: <<MyGroup@61a52fbd>>.updateRelation(0, -2147483648, 2147483647)

......

===============================================
Command line suite
Total tests run: 121, Failures: 4, Skips: 0
===============================================

看啊，他传入了2147483647, 0, 2147483647和null！瞧啊，他连一个Person也没有构造。哦我的上帝啊，在各个方法进入时组内人数都是0！这是多么有用的测试啊！亲爱的小彼得，除了这么富有智慧的工具又有谁能想的到这些边缘数据呢？JMLUnitNG真的是人类Coding史上的一座丰碑！（

唯一好的一点是他似乎会对不同操作序列下的Group进行测试，但是鉴于他所有Group只有id不同，emmm

此外，JMLUnitNG还是一个几年前就停止开发维护的软件，这不得不让人怀疑他能起到多大作用。更别提OpenJML清一色的not implemented（和层出不穷的报错）。

综上：JMLUnitNG在当前时间节点（如果不出意料在以后也是）既不可用又没用，近乎毫无作用，建议立即放弃。

Part-4 程序架构分析

三次作业内容是迭代增加的，因此以HW11的架构为例进行分析。

架构因为大部分直接使用课程组接口，因此在此不再多说。除了为了给我们留出自己发挥的空间导致的部分接口方法的缺失外，课程组代码架构相当合理。

Section-1 实现

HW9

容器选择：由于性能不是考虑重点，基本使用ArrayList解决。

重点方法：isCircle，在HW9中，对性能要求不高，直接使用bfs实现。

HW10

容器选择：数据量上来了，因此Network和Group在存储people时和Person的acquaintance中使用了Hashmap。但是由于Person中acquaintance初始化时选择了较大的容量，导致产生可以被Hack的点。

重点方法是：getGroupXXXX系列的方法，如果按照标准方法需要每次进行O(N)的操作，显然问题很大。考虑到Group在只有加人和加关系时更新数据，于是采用缓存方法。即Group在addPerson和Network addRelation时更新缓存。

需要注意的点有：

1. 概统中等价的两个方差公式在我们作业的场景下不等价，因为我们无法满足 \(\sum x = n * E(X)\) 。所以我们要在不利用这个条件的前提下手动展开推导。

2. 除了addPerson时更新缓存，还要注意在Group内Person增加关系时更新缓存。本人代码中通过直接在Network的addRelation方法中添加，这样做虽然直观但是有点提高模块间的耦合度。更为合适的方法可以是采用观察者模式，Person在增加新的关系的时候通知所在的Group。这样的话在HW11里delPerson方法中就要注意对观察关系的解除。

HW11

容器选择：与其纠结初始化容量，不妨直接上多容器，哪个合适就用哪个。这次作业本人综合使用了Hashmap和ArrayList，效果则还不错。遍历用ArrayList查找用Hashmap，就是要注意容器间的一直性

重点方法：三幻神qsl，qmp，qbs（。

• queryStrongLink

  我采用了类似暴力的做法：BFS先找出一条路径，再逐一枚举删除路径上的某个点看是否仍然联通。如果去掉任何一个点都仍然联通，就证明没有割点，是StronggLink。注意要特判person1和person2直接相连的情况。

• queryMinPath

  就是求最短路，我直接用了Dijkstra，配合优先队列进行堆优化。

• queryBlockSum

  求联通块数目，我用了魔改的并查集，在addPerson、addRelation时一步到位直接更改每个人的Block号，两个人的Block如果不同，建立联系后Block号按人数更多的的来。一步到位的更改法保证了路径始终只有一层，时间复杂度也可以接受。

需要注意的点有：

age上限提升到2000，而如果缓存年龄的平方和，2000*2000*800 > 2147483647会溢出。但是，缓存仍能正确的结果。具体分析可以参考这篇文章：HW11中对ageVar采用缓存优化的等价性证明（包括溢出情况）

Section-2 依赖关系

Section-3 复杂度分析

isCircleBfs复杂，是因为为了题目要求加了一些控制参数。其实可以拆分成：找到并加入邻接点，输出路径和bfs主体三个部分，不过整个项目只有少数几个个复杂函数，所以影响不大。queryStrongLink，dijkstra也是类似的道理。

奇怪的是MyNetwork里的delFromFroup、addtoGroup复杂度红了，MyGroup里对应的方法进行了大量操作反而没红。推测原因是MyNetwork里需要扔出各种异常，而MyGroup里操作虽然多但是都只影响自己。包括addRelation应该也是类似的原因。

Part-5 Bug以及测试

这一单元主要通过评测机对拍进行测试（ 这次是白嫖的辣哈哈哈GTCNB！! ），辅助以JUnit单元测试。JUnit单元测试可以用来测试一些异常情况，剩下的还是要靠随机数据对拍更方便可靠（因为我就出现过代码和JUnit测试一起写错的情况）。剩下要注意的点就是TLE了。

三次作业在强测和互测中均为发现Bug，但第二次作业在某些情况下会TLE（ 没错我又是在互测的时候自己发现而且没被卡（妙啊） ），原因是Person中Acquaintance的HashMap初始化容量过大，导致遍历时会炸掉，从此换了双容器天下太平（听说有人第三次被这个坑了，溜。

互测抓到的Bug基本都是TLE吧，功能性错误也就isCircle或者queryStrongLink考虑直连等情况出错了。

Part-6 感想

JML作为一种规范语言，它的作用就是确立开发者和使用者之间共同遵守的准则，这也就是所谓的契约式设计，Design By Contract。明确划分要求和实现。规格在开发过程中是系统架构师和实现者之间的桥梁，架构师用JML提出要求，实现者根据JML完成，更好地把架构和实现分开。

但是我个人觉得规格更重要的作用是在开发后交付给使用者，规格成为文档。JML成为类似于JavaDoc的存在。从这个角度看，JML就是一种划分模块责任边界，提高模块化程度的工具了。而且根据本人三次作业的感受，我觉得后一种更加重要。

此外，JML没法描述复杂度信息，这是一个缺点，也是这单元各种翻车的重要原因。

再有，JML的工具链，绝了。JML的设想太过宏伟，以至于难以实现。换句话说现实工程的话根本没用。想让真正的OO代码运行于JML上，目前看来还远远不现实。个人估计JML工具链距离成熟至少还有3-5年的距离，更长也不奇怪。也许几年后随着数学的发展可能会成为重要的工具。但是现在嘛...建议遇上就快 跑。

说实话，这一单元的作业我感觉没有前两单元那么精准，有力。这一单元除了跟着JML写就没啥架构上的考虑，唯一可以做文章的是单独抽象出Graph类，不过也没有多少人愿意去分开，因为必要不是太大（ 咱也没分因为懒 ）。给我的感觉没有一个明确的主线，最后就变成了数据结构还债。JML本身不好考察的确是一点，还有就是JML的内容撑不起来一个单元，第三单元目前的内容完全可以分在两次作业内完成。官方包代码也总感觉少些方法，虽说能看出来是想给我们留出发挥空间，但是这样有的时候就必须违反依赖倒置原则，感觉有点不爽。

最后，JML这一单元我真正第一次使用了JUnit，的确很好用，但是我醒悟的太晚，否则有第一次第二次JUnit的测试的迭代，我测试时也会更放心点吧。

总的来说这一单元体验也还不错，虽然没前两单元那么刺激（？），但是的确提高了我对面向对象里责任边界划分的认识，以及一些粗浅的工程化代码编写尝试。（ 其实主要是复（预）习了离散2和数据结构 ）希望下一单元能继续加深对OO的理解，为OO带来一个圆满的结尾。

至于JML还有它的“工具链”？告辞（

2020-BUAA OO-面向对象设计与构造-第三单元总结

原文：https://www.cnblogs.com/VOIDMalkuth/p/12942824.html