OO_JAVA_JML系列做业_单元总结

OO_JAVA_JML系列做业_单元总结

(1)梳理JML语言的理论基础、应用工具链状况

简单梳理

如下三者是jml规格里的核心，对一个方法功能和属性的限制：

1. requires子句：规定方法的前置条件(precondition)；
2. assignable子句：方法的反作用范围限定；
3. ensures子句：规定方法的后置条件(post condition)。

简单运用

采用OpenJML工具check第一次JML官方开源库代码获得以下结果：

对比第一次和第二次JML规格官方源码：

第一次：

/*@ public normal_behavior
      @ requires path != null && path.isValid() && \old(containsPath(path));
      @ assignable pList, pidList;
      @ ensures containsPath(path) == false;
      @ ensures (pidList.length == pList.length);
      @ ensures (\exists int i; 0 <= i && i < \old(pList.length); \old(pList[i].equals(path)) &&
      @           \result == \old(pidList[i]));
      @ also
      @ public exceptional_behavior
      @ assignable \nothing;
      @ signals (PathNotFoundException e) path == null;
      @ signals (PathNotFoundException e) path.isValid()==false;
      @ signals (PathNotFoundException e) !containsPath(path);
      @*/
    public int removePath(Path path) throws PathNotFoundException;

第二次：

/*@ public normal_behavior
      @ requires path != null && path.isValid() && containsPath(path);
      @ assignable pList, pidList;
      @ ensures containsPath(path) == false;
      @ ensures (\exists int i; 0 <= i && i < \old(pList.length); \old(pList[i].equals(path)) &&
      @           \result == \old(pidList[i]));
      @ ensures (\forall int i; 0 <= i && i < \old(pList.length) && \old(pList[i].equals(path) == false);
      @          containsPath(\old(pList[i])) && containsPathId(\old(pidList[i])));
      @ also
      @ public exceptional_behavior
      @ assignable \nothing;
      @ signals (PathNotFoundException e) path == null;
      @ signals (PathNotFoundException e) path.isValid() == false;
      @ signals (PathNotFoundException e) !containsPath(path);
      @*/
    public int removePath(Path path) throws PathNotFoundException;

发现问题根源在于requires判据自己就发生在该方法执行前，\old条件没法在此应用，由于，requires执行时就已是old的数据了。

(2)部署SMT Solver，至少选择3个主要方法来尝试进行验证，报告结果，有可能要补充JML规格

(3)部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例， 并结合规格对生成的测试用例和数据进行简要分析

对本身编写的graph接口的实现类MyGraph运行JMLUnitNG结果是这样：

