OO第三单元——JML之破分大法

Posted 2021-02-18 b-two-w

一．Jml总结及应用工具链

 

　　总的来说，jml就是对java程序进行规格化设计的一种表示语言，其中最核心的就是规格化，将代码要实现的功能和各项要求与约束不是通过自然语言，而是通过严密的逻辑语言来表达，这样让代码实现人员看的更加简洁明了，更极大地提高了代码的可维护性。

 

　　Jml这一大内容主要分为4个板块，分别是注释结构，JML表达式，方法规格和类型规格。

 

　　注释结构方面有着固定的格式，包括前置条件(requires)，副作用限定范围(assignable)，以及后置条件(ensures)。还有规格变量的声明，具体分为两类规格变量，静态变量和实例变量，两种变量分别需要static 和 instance来声明。

 

　　JML表达式则是对Java表达式的扩展，增加了一些操作符和原子表达式。原子表达式细分后有以下内容， esult表达式：表示一个非void类型的方法执行所获得的结果，即方法执行后的返回值。old表达式，用来表示一个表达式在相应方法执行前的取值。 ot_assigned()表达式：用来表示括号中的变量是否在方法执行过程中被赋值。 ot_modified()表达式，该表达式限制括号中的变量在方法执行期间取值未发生变化。 onnullelements(container)表达式：表示container对象中存储的对象不会有null。 ype表达式：返回类型type对应的类型（class）。 ypeof表达式：返回表达式对应的准确类型。量化表达式细分后有以下类型，forall表达式全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。 sum表达式：返回给定范围内的表达式的和。product表达式：返回给定范围内的表达式的连乘结果。max表达式：返回给定范围内的表达式的最大值。min表达式：返回给定范围内的表达式的最小值。 um_of表达式：返回指定变量中满足相应条件的取值个数。而集合表达式则是集可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素。最后一个便是操作符，JML表达式中可以正常使用Java语言所定义的操作符，包括算术操作符、逻辑预算操作符等，还定义了一下四类操作符。子类型关系操作符： E1<:E2 ，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。等价关系操作符，推理操作符和变量应用操作符。

 

　　至于方法规格和类型规格则是JML中极其重要的内容。方法规格的核心内容包括三个方面，前置条件、后置条件和副作用约定。其中前置条件是对方法输入参数的限制，如果不满足前置条件，方法执行结果不可预测，或者说不保证方法执行结果的正确性；后置条件是对方法执行结果的限制，如果执行结果满足后置条件，则表示方法执行正确，否则执行错误。副作用指方法在执行过程中对输入对象或 this 对象进行了修改（对其成员变量进行了赋值，或者调用其修改方法）。而类型规格指针对Java程序中定义的数据类型所设计的限制规则，一般而言，就是指针对类或接口所设计的约束规则。主要包括不变时invariant和状态约束变换constraint。

 

工具链：

工具链方面，笔者主要尝试使用了openJML和JMLUnit，但是或许因为年久失修的原因，使用的体验感极差，但是勉强还是可以用用的。

其中openJML主要可以用来进行JML语法检查：

openjml -check <source files>

 

以及静态检查：

openjml -esc <source files>

 

和运行时检查：

openjml -rac <source fils>

 

值得一提的是，jml除了本地可以部署，还可以使用官网的在线检测系统，这里对person类进行了简单的测试。

 

二．JMLUnitNG/JMLUnit的使用

 

　　对于原来所写的代码文件，直接使用JMLUnit会出现大量报错信息，所以摘选了Group中的部分代码进行测试。

 

public class MyGroup implements Group {
    private int id;
    private HashMap<Integer, Person> people = new HashMap<>();
    private int agesum = 0;
    private int agesumm = 0;
    private int vaSum = 0;
    private int reSum = 0;

    public void addVaSum(int va)
    {
        vaSum += va;
    }

    public void addReSum(int re)
    {
        reSum += re;
    }

    public MyGroup(int id) {
        this.id = id;
    }

    public int getId() {
        return id;
    }

    public boolean equals(Object obj) {
        if (obj == null || !(obj instanceof MyGroup)) {
            return false;
        }
        else {
            if (((MyGroup) obj).getId() == id) {
                return true;
            }
            else {
                return false;
            }
        }
    }

    public void addPerson(Person person) {
        for (Integer integer : people.keySet()) {
            if (person.isLinked(people.get(integer))) {
                reSum += 2;
                vaSum += 2 * person.queryValue(people.get(integer));
            }
        }
        agesum += person.getAge();
        agesumm += person.getAge() * person.getAge();
        people.put(person.getId(),person);
        reSum += 1;
    }
}

 

