【面向对象】三单元JML总结

前言

---

　　相比于前两个单元，这个单元对于测试能力的需求有了进一步的提升。对于所给的规格，我首先需要看懂，并且要使用比较好的方法进行实现。这也带来了一个问题，我必须能够编写测试集来测试自己写的数据结构。还有一个问题，就是即使我每个方法可能符合规格，但是整个程序在总体上会有bug怎么办。所以，这个单元既需要我们从方法级别进行考虑，又需要从工程级别进行量化。下面我将开始分享我的学习心得，请多多指教! \(O~O)/

JML知识梳理

---

　　第一次接触JML，我的反应是：这也太疯狂了吧，架构师不就是帮程序员把程序实现用伪代码描述了么！这种思想是完全错误的，首先规格化描述写的不是“方法流程”，另外按照给的数据结构来整只有死路一条。

这么优雅的过程，实现后可能就6个for循环连环套吧

　　那么JML(Java Modeling Language)到底是什么呢？“在面向对象编程中，一个重要原则就是尽可能地推迟对于“过程”的思考。”在每次编写程序后，想好了整体架构，搭建好了类和接口，之后面对的就是每一个方法。这个时候，我们思考的是这个方法能给我带来什么预期结果，之后再考虑如何实现。比如对于getLeastUnpleasantValue方法（上图），它带给我的结果是一个path，按照这个path走，我能最“满意”。JML在代码中增加了一些符号，这些符号只表述一个方法干什么，并不关系它的实现过程。使用JML，我们就可以描述对于某一个方法的预期功能，却不管实现过程，JML可以把过程性的思考延迟到方法设计中，这点完全符合了“面向对象”。

• JML的理论基础

　　JML非常强大，其有大量用于描述行为的结构（正常、异常行为；模型域、量词……）。JML可以写的很清晰、有层次。JML用这种“抽象”的数据结构去描述，带来了两个好处：首先，JML是独立的，不会因为实现代码结构的改变而被迫变化，这样这个方法的数据结构和整体程序的数据结构是相互独立的；其次，在有代码实现之前，就可以写JML。在实际设计中，JML可以在实现前对设计的规格进行精确传达，也可以帮助梳理自己实现的代码。

• JML的工具链

　　JML也拥有很多很好用的工具，可以提供JML规范检查，或者是随机测试数据生成测试。我对几种工具了解的不是很多，如果有什么好用的请大家补充。

1. 使用OpenJml的-check检查JML规范性
2. 使用SMT Solver检查代码等价性
3. 使用JMLUnitNG生成数据测试代码
4. ……

　　我将下发的JML指导书进行总结，链接在此：https://blog.csdn.net/weixin_41412192/article/details/89527142 

JMLUnit和JUNIT测试

---

 JUnit测试

　　虽然没有要求写这部分内容，但是我还是愿意分享这个过程。在对Graph的任何方法进行测试之前，首先要初始化整个图。这个过程我们没必要在每个test函数都进行一次，所以使用@BeforeClass。

　　接下来我详细根据JML介绍我的测试思路。

• containsNode(int nodeId)

//@ ensures \result == (\exists Path path; path.isValid() && containsPath(path); path.containsNode(nodeId));

　　从输入上看，此方法输入的是一个int类型是数；从结果上看，此方法返回的是一个boolean类型的常量。于是这个测试思路就很好想了，只需要检测“有”和“没有”的点就可以。我也加入了对于负数点的检测，扩充测试范围。

• containsEdge(int fromNodeId, int toNodeId)

    /*@ ensures \result == (\exists Path path; path.isValid() && containsPath(path);
      @      (\exists int i; 0 <= i && i < path.size() - 1; (path.getNode(i) == fromNodeId && path.getNode(i + 1) == toNodeId) ||
      @        (path.getNode(i) == toNodeId && path.getNode(i + 1) == fromNodeId)));
      @*/

　　从输入上看，输入的是任意两个int类型数据；从输出上看，得到的是一个boolean。这块需要注意的是，当输入的点不在图中时，直接输出false，而不能抛异常；自己和自己在containsEdge中没有特殊情况。另外，有些同学可能是用HashMap做的，当遇到（x,x）这种边的时候，可能会“加两次”。这样也会导致出错。所以，我将测试用例划分成了7类：

