OOUnit3Summary

一、JML基础梳理及工具链

jml语言基础

JML的全称是Java Modeling language，是一种行为接口规格语言，通过JML及其支持工具，不仅可以基于规格自动构造测试用例，还可用SMT Solver等工具以静态方式来检查代码实现对规格的满足情况。

1、注释结构

　　行注释：//@annotation

　　块注释：/*@ annotation @*/

2、JML表达式

　　1.1原子表达式

\result表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。

\old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。

\not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。

\not_modiﬁed(x,y,...)表达式：与上面的\not_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取值未发生变化。

\nonnullelements( container )表达式：表示 container 对象中存储的对象不会有 null 。

\type(type)表达式：返回类型type对应的类型(Class) 。

\typeof(expr)表达式：该表达式返回expr对应的准确类型。

1.2量化表达式

\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。

\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。

\sum表达式：返回给定范围内的表达式的和。

\product表达式：返回给定范围内的表达式的连乘结果。

\max表达式：返回给定范围内的表达式的最大值。

\num_of表达式：返回指定变量中满足相应条件的取值个数。

3、方法规格

　 (1) 前置条件：requires

　（2）后置条件：ensures

　（3）副作用范围限定：assignable或modifiable

4、类型规格

　　(1)不变式invariant：是要求在所有可见状态下都必须满足的特性，语法上定义 invariant P ，其中 invariant 为关键词， P 为谓词。

　 (2)状态变化约束constraint ：对象的状态在变化时往往也许满足一些约束，这种约束本质上也是一种不变式。

工具链

1.OpenJML：检查JML规格的正确性，提供对程序的静态和动态检查。

由于各种报错等问题，本人openjml的布局失败。。。

2.JMLUnitNG：根据JML自动生成测试数据来验证正确性。

首先，将(稍加修改的)MyGroup.java和openjml，junitng的jar包放在同一目录下，然后命令行运行如下命令：

java -jar jmlunitng.jar test/Group.java