　　在命令行中输入以下指令：

 java -jar jmlunitng.jar test/Group.java
 javac -cp jmlunitng.jar test/*.java
 java -jar openjml.jar -rac test/Group.java
 java -cp jmlunitng.jar test.Group_JML_Test

　　可以发现，jmlunit测试主要是从输入数据的边界来的，比如int类型的最大值和最小值以及特殊值0，而且不符合此次作业的相关需求，而且大部分测试都是failed，所以不太适合这次作业的使用。

三．作业架构与bug修复

 

1.第一次作业

 

　　第一次作业最终需要实现一个社交关系模拟系统。可以通过各类输入指令来进行数据的增删查改等交互。通过继承官方提供的接口Person和Network，来实现自己的Person和Network类。

 

　　第一次作业由于刚接触JML，便照着规格写代码，并没有进行任何的架构设计，仅仅是对容器的使用根据不同情况选用了不同类型的容器，每个方法的实现流程基本上都是围绕规格来实现的。

 

　　总的来说就是只有一个主类和两个MyNetwork和MyPerson类分别实现了对应的两个接口。

 

　　而正是因为架构的简单和代码的完全依照规格，导致我在强测中获得了0分，不仅是因为单元测试没有到位，导致某个函数的字符出现错误以致WRONG ANSWER，更因为没有架构设计和代码的简单性导致isCircle函数只要运行稍微多的数据就会出现ctle，因为我仅仅是简单的使用DFS函数，并没有做算法上的优化设计，更不用说整体的架构了，所以这次作业可以说是完成的最为失败的一次了。

 

　　对于之后的bug修复，我依据同学的建议将isCircle的DFS算法换成了并查集算法，并在代码中增加了一个专门供并查集使用的UnionFind类，这样不仅让isCircle的方法变得十分简单，更极大地提高了方法的执行效率，再也不会像DFS方法一样卡在半路一点反应都没有了。

 

 

2.第二次作业

 

　　第二次作业在第一次作业的基础上增加了Person接口，并需要我们继承接口实现自己的Person类，并且在Group接口中也相应增加了一些方法。

 

　　在第一次作业的悔恨上，我便更多地增加了一些自己的架构设计，稍微摆脱了jml规格的完全束缚，但是这还是不够，我的代码类还是仅有那几个类，并没有再单独地分出了另外的类别，只是在Group类中增加了一些缓存机制，以提升代码的执行效率，以免出现ctle的情况。这次增加的Network类和Group类中新增方法对算法并没有太高的要求，所以第二次作业还算是完成的较为轻松。

 

　　第二次作业虽然没有出现太大的问题，但是在强测中还是没有获得满分，具体的原因还是因为JUNIT测试的不够充分，正是某些方法看起来短短几行觉得一定不会出现错误便没有去测试，结果便是强测的WRONG ANWSER，第二次作业便就是因为某个简短的方法中一个引用写写反了，本来应该是people容器的，结果我写成了group容器，最后在bug修复中改了过来。

　　具体的代码框架如下所示：

 

 

3.第三次作业

 

　　第三次作业可以说是在jml这一单元中最难的作业，毕竟也是压轴登场，在Network中增加了几个较为复杂的方法，如果不使用适合的算法的话，这次作业很有可能不能通过。最为突出的便是queueminpath方法和queueStrongLinked方法 以及queueBlockSum方法，这三个算法都要对图进行大规模的遍历和计算，耗时较长。

 

　　单纯的我并不知道世间险恶，先尝试了一下较为简单的dfs算法和几个双重遍历，并略微进行了测试，发现速度没什么问题，基本上运行则立即出结果，就把代码提交了上去，中测可以说是不测，毫无悬念的通过中测。而类的方面仍然是简单几个大类，并没有细致地划分，而是在代码中摆脱规格限制，自己增加了一些其他数据结构和一些新的方法。

 

　　但看了讨论区的我觉得并没有这么简单，便发现测试数据一旦大到一定规模我的代码并执行得异常缓慢，所以便尝试使用新的存储的数据结构和新的算法。而后续的强测出现的错误也是ctle。

 

　　具体地来说，主要把queueminpath的dfs算法换成了spfa算法，queueStrongLinked的dfs算法换成了tarjan算法，这样我的时间复杂度便得以大幅的降低了。而queueBlocksum则是配合isCircle的方法实现缓存加维护更新机制，更进一步降低了时间复杂度。

 

　　具体的代码框架如下：

 

 

 

 

 

四．心得体会

　　刚开始接触第三单元的时候，我竟然觉得这是这三个单元中最简单的一个单元，但我是完完全全的想错了，不仅不是最简单的，反而在这三个单元中取得成绩最差的就是这个单元，绝对不是仅仅因为放松警惕导致的粗心大意，而是没有设计足够好的代码框架，加上没有使用合适高效的算法，导致强测分数一直都不理想。

　　正是因为这三次作业的失利，不禁让我对jml更进一步地进行了思索，规格只是规定了功能和要求，并没有对代码实现人员的实现过程进行了设计，我们在编写符合规格的代码前，通读规格，知道了设计人员的需求，在满足规格的正确性的基础上，代码的具体内容和整体框架仍然是由自己来决定和编写，不要被这个所谓的规格所限制住。

　　还有一个让我感触比较深刻的是，不仅是老师一直在强调的，同学们在研讨课上也提出过，oo课并不强调算法，而是注重代码的设计与框架，层次结构，只要这些方面不出问题的话，性能绝对不会太差。

　　最后一个让我永远无法忘记的就是openjml和jmlunit了，配置环境属实艰难，而且体验感极差，让本就贫苦的我更加雪上加霜。