1. 两点都在图中，并且边存在
2. 两点都在图中，但边不存在
3. from点不在图中，to点在
4. from点在图中，to不在
5. 两点都不在图中
6. from == to且有这条边
7. from == to但是没有这条边

 try_catch部分是对（x,x）这种数据的特殊测试

•  isConnected(int fromNodeId, int toNodeId) throws NodeIdNotFoundException

/*@ normal_behavior
@ requires (\exists Path path; path.isValid() && containsPath(path); path.containsNode(fromNodeId)) &&
@ (\exists Path path; path.isValid() && containsPath(path); path.containsNode(toNodeId));
@ assignable \nothing;
@ ensures (fromNodeId != toNodeId) ==> \result == (\exists int[] npath; npath.length >= 2 && npath[0] == fromNodeId && npath[npath.length - 1] == toNodeId;
@ (\forall int i; 0 <= i && (i < npath.length - 1); containsEdge(npath[i], npath[i + 1])));
@ ensures (fromNodeId == toNodeId) ==> \result == true;
@ also
@ exceptional_behavior
@ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(fromNodeId)); 
@ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(toNodeId));
@*/

　　这个方法与之前的containsEdge类似。从输入上看，输入的是任意两个int类型数据；从输出上看，得到的是一个boolean。这块需要注意的是，当输入的点不在图中时，直接输出false，而不能抛异常；自己和自己在isconnected中是一定为1的。在编写测试数据时，注意不仅要测试两个不是相邻的点，更要测试相邻的两个点。还有，要注意“换乘”的情况。所以，我将测试用例划分成了8类：

1. 两个点都在图中，（直接|间接）相连，不相邻
2. 两个点都在图中，相连，相邻
3. 两个点都在图中，不相连
4. from == to，相连
5. from == to，不相连
6. from不在图中（异常）
7. to不在图中（异常）
8. from和to都不在图中（异常）

我尝试使用ExpectedException类来分析抛出的异常情况，但是总是报错，现在也没有解决。

这两个分明是一样的，但是会报错

•  getShortestPathLength(int fromNodeId, int toNodeId) throws NodeIdNotFoundException, NodeNotConnectedException

/*@ normal_behavior
@ requires (\exists Path path; path.isValid() && containsPath(path); path.containsNode(fromNodeId)) &&
@ (\exists Path path; path.isValid() && containsPath(path); path.containsNode(toNodeId));
@ assignable \nothing;
@ ensures (fromNodeId != toNodeId) ==> (\exists int[] spath; spath.length >= 2 && spath[0] == fromNodeId && spath[spath.length - 1] == toNodeId;
@ (\forall int i; 0 <= i && (i < spath.length - 1); containsEdge(spath[i], spath[i + 1])) &&
@ (\forall Path p; p.isValid() && p.getNode(0) == fromNodeId && p.getNode(p.size() - 1) == toNodeId && 
@ (\forall int i; 0 <= i && (i < p.size() - 1); containsEdge(p.getNode(i), p.getNode(i + 1))); p.size() >= spath.length) &&
@ (\result == spath.length - 1));
@ ensures (fromNodeId == toNodeId) ==> \result == 0;
@ also
@ exceptional_behavior
@ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(fromNodeId)); 
@ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(toNodeId));
@ signals (NodeNotConnectedException e) !(\exists int[] npath; npath.length >= 2 && npath[0] == fromNodeId && npath[npath.length - 1] == toNodeId;
@ (\forall int i; 0 <= i && (i < npath.length - 1); containsEdge(npath[i], npath[i + 1])));
@*/

　　这个函数算是这次作业中的难度巅峰了，但是测试起来一点也不难！这里面要注意的是几种异常情况的抛出，from == to怎么办。我将测试分为 类：

1. 两个点都在图中，相连
2. 两个点都在图中，不相连（异常）
3. from == to，相连
4. from == to，不相连
5. from不在图中（异常）
6. to不在图中（异常）
7. from和to都不在图中（异常）

 由于我没解决对异常抛出的正确性判定，我代码中先不测试了。

JMLUnit测试

　　这块我弄了很长时间，前期一直出现无法导入，正确的命令行是这样的：

java -jar jmlunit-1_4/jmlunitng-1_4.jar -cp Project10_marven/specs-homework-2-1.2-raw-jar-with-dependencies.jar Project10_marven/src/main/java/MyGraph.java