➜  src git:(master) ✗ jmlunitng -cp ~/javalib/specs-homework-2-1.2-raw-jar-with-dependencies.jar container/MyGraph.java 
JMLUnitNG exited because of an irrecoverable error: 
org.jmlspecs.jmlunitng.JMLUnitNGError: Encountered 100 compilation errors: 
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:21: 错误: 非法的类型开始
    private HashMap<SymPair<Integer>, Integer> edges = new HashMap<>();
                                                                   ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:24: 错误: 非法的类型开始
            shortestRoutes = new HashMap<>();
                                         ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:37: 错误: 非法的类型开始
        return edges.containsKey(new SymPair<>(var1, var2));
                                             ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:49: 错误: 非法的类型开始
        if (!shortestRoutes.containsKey(new SymPair<>(var1, var2))) {
                                                    ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:52: 错误: 非法的类型开始
        return shortestRoutes.containsKey(new SymPair<>(var1, var2));
                                                      ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:61: 错误: 非法的类型开始
        return shortestRoutes.get(new SymPair<>(var1, var2));
                                              ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:68: 错误: 须要')'
        updateEdges(path, this::edgeAddingConsumer);
                              ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:68: 错误: 非法的表达式开始
        updateEdges(path, this::edgeAddingConsumer);
                               ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:68: 错误: 须要';'
        updateEdges(path, this::edgeAddingConsumer);
                                                  ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:76: 错误: 须要')'
        updateEdges(path, this::edgeRemovingConsumer);
                              ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:76: 错误: 非法的表达式开始
        updateEdges(path, this::edgeRemovingConsumer);
                               ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:76: 错误: 须要';'
        updateEdges(path, this::edgeRemovingConsumer);

...

可见的是，JMLUnitNG至少不支持两种特性：

1. 泛型的自动推断特性，在声明处已经声明的泛型，在new实例化时，不须要填充泛型类型，编译器能够自动推断，可是JMLUnitNG不支持；
2. 函数式接口的两种形式都不支持，不管是方法引用的双冒号，仍是lambda表达式。

不支持上述特性，不可思议其普遍运用。

(4)按照做业梳理本身的架构设计，并特别分析迭代中对架构的重构

第一次做业

说实话，跟大部分人相同，path container采用三个hash map莽到底，规格很简单，功能很简单，正确性容易达成。

第二次做业

这个也没有什么特点，就是BFS能用，便采用这个算法计算最短路径了，想必跟大部分人也是大同小异的设计。

正确性方面仍是较为容易达成的，强测和互测都没有发现bug。

第三次做业

联通集计算

经过一个map来保留联通集的信息，其原理在于单个path内部的连通性是能够保障的，就能够在path ID的基础上创建联通集，我也是这么作的，一个pathID映射该path联通的pathID的集合，这样，就能够在线性时间内完成一次path的添加工做，其线性时间，主要依赖path自己的长度，因为我看见你们都是提到DFS能解决连通性的问题，就这么设计了，因此，我在这里大概说一下个人不同的联通集的设计思路。

做业架构感想

说实话，没有算法，架构只是纸上谈兵，这是我第三次做业的感想，选择了最朴素的分离解耦的思惟，可是在算法上，复杂度太高，没有充分考虑可缓存的，没有充分考虑遍历的控制，虽然下降了每一个方法的复杂度，但这样的程序，是没有实际价值的，换言之，我大部分是作了无用功；

到如今，我也没设计出本身的完成第三次做业的思路，虽然学习别人的思路是必要的，我仍是想弄清楚，怎样的缘由致使了个人遍历没法达到想要的效果，而后深入理解怎样设计遍历算法，这是我想探究的事物。

我对搜索自己有了更深入的理解，所谓遍历，究其目的，就是寻找要寻找的目标，或者是在肯定的线性集合里搜索，或者是在有更加特殊的结构的集合里搜索，为了完成这个任务，就要有无数优化加入其中，最朴素的，就是排序，排序能够极大的加快搜索的过程，放在单纯的线性集合里，排序能够将集合视为二分集，进行二叉树上的搜索，达到最高的静态集合的搜索效率，而在图结构里，搜索单源最短路径，也能够利用相似的方法，即dijkstra算法，每次根据基础集合从待选集合中搜索路径长度最小的一个，加入基础集合，变相地实现了排序的要求，排序的目的，就旨在滤除不须要的数据或数据集合，将其提早排除，加速搜索的过程。

总的来讲，对集合的遍历操做十分依赖集合自己的结构，没有排序这样的优化，计算就永远是暴力计算，是不可取的。

(5)按照做业分析代码实现的bug和修复状况

这个。。第一次有一个bug可是比较隐蔽，强测和互测均未发现，最后是我在第二次做业编写中发现的，而且就排除掉了，是两个path compare的函数的错误，第二次做业最后经过了强测和互测，没有发现bug；

第三次做业，至今为止，我仍是没有设计出遍历算法或者遍历同时计算的算法，保证计算的彻底性的算法，没有这个，计算出的结果，就不能肯定是最小值。

目前还在思考修复中，也许若是不采用讨论区大佬提的拆点算法了话，可能暂时修复不出来。

(6)阐述对规格撰写和理解上的心得体会

规格是对方法结果的一种约束，能够做为需求的一种清晰表述，利于针对其进行规范详尽的测试，由于结果都用可证实的形式描述出来，因此针对jml规格，能够采用更加针对性的测试，测试单个函数的功能正确性，并进一步提升junit的测试手段。

有了完善的规格，必定程度上，有利于咱们写出更加正确的程序，固然，其做用主要仍是测试方面，根据规格能够更加形式化地验证，乃至采用自动化地方法生成测试程序，甚至测试数据，这都是可能的。