标签：class   exp   constrain   必须   containe   一个   也有   return   双连通分量   

OO第三单元总结

一、JML理论基础与工具链

理论基础

　　JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言，即JML限制了各个类的规格。JML是一种行为接口规格语言。我们目前学到的JML仅限于level0，还只是入门级而已。

1. 注释结构

2. JML表达式

   1. 原子表达式：\result \old(expr) not_assigned(x, y, ...) \not_modified(x, y, ...)
   2. 量化表达式：\forall \exists \sum等。
   3. 集合表达式（似乎没怎么用到）。
   4. 操作符：b_expr1<==>b_expr2 b_expr1==>b_expr2

   个人感觉基本和离散数学的感觉差不多。

3. 方法规格

   前置条件requires P表示要求方法的调用者确保表达式P为真；后置条件ensures P表示要确保方法执行返回结果要保证P为真；normal_behavior表示正常功能行为；exceptional_behavior表示异常行为，要用到signals (***Exception e) b_expr 子句，即当b_expr为真时抛出异常。

4. 类型规格

   不变式invariant：要求在所有可见状态下都必须满足的特性。

   状态变化约束constraint：对前序可见状态和当前可见状态的关系进行约束。

工具链

• IDEA中的Junit插件，用于对代码进行单元测试。
• openJML，用于检查jml语法的正确性以及检查代码是否符合jml。实用性存疑，更多功能待发现。这里贴一个线上平台，直接把代码贴上去就能测，省的本地配环境了。
• JMLUnitNG，可自动生成测试数据。
• 工具具体用法见焦大佬博客：https://www.cnblogs.com/pekopekopeko/p/12920417.html。

二、SMT Solver

　　下载openJML时候里面就有了各种平台下可用的solver。将openjml.jar，z3-4.7.1.exe，__修改后的__MyPerson.java放在一个文件夹下然后在命令行输入java -jar openjml.jar -exec z3-4.7.1.exe -esc MyPerson.java，得到一堆警告但至少没有报错（sigh）。

　　说一下我对MyPerson.java的修改过程。首先openjml检查时，如果类规格里写了MyPerson[] acquaintance，在实现时就只能同样用数组实现，要么就得改JML，这也实在是openJML的一大恶心之处。改完之后的MyPerson类一窥（省略了很多函数）：

public class MyPerson{
    private /*@ spec_public @*/ int id;
    private /*@ spec_public @*/ MyPerson[] acquaintance = new MyPerson[1000]; //这里为了符合JML无奈之下使用了静态数组
    private /*@ spec_public @*/ HashMap<Integer,Integer> value = new HashMap<>();

    //@ ensures \result == id;
    public /*@ pure @*/ int getId() {
        return this.id;
    }

    /*@ public normal_behavior
      @ requires (\exists int i; 0 <= i && i < acquaintance.length;
      @          acquaintance[i].getId() == MyPerson.getId());
      @ assignable \nothing;
      @ ensures (\exists int i; 0 <= i && i < acquaintance.length;
      @         acquaintance[i].getId() == MyPerson.getId() && \result == value.get(MyPerson.getId()));
      @ also
      @ public normal_behavior
      @ requires (\forall int i; 0 <= i && i < acquaintance.length;
      @          acquaintance[i].getId() != MyPerson.getId());
      @ ensures \result == 0;
      @*/
    //这里规格的第六行把value[i]改成了value.get(MyPerson.getId()))
    public int queryValue(MyPerson MyPerson) {
        if (value.containsKey(MyPerson.getId())) {
            return value.get(MyPerson.getId());
        }
        return 0;
    }
}

三、JMLUnitNG

　　JMLUnitNG好就好在可以自动生成测试数据，据我观察其实也就是生成一些极限数据确保程序在极限情况下的正确性。

　　但是有一点我真的非常疑惑，同样的数据我用Junit测试和代码实际运行都是对的，为什么交给JMLUnitNG这东西就总是fail呢？问过不少同学也有同样的问题，向助教大大请教也没有得到解释，这一点我真的是无可奈何了......

四、我的架构设计——以第三次作业为例

　　总体上我这次的架构就是按照JML的结构来的。

　　在求连通块个数时用到了并查集，将并查集相关操作封装在类UnionFindSet 中。用一个HashMap维护并查集（键值为节点（用户）的id，值为节点的祖先），成员函数为即为并查集的常规加点、求祖先、连边等操作。

　　在求点双连通分量和最短路时没有把相关算法封装到单独的类中而是在MyNetwork类中多写了几个函数，毕竟每个算法只用到了单独一个函数。但是Tarjan算法需要维护全局变量（dfn数组等），就使得MyNetwork类平白无故多了很多成员变量。UML图如下：

五、BUG

• 第一次作业的时候忽视了两个normal_behavior之间的关系，他们应该是if-else_if的互斥关系，而不是if-if的并列关系，有可能在第一个if中修改了成员变量使得第二个if的判断条件成立了，于是错误的又进入了第二个if。幸亏是在强测前发现的，不然真就凉透了。
• 第二次作业还好，没有什么刻骨铭心的bug。
• 第三次作业CTLE了，因为最短路算法没有采用堆优化于是在强测中被卡了3个点...奇了怪了我本地跑强测数据都不超过1.5s的啊（小声）。
• 三次互测中没有被hack，也没有发现别人的bug。

六、体会

• 照抄JML肯定是不行的，JML只是确定了各个类和方法的规则，至于内部的运作方式、代码架构和具体实现还是要自己理解，不能机械的照搬JML。
• JML作为一种规格化的东西，确实能够简明扼要的告诉我们代码应该怎么写，但是JML相关的工具__真的不是很友好__......（当然也可能就是我太菜）
• 网上找到的JML相关资料绝大多数都是往届学长学姐的OO博客，难道北航真的是中国JML独一份吗？

OO第三单元总结

标签：class   exp   constrain   必须   containe   一个   也有   return   双连通分量   

原文地址：https://www.cnblogs.com/Locksoyev/p/12939680.html