然后就生成了无比多的.java，点击我选中的test文件就可以测试了。测试结果巨长我就只放一小部分了。

       

在这一长串中我发现getpathid和所有remove都是错的，而且都是那种很神奇的数据，比如null、0、maxInt。我觉得可能是因为这些数据没有找到点，就跑出来异常，然后测试就fail了。（因为其他没有throw exception的方法都没有出错）。不过我不知道这样怎么解决，所以先把问题留在这里。

 　　观察发现，随机生成的数据实际上不随机，都是一些边界数据。我发现：

1. 对于int型的变量，数据都为0，-2147483648，2147483647（maxInt）
2. 对于Object的，使用null

所以我认为我不太理解这个玩意的意义，这些数据并不能检测出我大部分的bug。

架构分析

---

 　　必须承认，我这回三次作业都是一锅粥的状况。一方面是时间不太够我去调整结构了，另一方面是我也不太会写标程那种优雅的结构。在分析标程之前，我先回顾一下自己的程序。

　　在三次作业中，我都使用了ThreadMXBean包来测量CPU时间。但是这个时间并不精准，只有一部分的参考性。

• 第一次作业

          

　　先从MyPath说起。我使用了ArrayList数据结构，因为它是动态数组，容量可以自由改变，并且各种操作（即使实现上都是O(n)）非常方便。但是ArrayList相比于静态数组，时间是它最大的弱点。不过我认为，这一点节省的时间对于我们的作业来讲微不足道。

　　之后看一下MyPathContainer，我使用了HashMap创造了一种来回的映射关系，“pathId到Path”和“Path到pathId”。这样做的好处有许多：

1. 查询的时候，可以利用HashMap的hashcode优势，速度极快
2. 动态结构HashMap增删很容易

并且，我建立了mapId这个HashMap，来存储不同的点有多少个。这样，我将时间复杂度全都放在了add和remove中，查询的时候都只是O(1)。

　　　　　　　Iterator itNode = path.iterator();
            while (itNode.hasNext()) {
                int a = (Integer) itNode.next();
                if (mapId.containsKey(a)) {
                    mapId.put(a,mapId.get(a) + 1);
                } else {
                    mapId.put(a,1);
                }
            }

• 第二次作业

   

 

                         

 

 　　为了计算最短路径，必须生成邻接矩阵，那么也就需要记录边与边之间的连接关系。我把这个“记录”行为放在了add和remove中，平坦时间复杂度。由于一条边可能出现多次，所以还需要记录这条边的个数。因而结构体是HashMap<Integer,HashMap<Integer,Integer>>。

// add方法内“标记”边
private void markPath(Path path) {
        int size = path.size();
        for (int i = 0;i < size - 1;i++) {
            int a = path.getNode(i);
            int b = path.getNode(i + 1);
            markEdge(a,b);
            if (a != b) {
                markEdge(b,a);
            }
        }
    }

在初始化邻接矩阵时，会遇到这种情况：需要知道所有点中的第i个点的nodeId；需要知道nodeId是所有点中的第几个点。因而我创建了两个映射专用HashMap，建立这种映射关系。由于会出现add和remove，这种关系经常会被破坏，而缓存机制又过于复杂，所以我选择在初始化邻接矩阵时更新这两个HashMap。

    private void initDistanceMap() {
        Iterator<Integer> it = adjacentMap.keySet().iterator();
        int im = 0;
        nodeLink = new HashMap();
        nodeReverseLink = new HashMap();
        while (it.hasNext()) {
            int key = it.next();
            nodeLink.put(key,im);
            nodeReverseLink.put(im,key);
            im++;
        }
        int size = nodeLink.size();
        distanceMap = new int[size][size];
        for (int i = 0; i < size;i++) {
            for (int j = i; j < size;j++) {
                if (i == j) {
                    distanceMap[i][i] = 0;
                    continue;
                }
                if (containsEdge(nodeReverseLink.get(i),
                        nodeReverseLink.get(j))) {
                    distanceMap[i][j] = 1;
                    distanceMap[j][i] = 1;
                } else {
                    distanceMap[i][j] = inf;
                    distanceMap[j][i] = inf;
                }
            }
        }
    }

