OO第三单元_JML&架构单元总结

JML&架构单元总结

一、JML总结

JML理论

JML简介
JML是一种形式化的、面向JAVA的行为接口规格语言(behavioral interface specification language)
JML特点
JML允许在规格中混合使用Java语法成分和JML引入的语法成分，JML拥有坚实的理论基础，JML使用Javadoc的注释方式 • 结构化、扩展性强（块注释:/@ ... @/，行注释://@）。
JML使用
在我看来，JML是一种很适合展现工程架构的规格语言。在团队合作、任务派发方面有重要的作用和地位，如果能正确的给出规格，对于一个团队来说将是莫大的帮助。按照给定规格完成代码，大大减小了出现各种错误的可能性，也更能保证我们的代码有确定的架构。而对于我来说，学习JML之后，依照JML来进行规格的学习，更是让我更加直观的了解了规格和其重要性。下面介绍一下我个人对JML和架构的总结。

对于JML我个人会把他拆成三个层次来观察和实现自己代码

状态层次
在看到一份JML规格时，我首先会看他对于通常状态和异常状态的分类，这样首先将JML规格拆成几个部分，可以较好的完成编程不易出错。并且在形式化验证时可以优先去查证层次之间是否有冲突。

先决条件
对于每一个层次，我首先关注的是它的先决条件也就是JML中的requires前置条件，他正是为了规定了每一个状态对于数据的要求，也就是对于什么数据才进行处理这样我们就可以构造好程序的分支结构。

得到结果
在我们构造好整体的分支层次后，要干正事了，干正事前看看有没有副作用，这一点保证了我们对于“对象“的操作是安全的，然后就需要理解后置条件完成代码了，这里也是JML语法涉及最多的部分（forall，exist等等），具体语法就不再赘述啦。而在这一步，如果遇到复杂的方法，我们不能按照JML规格一步一步写，而是理解了JML规格选择合适的算法和数据结构来处理（比如qbs方法）。

JML工具及用途

openJML：对JML注释的完整性进行检查。检查包括经典的类型检查、变量可见性与可写性等。通过命令行使用OpenJML时，可以通过-check参数（缺省）指定类型检查。

SMT Solver：检查代码规格，生成测试。

JMLUnitNG：针对类自动生成测试样例并进行测试。（一般是对边界值和空值进行测试）

由于我个人电脑的问题，始终无法成功运行，关于这一部分我真的非常抱歉。所以我只好开着语音远程和我的舍友一起做了代码的check工作（如下图所示），剩下的工具链只是了解了其用法和测试机理。

二、依据JML标准的架构设计

三次作业的设计

第一次作业
第一次作业整体比较简单，只要仔细阅读规格完成代码即可，除了isCircle需要自己实现具体代码以外，其他方法只需要直接将规格描述改写为代码即可。但是需要注意，在选择容器方面要格外注意。在Person中有“熟人数组”和“熟悉度数组”，相当于分别对应着某人关系网中的联通点和该联通点边的权值。因此，为了便于添加和查询操作，可以使用容器HashMap来对应存储熟人和熟悉度。这样可以让代码清晰高效，避免了不必要的遍历和多余的实现。而在Network中，大部分都是通过Person的属性id进行对Person的查询，并且该属性和Person为一一映射的关系，故而我也使用HashMap以id对应Person的方式构造了关系网中的所有成员数组“People”。
第二次作业
第二次作业基本上承袭了第一次作业，除了数据量变大和新增了一个类group和一些方法外没有什么特别的变化，相较于第一次作业更为简单（可能是已熟悉JML的原因）。但需要注意要引入缓存机制，否则会出现超时的问题。我选择的方式是在每一次addPerson和addRelation时直接进行更新处理，这样就将O(n^2)变成了O(n)，可以解决超时的问题。

主要代码段：

public void update(int value) {
        valueSum += value * 2;
        relationSum += 2;
}

public void addPerson(Person person) {
        if (!people.contains(person)) {
            people.add(person);
            personArrayList.add(person);
            int sum = 0;
            int sum1 = -1;
            for (Person p : personArrayList) {
                if (p.isLinked(person)) {
                    sum += p.queryValue(person);
                    sum1++;
                }
            }
            valueSum = valueSum + 2 * sum;
            relationSum = relationSum + 2 * sum1;
        }
    }

第三次作业
在第三次作业中我对架构进行了较大改动，为了对程序进行并查集和Dijkstra堆优化，我向Person中添加了新的成员：

    // Dijkstra
    private int dis;
    private boolean minWay;
    // BlockSum
    private Person father;

而由于整体网络和节点关系未发生变动，所以整体架构仍然沿袭了第一次作业。

三、BUG分析

分析自己的BUG

三次作业共出现了三处错误，第二次作业是由于优化方式错误，导致有一个点超时，而第三次作业则是由于初始化，导致程序会到边界时间，波动导致两个点超时，重新提交后通过测试，直接修复了BUG。本次作业我采用对照标准形式化验证以及DataMaker和对拍器配合的检查方式，所以程序没有出现行为错误。

查找别人的BUG

三次作业我都是直接使用卡边界数据的方式进行Hack，但是效果并不是很好，在写博客时我反省发现，互测还是需要我们人人真真的读他人程序来发现错误，这样才能提高自己，才能发现问题。

四、心得体会

其实作为规格的学习单元，本单元我还是有所收获的，尽管难度相较于前两个单元来说平滑了不少，但是学到的知识却并不比前两个单元少。本单元我学会了如何按照规格书写代码以及如何书写规格，并且了解了规格和开发之间微妙的关系。但是从另一方面来讲，对于“规格”这个抽象的概念还是理解的不够深入，实际应用可能并不能做的很好。最后我感觉本单元其实给下一单元做了很好的铺垫，让我们复习了数据结构并结合Java语言的容器进行了实现，这一方面我确实收获颇丰。

继续冲！