javac -cp jmlunitng.jar test/*.java

java -jar openjml.jar -rac test/Group.java test/Person.java

java -cp jmlunitng.jar test.Group_JML_Test

经过一系列尝试之后，终于是有结果了，以下是本人运行结果的片段，由于测试样例大多为一些边界数据，并不是所有的点都是pass，下图仅为pass的部分点:

二、前三次作业内容分析

前言

第三单元的作业以JML语言主题，以人际关系网络为背景，分三次要求逐步增加，难度逐步提高。这三次作业，让我进一步理解了java编程语言，明白了规格和实现之间的关系，使得我在编程上更为严谨。

以下是我对于这三次作业的总结，希望能给我以后得到作业和今后的编程道路提供帮助和参考。

第一次作业

架构分析：第一次作业主要是基于规格填写代码，难度不高。在isCircle方法中，本人使用了DFS，这并不是效率很高的算法，但对于本次作业的数据规模来说足够通过。

bug分析：本人在本次作业中并未被测出bug。

第二次作业

架构分析：第二次作业也主要是基于规格填写代码，增加了Group类，数据规模相对于第一次大大增加，本人不得不对其做一些优化；本人将isCircle方法改为了查并集，并且对于组内的关系合，平均年龄等数据采用了缓存机制；这些优化对于这种高访问低修改的数据效果十分明显。

bug分析：本人在这次作业中因为没要看到一行规格的描述(选择性忽略)，导致强测挂了4个点；具体来说是group的人数小于1111，本人检查工作和测试工作做的十分不到位。

第三次作业

架构分析：第三次作业的难度相对于一，二次作业有了明显的提升，尤其是qmp(最短路径查询)，qsl (环路查询)方法，本人前者采用了Dijkstra算法，后者采用了DFS环路查询算法，然而这两者复杂度较高，为强测和互测埋下隐患。

bug分析：本人在这次作业中的qmp和qsl均出现了tle问题，导致强测直接挂了5个点，本人不得不进行优化算法；参考了讨论区大佬和一些博客之后，本人qmp采用了优先队列的Dijkstra算法，qsl采用了枚举删点判断联通的方法，性能大大提高。

三、算法分析

虽然这次的博客在jml工具链方面着实恶心人，但三次作业下来本人还是接触到了一些非常有用的算法，虽然它们都是我因为数据强度关系不得已之为，但还是在这里总结一下, 这些东西至少比jml工具链的验证要有意义的多：

1.iscircle--并查集

每一个极大连通子图都抽象为一个群体，拥有共同的祖先(ancestor)，每个人都有唯一的父亲结点(parent)，每次进行isCircle，只需对两个结点循环找父亲结点 (追根溯源)，直到找到祖宗(祖宗的父亲为其本身),两者的祖宗结点相同，则必连通。

int ancestor1 = p1.getParent();

while (ancestor1 != p1.getId()) {

　　p1 = MygetPerson(ancestor1);

　　ancestor1 = p1.getParent();

}

int ancestor2 = p2.getParent();

while (ancestor2 != p2.getId()) {

   p2 = MygetPerson(ancestor2);

   ancestor2 = p2.getParent();

}
p1.setParent(ancestor1);
p2.setParent(ancestor2);

return ancestor1 == ancestor2;

同时，在addrelation的时候，需要循环查找两者的祖先，若祖先不相同，则将后者的祖先的parent设置为前者的祖先，这样可以保证查找祖先路径的唯一性；

同时，为了进一步提高效率，本人采取了压缩路径的方法，每一次循环找祖先(adderlation,isCircle)，都将结点的parent直接设置为自己的祖先，下一次访问课大大减少循环次数。

2.queryMinPath--优先队列的Dijkstra算法

此算法借鉴了一些博客，做了一些修改以适应本人的体系，采用java的核心类PriorityQueue，并将人抽象为id-distance二元对，用Weight类来表示这个二元对，并增加MyComparator类(继承Comparator，重写compare方法，为优先队列内部的堆排序提供比较原则)

        MyComparator myComparator = new MyComparator();

        PriorityQueue<Weight> que = new PriorityQueue<Weight>(myComparator);

        HashMap<Integer, Integer> visit = new HashMap<Integer, Integer>();

        HashMap<Integer, Integer> distance = new HashMap<Integer, Integer>();

        Weight nweight = new Weight(id1, 0);

        distance.put(id1, 0);

        que.add(nweight);

        while (!que.isEmpty()) {

            Weight now = que.poll();

            int id = now.getId();

            if (visit.containsKey(id)) {

                continue;

            }

            if (id == id2) {

                break;

            }

            int min = now.getWeight();

            visit.put(id, 1);

            MyPerson top = MygetPerson(id);

            for (int i = 0; i < top.getAcquaintanceSum(); i++) {

                MyPerson np = top.getAcquaintance(i);

                if (!visit.containsKey(np.getId())) {

                    if (!distance.containsKey(np.getId()) ||

                            min + top.queryValue(np) < distance.get(np.getId())) {

                        int update = min + top.queryValue(np);

                        Weight next = new Weight(np.getId(), update);

                        distance.put(np.getId(), update);

                        que.add(next);

                    }

                }

            }

        }

        return distance.get(id2);

3.queryStrongLink--删点寻通路

这个方法也是询问了大佬，本人一开始是用DFS找环路这种朴素的方法实现的，但无奈这个算法效率过于低下

此方法分为两种情况

1）.两点直接相连：将连点之间的边(关系)删去，并进行DFS查找通路，若存在，则两点必成环

        if (p1.isLinked(p2)) {

            //System.out.println("mode1");

            visit = new HashMap<Integer, Integer>();

            final int value = p1.queryValue(p2);

            p1.delAcquaintance(p2);

            p2.delAcquaintance(p1);

            final boolean isfind = findPath(id1, id2);

            p1.addAcquaintance(p2);

            p2.addAcquaintance(p1);

            p1.addValue(value);

            p2.addValue(value);

            return isfind;
       ｝

注意，由于这次背景架构的特殊性，删边即删除关系(熟人列表)，由于arraylist顺序存储的特性，本人的Person类的熟人和Value集合位置是一一对应的，暂时删除人的时候关系值也要一并删除，加回的时候，要一并加回；

2），不直接相连：将除两点外的点一个个删去判断删除后有无通路，在一个个加回，事实上，若两点成环，删去任意一个点，不影响两者之间的连通性(找割点)，实际上这只是一个必要条件，无法涵盖第一种情况，所以需要分类讨论，较为统一得到做法是直接删边，但这样更为复杂，遂放弃。

       else {

            for (int i = 0; i < people.size(); i++) {

                int id = people.get(i).getId();

                if (id == id1 || id == id2) {

                    continue;

                } else {

                    visit = new HashMap<Integer, Integer>();

                    MyPerson np = peomap.remove(id);

                    //System.out.println("Remove:" + np.getId());

                    if (!findPath(id1, id2)) {

                        peomap.put(id, np);

                        //System.out.println("Fail:" + np.getId());

                        return false;

                    }

                    peomap.put(id, np);

                }

            }

            return true;

        }

    }

同时要注意，由于数据规模的问题，visit采用数组，Person在arraylist中的位置对应数组中的index这样会炸tle，因为从id得知其位置需要一个遍历操作，才能知道其有无被访问过，然后遍历操作不可怕，可怕的是在循环中的遍历，更可怕的是在循环中的DFS中的每一次递归中的遍历；可取的做法是采用Hashmap，将id和是否被访问的标志为存的二元对存放。

四、心得体会

按理来说，本单元相对于前两单元是比较轻松的，但本人做的反而比前两次作业差，这主要是本人的疏忽和算法优化的工作不到位所致；相信经历了这单元之后，本人对于代码编写将更为严谨，也会更加注重算法复杂度的考量。

巴特西