HashMap对于映射关系使用起来非常的方便，但是一个巨大的缺点就是它遍历起来非常耗费时间。所以要注意尽量不用HashMap本身进行遍历，尽量利用hashcode。

• 第三次作业

挺好的我这几次作业都是“一类到底”……

　　由于我不太会使用工厂模式，我干脆直接建立了一个“仓库”类（Storage），存储所有的映射关系。除了上次作业中我建立的所有点和标号之间的映射关系，我还建立了针对每一个path之内的这种映射关系。这次作业我的算法主旨是“只改变算法的权值矩阵“。在init函数中，需要遍历每个path。所以我把这个步骤也放在了add和remove中。

        

public void addPathWeight(Path path) {
        int count = path.getDistinctNodeCount();
        int size = path.size();
        int[][][] weight = new int[3][count][count];
        // price: 0 unple: 1 change: 2
        for (int i = 0;i < count;i++) {
            for (int j = i;j < count;j++) {
                if (i == j) {
                    weight[0][i][j] = 0;
                    weight[1][i][j] = 0;
                    weight[2][i][j] = 0;
                }
                weight[0][i][j] = inf;
                weight[0][j][i] = inf;
                weight[1][i][j] = inf;
                weight[1][j][i] = inf;
                weight[2][i][j] = inf;
                weight[2][j][i] = inf;
            }
        }
        HashMap<Integer,Integer> pathNodeLink
                = Storage.getPathNodeLink().get(path);
        for (int i = 0;i < size;i++) {
            for (int j = i;j < size;j++) {
                int n1 = pathNodeLink.get(path.getNode(i));
                int n2 = pathNodeLink.get(path.getNode(j));
                if (j - i < weight[0][n1][n2] || j - i < weight[0][n2][n1]) {
                    weight[0][n1][n2] = j - i;
                    weight[0][n2][n1] = j - i;
                }
                int val = getFakeUnpleasantValue(path,i,j);
                // System.out.println(n1 + " " + n2 + " " + val);
                if (val < weight[1][n1][n2] || val < weight[1][n2][n1]) {
                    weight[1][n1][n2] = val;
                    weight[1][n2][n1] = val;
                }
                weight[2][n1][n2] = 1;
                weight[2][n2][n1] = 1;
            }
        }
　　　　　// 由于有环的情况，所以得对每个path先Floyd一次。
        for (int k = 0;k < count;k++) {
            for (int i = 0; i < count;i++) {
                for (int j = 0; j < count;j++) {
                    for (int l = 0;l < 2;l++) {
                        int sum = weight[l][i][k] + weight[l][k][j];
                        if (weight[l][i][j] > sum) {
                            weight[l][i][j] = sum;
                            weight[l][j][i] = sum;
                        }
                    }
                }
            }
        }

        HashMap<Path,int[][][]> weightMap = Storage.getWeightMap();
        weightMap.put(path,weight);
        Storage.setWeightMap(weightMap);
    }

• 标程分析

           

我的图从来没有画的这么整齐过……

 　　Graph和Map方法的核心都在几个core类中。那addEdge举例，core类中存放的是比较”底层“的方法，而在MyGraph类中则调用core的方法，因而很清晰。假如未来的作业中变成了有向图，改动也不是很大。

      

　　我一直不明白的是这次作业怎么建立工厂，看了标程有一点明白了。首先建立一个factory接口，之后建立针对不同种图的几种工厂。在这几个工厂中，都有构造方法、init方法、权重方法、计算方法和更新方法。这样做的好处是可以应付各种图的需求。

bug情况

---

　　这几次作业我都没有被强测或者在互测中测出bug。\(O_-)/而且由于组内同学太强了，我也没有找到他们的bug……但是我还是有一些心得可以分享。

　　这次测试我采用的是黑盒测试（随机测试）+白盒测试（定点测试）的方式。我首先对写的每一个方法使用Junit进行测试，之后从整个工程的方面进行测试。

Junit测试

　　前文提到了，在此不赘述。(0_0)

黑盒测试

　　纯随机数据，生成各种意想不到的情况。感谢默默同学写的随即数据生成器，由于我没有版权，不放代码啦！真的是很棒！

白盒测试

　　白盒测试分为两个阶段，分别针对可能发生的不同种情况。我将拿第三次作业举例。

• 第一阶段：针对于实现方法的具体测试。

　　　// 这是初始化一种映射关系的方法
　　　protected void initLink() {
        HashMap<Integer,HashMap<Integer,Integer>>
                adjacentMap = Storage.getAdjacentMap();
        Iterator<Integer> it = adjacentMap.keySet().iterator();
　　　　　// 每次初始化的适合，必须new新的
        HashMap<Integer,Integer> nodeLink = new HashMap<>();
        HashMap<Integer,Integer> nodeReverseLink = new HashMap<>();
        int im = 0;
        while (it.hasNext()) {
            int key = it.next();
            nodeLink.put(key,im);
            nodeReverseLink.put(im,key);
            im++;
        }
        Storage.setNodeLink(nodeLink);
        Storage.setReverseNodeLink(nodeReverseLink);
    }

　　测试上面的方法，需要有几种测试数据。比如既要有add 1 2 3 remove 3这种，也要有add 1 2 3 remove 2这种能够创造出{1 x 3}的数据。如果在代码段中我标注的部分没有new，那么就会报错。

• 第二阶段：针对总体架构的测试

　　在测试了单个方法之后，需要创造数据来测试方法之间是否能够成功协作。创造数据时，改变查询顺序或者查询次数，能获得一致的查询结果。

改变查询顺序：

PATH_ADD 1 2 3 4 5 6 2

PATH_ADD 3 2 8 9 1 2

第一组：

{GET_SHORTEST_PATH_LENGTH 3 6

GET_LEAST_UNPLESENT_VALUE 3 6

GET_LEAST_TICKET_PRICE 3 6

GET_LEAST_CHANGE_COUNT 3 6}

第二组：

{GET_LEAST_UNPLESENT_VALUE 3 6

GET_LEAST_TICKET_PRICE 3 6

GET_LEAST_CHANGE_COUNT 3 6

GET_SHORTEST_PATH_LENGTH 3 6}

……

改变查询次数：

PATH_ADD 1 2 3 4 5 6 2

PATH_ADD 3 2 8 9 1 2

GET_LEAST_UNPLESENT_VALUE 3 6

GET_LEAST_UNPLESENT_VALUE 3 6

GET_LEAST_UNPLESENT_VALUE 3 6

GET_LEAST_UNPLESENT_VALUE 3 6
　　需要特别注意的一点是连通块的方法。由于我的连通块使用的是dfs不是权值矩阵，所以这个方法调用时也会更新所有map之后计算。这里的flag标志位就有可能产生问题。比如我的代码如果先计算连通块，再进行其他的查询，我就会陷入无尽的更新循环之中。在测试中用我写的方法，是可以测试出来问题的。但是随即数据就不一定了！

心得体会

---

对JML的思考

　　这几次虽然很认真地学习了JML规格，但是实际上自己写的时候并不能很好地将JML与代码进行结合，有些地方没有认真注意：

1. 严格保证方法结果，不能私加内容
2. 可以利用规格生成随即数据进行测试（JMLUnitNG）

　　但是我也学到了很多，比如：

1. 先查看先行条件；再查看结果保证
2. 查看修改的变量，思考其是不是需要维护
3. 规格不束缚自己的实现方式
4. 规格书写：只能调用pure方法；有许多能简化书写内容的结构（exists | forall）；……

对数据结构的思考

　　需要的是性能 + 方便使用结合。所以我自认为这回我写的映射机制是很好的。另外对于一些容器，一定要去看底层代码，因为有些时候自己觉得是O(1)的方法，可能不是！详见ArrayList。

总结

---

　　这个单元非常有意思，经常是自己担心的事情没有发生，而没去考虑的却导致WA声一片。比如第三次作业，我先开始使用的是Dijstra+部分缓存，后来离作业截至前两三个小时才发现自己的缓存功能有问题！后来全都改成了Floyd。但是更加戏剧化的是，我的Floyd的三层循环顺序给写反了！这个错误，还不是每次都能够显现出来，是需要一个比较大的测试集的。这些问题，都是我没思考过的。而我最担心的时间问题，最后发现强测中我最长CPU时间也只有6s左右。难怪助教说WA比TLE容易的多！

　　最后感谢同学们在讨论区各种发言，我受益匪浅！我们一起征战最后的一单元！