OO第三单元总结性博客

JML理论基础与工具链

JML理论基础

JML是一种将java程序规格化表达的一种语言，其描述的是行为的规格，而非具体的代码实现。

通过对程序开展规格化设计，当然前提是使用JML这种规范化的语言，可以使得代码具有严谨的逻辑，因为代码的实现一定按照规格去实现，而规格是逻辑严谨的。

同时代码的可维护性进一步提高，书写规格保证了可以在不写代码的情况下，首先描述其功能，等到需要写的时候再进行代码书写，提高可维护性。

工具链

一系列JML相关的支持工具为开发者提供了便捷的验证与构造方法，为JML的传播起到了积极作用。下面我总结了一些实用的，建议在JML规格语言之上的工具。

  • OpenJml

    一个可以自动检测JML规范的插件

  • JMLdoc与JMLunit

    前者与javadoc类似，后者可自动生成测试

SMT Solver部署与部分方法验证

下载OpenJML的jar文件，并进行测试。

由于并未部署环境，采用命令java -jar <path>/openjml.jar -esc <soursefile>进行验证与处理，我用第三次作业的MyPath.java。

首先进行语法检测

 1 chenrenjiedeMacBook-Pro:openjml-0.8.42-20190401 chenrenjie$ java -jar openjml.jar -cp /Users/chenrenjie/Desktop/TEST/specs-homework-3-1.3-raw-jar-with-dependencies.jar -check /Users/chenrenjie/Desktop/TEST/src/MyPath.java
 2 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:63: 错误: 找不到符号
 3       @ ensures \result == (((Path) obj).nodes.length == nodes.length) &&
 4                                       ^
 5   符号:   变量 nodes
 6   位置: 接口 Path
 7 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:64: 错误: 找不到符号
 8       @                      (\forall int i; 0 <= i && i < nodes.length; nodes[i] == ((Path) obj).nodes[i]);
 9                                                                                                  ^
10   符号:   变量 nodes
11   位置: 接口 Path
12 2 个错误

View Code

将Path改成MyPath后，再检查一次

1 chenrenjiedeMacBook-Pro:openjml-0.8.42-20190401 chenrenjie$ java -jar openjml.jar -cp /Users/chenrenjie/Desktop/TEST/specs-homework-3-1.3-raw-jar-with-dependencies.jar -check /Users/chenrenjie/Desktop/TEST/src/MyPath.java
2 chenrenjiedeMacBook-Pro:openjml-0.8.42-20190401 chenrenjie$

View Code

可通过语法检测

再进行代码静态检查

  1 chenrenjiedeMacBook-Pro:openjml-0.8.42-20190401 chenrenjie$ java -jar openjml.jar -cp /Users/chenrenjie/Desktop/TEST/specs-homework-3-1.3-raw-jar-with-dependencies.jar -esc /Users/chenrenjie/Desktop/TEST/src/MyPath.java
  2 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:18: 警告: The prover cannot establish an assertion (PossiblyNegativeIndex) in method MyPath
  3             arrayList.add(nodeList[i]);
  4                                   ^
  5 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:13: 警告: The prover cannot establish an assertion (NullField) in method MyPath
  6     //@ public instance model non_null int[] nodes;
  7                                              ^
  8 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:113: 警告: The prover cannot establish an assertion (PossiblyBadCast) in method compareTo:  a java.lang.Object cannot be proved to be a java.lang.Integer
  9             Integer integer1 = (Integer) iterator1.next();
 10                                ^
 11 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:114: 警告: The prover cannot establish an assertion (PossiblyBadCast) in method compareTo:  a java.lang.Object cannot be proved to be a java.lang.Integer
 12             Integer integer2 = (Integer) iterator2.next();
 13                                ^
 14 openjml.jar(specs/java/util/Collection.jml):70: 警告: The prover cannot establish an assertion (Invariant) in method compareTo
 15     //-RAC@ public invariant content.owner == this;
 16                    ^
 17 openjml.jar(specs/java/util/Collection.jml):71: 警告: The prover cannot establish an assertion (Invariant) in method compareTo
 18     //-RAC@ public invariant content.theSize >= 0;
 19                    ^
 20 openjml.jar(specs/java/util/Map.jml):76: 警告: The prover cannot establish an assertion (Invariant) in method compareTo
 21         public invariant content.owner == this;
 22                ^
 23 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:46: 警告: The prover cannot establish an assertion (Postcondition: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:44: 注: ) in method containsNode
 24         return this.node.containsKey(node);
 25         ^
 26 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:44: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:46: 注:
 27     //@ ensures \result == (\exists int i; 0 <= i && i < nodes.length; nodes[i] == node);
 28         ^
 29 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:73: 警告: The prover cannot establish an assertion (Assignable: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 注: ) in method equals:  \everything
 30             if (((Path) obj).size() == this.size()) {
 31                                  ^
 32 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:73: 注:
 33       @ public normal_behavior
 34                ^
 35 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:74: 警告: The prover cannot establish an assertion (Assignable: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 注: ) in method equals:  \everything
 36                 Iterator iterator = ((Path) obj).iterator();
 37                                                          ^
 38 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:74: 注:
 39       @ public normal_behavior
 40                ^
 41 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:76: 警告: The prover cannot establish an assertion (Assignable: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 注: ) in method equals:  moreElements
 42                     Integer integer1 = (Integer) iterator.next();
 43                                                               ^
 44 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:76: 注:
 45       @ public normal_behavior
 46                ^
 47 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:76: 警告: The prover cannot establish an assertion (Assignable: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 注: ) in method equals:  remove_called_since
 48                     Integer integer1 = (Integer) iterator.next();
 49                                                               ^
 50 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:76: 注:
 51       @ public normal_behavior
 52                ^
 53 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:76: 警告: The prover cannot establish an assertion (Assignable: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 注: ) in method equals:  objectState
 54                     Integer integer1 = (Integer) iterator.next();
 55                                                               ^
 56 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:76: 注:
 57       @ public normal_behavior
 58                ^
 59 openjml.jar(specs/java/util/Collection.jml):70: 警告: The prover cannot establish an assertion (Invariant) in method equals
 60     //-RAC@ public invariant content.owner == this;
 61                    ^
 62 openjml.jar(specs/java/util/Collection.jml):71: 警告: The prover cannot establish an assertion (Invariant) in method equals
 63     //-RAC@ public invariant content.theSize >= 0;
 64                    ^
 65 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:81: 警告: The prover cannot establish an assertion (Postcondition: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:63: 注: ) in method equals
 66                 return true;
 67                 ^
 68 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:63: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:81: 注:
 69       @ ensures \result == (((MyPath) obj).nodes.length == nodes.length) &&
 70         ^
 71 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:63: 警告: The prover cannot establish an assertion (UndefinedBadCast) in method equals:  a java.lang.Object cannot be proved to be a MyPath
 72       @ ensures \result == (((MyPath) obj).nodes.length == nodes.length) &&
 73                              ^
 74 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:81: 警告: Associated method exit
 75                 return true;
 76                 ^
 77 openjml.jar(specs/java/util/Map.jml):76: 警告: The prover cannot establish an assertion (Invariant) in method equals
 78         public invariant content.owner == this;
 79                ^
 80 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:76: 警告: The prover cannot establish an assertion (PossiblyBadCast) in method equals:  a java.lang.Object cannot be proved to be a java.lang.Integer
 81                     Integer integer1 = (Integer) iterator.next();
 82                                        ^
 83 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:78: 警告: The prover cannot establish an assertion (Postcondition: openjml.jar(specs/java/lang/Object.jml):78: 注: ) in method equals
 84                         return false;
 85                         ^
 86 openjml.jar(specs/java/lang/Object.jml):78: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:78: 注:
 87       @     ensures \result;
 88             ^
 89 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:76: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 注: ) in method equals
 90                     Integer integer1 = (Integer) iterator.next();
 91                                                               ^
 92 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:76: 注:
 93       @ public normal_behavior
 94                ^
 95 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:76: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: openjml.jar(specs/java/lang/Object.jml):76: 注: ) in method equals
 96                     Integer integer1 = (Integer) iterator.next();
 97                                                               ^
 98 openjml.jar(specs/java/lang/Object.jml):76: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:76: 注:
 99       @   public normal_behavior
100                  ^
101 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:56: 警告: The prover cannot establish an assertion (Postcondition: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:50: 注: ) in method getDistinctNodeCount
102         return node.size();
103         ^
104 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:50: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:56: 注:
105       @ ensures (\exists int[] arr; (\forall int i, j; 0 <= i && i < j && j < arr.length; arr[i] != arr[j]);
106         ^
107 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:40: 警告: The prover cannot establish an assertion (Postcondition: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:37: 注: ) in method getNode
108         return arrayList.get(index);
109         ^
110 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:37: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:40: 注:
111       @ ensures \result == nodes[index];
112         ^
113 错误: ESC could not be attempted because of a failure in typechecking or AST transformation: getUnpleasantValue
114 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:138: 警告: The prover cannot establish an assertion (Postcondition: openjml.jar(specs/java/lang/Object.jml):63: 注: ) in method hashCode
115         return Arrays.hashCode(arrayList.toArray());
116         ^
117 openjml.jar(specs/java/lang/Object.jml):63: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:138: 注:
118     //-RAC@ ensures \result == theHashCode;
119             ^
120 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:31: 警告: The prover cannot establish an assertion (Postcondition: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:28: 注: ) in method size
121         return arrayList.size();
122         ^
123 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:28: 警告: Associated declaration: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:31: 注:
124       @ ensures \result == nodes.length;
125         ^
126 41 个警告

View Code

发现了很多警告，选择其中三个进行分析：

  • 分析样例一

 1 //@ public instance model non_null int[] nodes;
 2 public MyPath(int[] nodeList) {
 3     arrayList = new ArrayList<>();
 4     node = new HashMap<>();
 5     for (int i = 0; i < nodeList.length; i++) {
 6         arrayList.add(nodeList[i]);
 7         if (node.containsKey(nodeList[i])) {
 8             node.put(nodeList[i], node.get(nodeList[i]) + 1);
 9         } else {
10             node.put(nodeList[i], 1);
11         }
12     }
13 }

View Code

1 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:18: 警告: The prover cannot establish an assertion (PossiblyNegativeIndex) in method MyPath
2             arrayList.add(nodeList[i]);
3                                   ^

View Code

　　这里表现的是PossiblyNegativeIndex的问题，即下标可能为负数，代码如下这里描述的是下标可能为负数的情况，但事实上下标不会为负数。

  • 分析样例二

1 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:76: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: /Users/chenrenjie/Desktop/TEST/src/MyPath.java:60: 注: ) in method equals
2                     Integer integer1 = (Integer) iterator.next();
3                                                               ^

View Code

 1 public boolean equals(Object obj) {
 2     if (obj instanceof Path) {
 3         if (((Path) obj).size() == this.size()) {
 4             Iterator iterator = ((Path) obj).iterator();
 5             for (Integer integer : this) {
 6                 Integer integer1 = (Integer) iterator.next();
 7                 if (!Objects.equals(integer, integer1)) {
 8                     return false;
 9                 }
10             }
11             return true;
12         }
13         return false;
14     } else {
15         return false;
16     }
17 }

View Code

这里用到了强制类型转换，将一个Obj类强制转换成Integer，而这样的转换是有风险的，故产生了警告。

  • 分析样例三

    1 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:63: 警告: The prover cannot establish an assertion (UndefinedBadCast) in method equals:  a java.lang.Object cannot be proved to be a MyPath
2       @ ensures \result == (((MyPath) obj).nodes.length == nodes.length) &&
3                              ^

    View Code

    这是规格中的转换问题，这种转换是不好的声明。

通过上述三个例子的分析，可以看到静态检查是在充分考虑了各种情况后进行的检查，其具有普适应，而对于独特的程序，有时候这种检查过于繁琐，往往会出现一些本不可能产生的情况，仍然被报警告。

JMLUnitNG部署与测试用例生成

针对本次作业的Graph和Path，分别进行了测试，结果都是失败的。原因可能是在我的程序中无法对单独的java文件进行测试，其文件相互有所依赖。致使如下结果

  1 chenrenjiedeMacBook-Pro:Desktop chenrenjie$ java -jar jmlunitng.jar -cp /Users/chenrenjie/Desktop/TEST3/specs-homework-2-1.2-raw-jar-with-dependencies.jar -sp /Users/chenrenjie/Desktop/specs-homework-3-opensource/src/main/java -d test /Users/chenrenjie/Desktop/TEST/src/MyPath.java
  2 JMLUnitNG exited because of an irrecoverable error:
  3 org.jmlspecs.jmlunitng.JMLUnitNGError: Encountered 16 compilation errors:
  4 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:15: 错误: 非法的类型开始
  5         arrayList = new ArrayList<>();
  6                                   ^
  7 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:16: 错误: 非法的类型开始
  8         node = new HashMap<>();
  9                            ^
 10 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:1: 错误: 程序包com.oocourse.specs3.models不存在
 11 import com.oocourse.specs3.models.Path;
 12                                  ^
 13 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:1: 错误: 程序包com.oocourse.specs3.models不存在
 14 import com.oocourse.specs3.models.Path;
 15                                  ^
 16 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/ArrayList.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 17   建议升级此编译器。
 18 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/AbstractList.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 19   建议升级此编译器。
 20 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/AbstractCollection.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 21   建议升级此编译器。
 22 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Object.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 23   建议升级此编译器。
 24 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Collection.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 25   建议升级此编译器。
 26 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Iterable.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 27   建议升级此编译器。
 28 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/List.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 29   建议升级此编译器。
 30 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/AbstractList$ListItr.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 31   建议升级此编译器。
 32 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/AbstractList$Itr.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 33   建议升级此编译器。
 34 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/RandomAccess.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 35   建议升级此编译器。
 36 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Cloneable.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 37   建议升级此编译器。
 38 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/io/Serializable.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 39   建议升级此编译器。
 40 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/ArrayList$ArrayListSpliterator.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 41   建议升级此编译器。
 42 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/ArrayList$SubList.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 43   建议升级此编译器。
 44 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/ArrayList$ListItr.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 45   建议升级此编译器。
 46 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/ArrayList$Itr.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 47   建议升级此编译器。
 48 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 49   建议升级此编译器。
 50 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/AbstractMap.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 51   建议升级此编译器。
 52 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Map.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 53   建议升级此编译器。
 54 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Map$Entry.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 55   建议升级此编译器。
 56 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/AbstractMap$SimpleImmutableEntry.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 57   建议升级此编译器。
 58 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/AbstractMap$SimpleEntry.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 59   建议升级此编译器。
 60 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$TreeNode.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 61   建议升级此编译器。
 62 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$EntrySpliterator.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 63   建议升级此编译器。
 64 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$ValueSpliterator.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 65   建议升级此编译器。
 66 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$KeySpliterator.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 67   建议升级此编译器。
 68 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$HashMapSpliterator.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 69   建议升级此编译器。
 70 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$EntryIterator.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 71   建议升级此编译器。
 72 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$ValueIterator.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 73   建议升级此编译器。
 74 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$KeyIterator.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 75   建议升级此编译器。
 76 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$HashIterator.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 77   建议升级此编译器。
 78 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$EntrySet.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 79   建议升级此编译器。
 80 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$Values.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 81   建议升级此编译器。
 82 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$KeySet.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 83   建议升级此编译器。
 84 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap$Node.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 85   建议升级此编译器。
 86 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Iterator.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 87   建议升级此编译器。
 88 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Arrays.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 89   建议升级此编译器。
 90 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Arrays$ArrayList.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 91   建议升级此编译器。
 92 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Arrays$LegacyMergeSort.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 93   建议升级此编译器。
 94 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Arrays$NaturalOrder.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 95   建议升级此编译器。
 96 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Objects.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
 97   建议升级此编译器。
 98 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:9: 错误: 找不到符号
 99 public class MyPath implements Path {
100                                ^
101   符号: 类 Path
102 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Integer.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
103   建议升级此编译器。
104 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Number.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
105   建议升级此编译器。
106 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Comparable.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
107   建议升级此编译器。
108 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Integer$IntegerCache.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
109   建议升级此编译器。
110 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:109: 错误: 找不到符号
111     public int compareTo(Path o) {
112                          ^
113   符号:   类 Path
114   位置: 类 MyPath
115 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/ArrayList.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()': 找不到jdk.Profile+Annotation的类文件
116 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/AbstractList.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
117 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/AbstractCollection.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
118 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Object.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
119 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Collection.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
120 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Iterable.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
121 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/List.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
122 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/RandomAccess.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
123 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Cloneable.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
124 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/io/Serializable.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
125 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/HashMap.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
126 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/AbstractMap.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
127 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Map.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
128 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Iterator.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
129 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Arrays.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
130 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/util/Objects.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
131 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Integer.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
132 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Number.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
133 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Comparable.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
134 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Annotation.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
135   建议升级此编译器。
136 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Override.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
137   建议升级此编译器。
138 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Retention.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
139   建议升级此编译器。
140 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/annotation/RetentionPolicy.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
141   建议升级此编译器。
142 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Annotation.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
143 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Target.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
144   建议升级此编译器。
145 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/annotation/ElementType.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
146   建议升级此编译器。
147 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Override.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
148 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Retention.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
149 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/annotation/RetentionPolicy.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
150 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Target.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
151 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/annotation/ElementType.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
152 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/AutoCloseable.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
153   建议升级此编译器。
154 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/AutoCloseable.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
155 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:16: 错误: 类型变量数目错误; 需要2
156         node = new HashMap<>();
157                           ^
158 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/String.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
159   建议升级此编译器。
160 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/String.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
161 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Byte.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
162   建议升级此编译器。
163 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Byte.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
164 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Character.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
165   建议升级此编译器。
166 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Character.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
167 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Short.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
168   建议升级此编译器。
169 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Short.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
170 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/RuntimeException.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
171   建议升级此编译器。
172 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/RuntimeException.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
173 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:72: 错误: 找不到符号
174         if (obj instanceof Path) {
175                            ^
176   符号:   类 Path
177   位置: 类 MyPath
178 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:73: 错误: 找不到符号
179             if (((Path) obj).size() == this.size()) {
180                   ^
181   符号:   类 Path
182   位置: 类 MyPath
183 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:74: 错误: 找不到符号
184                 Iterator iterator = ((Path) obj).iterator();
185                                       ^
186   符号:   类 Path
187   位置: 类 MyPath
188 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:75: 错误: for-each 不适用于表达式类型
189                 for (Integer integer : this) {
190                                        ^
191   要求: {1}
192   找到:    {0}
193 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:61: 错误: 找不到符号
194       @ requires obj != null && obj instanceof Path;
195                                                ^
196   符号:   类 Path
197   位置: 类 MyPath
198 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:67: 错误: 找不到符号
199       @ requires obj == null || !(obj instanceof Path);
200                                                  ^
201   符号:   类 Path
202   位置: 类 MyPath
203 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Math.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
204   建议升级此编译器。
205 /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Math.class): 警告: 无法找到类型 'Profile+Annotation' 的注释方法 'value()'
206 警告: /Library/Java/JavaVirtualMachines/jdk1.8.0_201.jdk/Contents/Home/lib/ct.sym(META-INF/sym/rt.jar/java/lang/Math$RandomNumberGeneratorHolder.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
207   建议升级此编译器。
208 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:108: 错误: 方法不会覆盖或实现超类型的方法
209     @Override
210     ^
211 /Users/chenrenjie/Desktop/TEST/src/MyPath.java:131: 错误: 方法不会覆盖或实现超类型的方法
212     @Override
213     ^
214 /Users/chenrenjie/Desktop/specs-homework-3-opensource/src/main/java/com/oocourse/specs3/models/Path.java:3: 错误: 找不到符号
215 public interface Path extends Iterable<Integer>, Comparable<Path> {
216                                                             ^
217   符号: 类 Path
218
219     at org.jmlspecs.jmlunitng.JMLUnitNG.processAllCompilationUnits(JMLUnitNG.java:527)
220     at org.jmlspecs.jmlunitng.JMLUnitNG.run(JMLUnitNG.java:414)
221     at org.jmlspecs.jmlunitng.JMLUnitNG.main(JMLUnitNG.java:177)

View Code

那么换一个java文件进行尝试。

 1 public class compare {
 2     /*@ public normal_behaviour
 3       @ ensures \result == lhs - rhs;
 4     */
 5     public static int compare(int lhs, int rhs) {
 6         return lhs - rhs;
 7     }
 8
 9     public static void main(String[] args) {
10         compare(114514, 1919810);
11     }
12 }

View Code

模拟这样的测试，来源于讨论区，运行命令

1 chenrenjiedeMacBook-Pro:Desktop chenrenjie$ java -jar /Users/chenrenjie/Desktop/jmlunitng.jar /Users/chenrenjie/Desktop/demo/src/compare.java

View Code

可以得到如下结果

再进行如下命令

1 chenrenjiedeMacBook-Pro:Desktop chenrenjie$ javac -cp /Users/chenrenjie/Desktop/jmlunitng.jar /Users/chenrenjie/Desktop/demo/src/*.java

View Code

可成功编译，再执行openjml的指令

1 chenrenjiedeMacBook-Pro:openjml-0.8.42-20190401 chenrenjie$ java -jar openjml.jar -rac /Users/chenrenjie/Desktop/demo/src/compare.java

View Code

最后运行

1 chenrenjiedeMacBook-Pro:Desktop chenrenjie$ java -classpath /Users/chenrenjie/Desktop/jmlunitng.jar:/Users/chenrenjie/Desktop/demo/src compare_JML_Test

View Code

得到结果如下

 1 [TestNG] Running:
 2   Command line suite
 3
 4 Passed: racEnabled()
 5 Passed: constructor compare()
 6 Passed: constructor compare(-2147483648, -2147483648)
 7 Failed: constructor compare(0, -2147483648)
 8 Failed: constructor compare(2147483647, -2147483648)
 9 Passed: constructor compare(-2147483648, 0)
10 Passed: constructor compare(0, 0)
11 Passed: constructor compare(2147483647, 0)
12 Failed: constructor compare(-2147483648, 2147483647)
13 Passed: constructor compare(0, 2147483647)
14 Passed: constructor compare(2147483647, 2147483647)
15 Passed: static main(null)
16 Passed: static main({})
17
18 ===============================================
19 Command line suite
20 Total tests run: 13, Failures: 3, Skips: 0
21 ===============================================

View Code

可以看到，其主要是用了一些边界数据进行比较，这样有助于极端情况下的测试。

但对于一些复杂的java文件，这种样例的构造往往很困难。

架构设计梳理

三次作业仍然是增量式的设计，在每次设计上增加新的功能，大范围的保持原架构的不变。

  • 第一次作业

    按照指导书的要求完成两个类，分别实现各种方法即可。需要注意的是，为了更好的控制复杂度，最好采用相关复杂度低的容器，比如用hashmap完成查找这一功能。

    对于MyPath内部，只需要构建一个arraylist去顺序存储其nodeid，从而使得index的索引复杂度为O(1)，而后构建一个key = nodeid, value = count的hashmap，可以很方便的统计不同节点的个数。

    对于MyPathContainer，需要完成path与index的双向映射，还需要一个hashmap去储存所有的node与引用次数，由此可以很快速的统计出不同的节点。

    对于增删操作，只需要对不同的节点的次数进行减1，并将双向映射相应修改即可。

  • 第二次作业

    在第一次作业的基础上增加一些新的数据结构，为了使得代码修改量小，便直接在原来的基础上增加代码，而不进行重构的修改。

    首先从一个单一的容器的结构，变成一个图结构，并且还需要对图中的邻接情况，最短路径等进行考虑，因此需要引入邻接矩阵，其表现形式为HashMap<nodeid, HashMap<nodeid, count>>，从而每个节点都有一个hashmap去储存着邻接的节点与引用次数，相应的增删也需要对矩阵进行修改。而后引入同样的结构的最短距离矩阵，以作为一个缓存，显然每当增删的时候，需要对其进行清空。

    关于isconnect方法的处理，由于此次作业的边权值为1，可以直接采用BFS的方法处理，这样处理速度快，效率高，可以中间缓存大量的节点而非一个节点的最短距离。

    此处的不足之处在于并未进行双向缓存，以及一次BFS仅仅截止到了终点，事实上是可以全部遍历完全的，有时候这样效率可能会更高一些。

    其他的内容均与第一次作业保持一直，这样的设计增加了复杂度，有些东西本可以合并在一起，考虑到代码效率和正确性的风险，采用原来的功能用原来的代码，新功能用新代码，两者互不相关，可以最大程度确保新加的代码不会影响上次指令的正确性，缺点也很明显，冗余，复杂。　　

  • 第三次作业

    第三次作业对架构能力考验更大，对全局设计的能力有着更强的要求。不幸的是，我仍然采用了上述的设计模式，不改源代码，在基础上不断增加，致使代码超过1000行...

    第三次作业主要是研究四个权值不一样的最短路径的问题，当然还有一个连通块问题。

    其中四个最短路径可以采用统一的一个dijkstra进行模拟，事实上我只在三个最短路径采用dijkstra，最简单的最短路径仍采用bfs，原因仍是不改代码。那么由于增加了换乘需求，因此考虑何处换乘，成为了一个困扰自己的最重要的问题。此站是否需要换乘？在困扰一天之后，我开始动笔进行书写，我考虑的是尽可能不换乘，从而用dijkstra不断扩展，最后我发现，它本质上并不是局部最优就是全局最优，尤其是在一个节点在多条线的时候，很难描述清楚这种杂糅的状态，因此不得不，也一定要进行拆点的处理。

    与讨论区的大神不同的是，我的拆点是将一个点，如果被多个path所引用，则其拆分成多个Node，每个Node有一个pathid和nodeid，这样一个成为多个，每个nodeid相同的点之间是一个完全图。而在其外部，则很清晰的构建出一个邻接矩阵。比如1号线和2号线都有1节点，而1号线的1节点与2节点邻接，则在邻接矩阵中是1号线的1节点与1号线的2节点邻接，去其他线路的都没有任何关系。这样各条path是独立的，其产生的联系必须通过换乘，且是在同一个nodeid，不用的pathid之间，这种内部完全图之间的换乘。

    通过这样拆分，可以将整个图构建成一个新图，这个图上，从fromnode出发，需要注意的是fromnode是一个int的变量，而新图的每个节点都是一个有着nodeid，和pathid的新的类。因此fromnode上可能是在多条线，或者说一个fromnode可以对应多个node，这种关系可以用hashmap进行表达。而在遍历时候，我们是随机选择的一个Node进行出发的，这是否意味着需要将fromnode对应的所有Node都遍历呢？事实上并不需要。我们只用在出发的时候将每个nodeid为fromnode的点加入到最终集合，并权值标定为0 ，这时候，从哪个地方出发还重要吗？已经不再重要了。

    由此可以通过一次dijkstra，得到单源的所有最短路径，对其传入不同的参数，可以得到不同的结果，不满意度，票价等等，都可以被解决。

    不幸的是，这样的设计写出了很多bug，稍后会进行分析。

    对于连通块，设想的是构造一个node集合的副本，既然最短路径用的是bfs，不妨就让其bfs到结束，并删除这个副本的元素，直到这个副本的size为0，也就是所有的都被遍历了，否则可以对连通块个数加1。

    然而不幸的是，又出现了bug。

    由于图太大，难以放下，故不在此放第三次作业的类图了。　　

bug相关

在前两次作业中，由于课后进行了多次对拍，未发现bug。复杂度控制也比较好，超时情况也未出现。

在第三次作业，分别出现了一个bug和tle的情况。由于第三次作业的时间线把握不准，直到周二下午才将整体写完，通过中测，并开始对拍。期间发现几个bug进行了修改，但最后还是遗留下来了bug。

bug主要出现在对连通块的处理上，我的处理采用的是删除式的处理，而当size不为0，就添加1。这个步骤是在isconnect函数作业，起初想的是毕竟遍历完了，不为0，这时候的起点应该不会是原来的起点，这的确如此，因为原来的从那个起点出发的所有邻接点都已经被缓存下来，而我将其引申为应该不是原来被删除集合中的点了。这样便出现了问题，如果有两条毫不相干的路径，在第一条路径随便两个点isconnect后，第一条路径在集合中都被移除，这时候size不为0。如果换一个起点，还是第一条路径，此时未被缓存，将再次给连通块加1，而此时它根本不在目前的集合中，因此产生了bug。其修改是判断size不为0，同时，fromnode还需要在当前的还没删除的集合中，否则就不加1。

很明显这是由于我没有很好的控制好思维，产生了部分偏差，而在强测中，由于运气好，只有一个点涉及到了这种情形，但在互测中却被hack20次之多。后来我仔细的想了想为什么对拍没发现，强测也只出现一个bug。事实上这个bug是很严重的，其主要原因在于往往我们add的时候，都是连通的，很少有不连通的，每次isconnect，集合的size便为0，故不会多次添加，这是由于数据的针对性导致的。只要数据有针对性一些，立刻会被发现。

说完了wa，下面聊聊tle。

在我的架构里，tle的出现来源于很多情况，我的拆点复杂，且需要在终止点的时候进行一下遍历，然后每次换乘也需要遍历当前的nodeid对应的所有节点的最小的那个，这很费时间。因此在互测中会超时，而解决方案是采用优先级队列，可以降低一些时间，但仍不能降低到与大神们一样的地步。

在修复bug阶段，我很轻易的修复了wa的bug和tle的部分bug，但对于完全随机的疯狂的最短路径探索，我仍然会超时，因此最后还有一个bug未能修复，修复这个bug则需要更改自己的架构，且大改，权衡后故放弃。

心得体会

OO作业已经做了十二次了，其中有9次代码训练，三次博客作业，马上就要接近尾声，我的代码也逐渐从bug很多，到目前bug没那么多了。写出高质量的代码，一直以来是我们的追求，当然我知道，我离那里还有很远很远，但不论怎么说，进步总是有的，我总能看见他。求导的三次作业，一次未进互测，一次C组。电梯作业，一次A组，两次B组，没有任何正确性问题。规格单元，两次A组，一次B组，有一个正确性问题。逐渐的，我的平均水平在提高，希望在未来，的最后一个单元，可以完好的结局，虽然是一个不好的开头，但我仍期待有一个好的结尾。

转载于:https://www.cnblogs.com/whyme972056672/p/10898515.html

OO第三单元总结性博客相关推荐

  1. BUAA_OO第三单元总结性博客作业——JML

    一.JML 在第三单元的面向对象课程中我们第一次接触了JML语言以及基于JML规范的规格化设计.在之前一系列关于面向对象思想的学习认识中,我们知道了Java是一种面向对象的语言,面向对象思想的一个重要 ...

  2. BUAA_OO第一单元总结性博客作业——表达式求导

    一.程序设计思路 在我的三次作业中都采用了类的分层结构,采用逐项匹配,分层求导的思路. (一). 第一次作业中构建了Polynimial(多项式)类,在类的构造器中就完成了对非法空格的判断并对合法表达 ...

  3. OO第三单元JML规格总结分析

    OO 第三单元博客作业 1. JML语言概述 1.1 理论基础 综述 Java建模语言(Java Modeling Language,JML)是一种进行详细设计的符号语言,使人们用一种全新的方式来看待 ...

  4. 第三百篇博客：写给自己的总结

    文章目录 返航 我的中考和高考 初入大学的迷茫与思考 人生第一个Hello World! 第一次尝试找实习 加入工作室 对技术的反思 第一次做外包项目 脱单纪念日 准备春招 人生第一个Offer 惨败 ...

  5. OO第三单元——规格化设计与地铁系统——总结

    OO第三单元--JML的使用与地铁系统 梳理JML语言的理论基础.应用工具链情况 JML The Java Modeling Language (JML) is a specification lan ...

  6. OO第三单元单元总结

    OO第三单元单元总结 测试过程 黑箱操作和白箱操作 黑箱操作我认为就是通过随机构造合法数据对代码进行测试,在测试过程中应当着重对边界条件.前置条件.结果正确性等方面进行判断.不需要具体到代码的逻辑,通 ...

  7. 三步完成博客打赏功能

    打赏功能简单概括一下就是别人进入你的博客园,能看到打赏,打赏可以通过支付宝和微信的方式来向你支付打赏金额,之前看到博客上许多人发这个功能,我就总结了一下,尽量用最简单的方式来让别人看懂,然后加以运用 ...

  8. 三十天博客计划之《引言》

    大学的时候开始维护一个博客:DarkScope从这里开始,断断续续几十篇文章,也累积了一些访问量.不过最近的一篇已经是17年12月了,没有继续下去的原因很多,但归根结底是没有找到一个可持续发展的方式去 ...

  9. BUAA OO 第三单元 规格化设计

    黑箱测试 黑箱测试将被测软件看做一个打不开的黑盒,主要根据功能需求设计测试用例进行测试. 可以检测软件功能能否按照需求规格说明书的规定正常工作,是否有功能遗漏,行为.性能是否满足要求等. (个人感觉像 ...

最新文章

  1. 如何优雅的设计 Java 异常
  2. Swagger的简单入门【转载】
  3. javaWeb服务详解【客户端调用】（含源代码，测试通过，注释） ——applicationContext.xml
  4. 在c语言中优先级最低的是6,C语言中 *，＜＜，= ，-＞哪个优先级最低
  5. 学计算机的让修电脑搞笑段子精选,搞笑段子：阿姨，我是真的就来给他们修电脑的！...
  6. BBC：大数据带来的弊病？近因效应
  7. Mars 算法实践——人脸识别 1
  8. lua mysql 存储类型_Lua学习----Lua基础数据类型
  9. Unity音频可视化插件
  10. win10计算机丢失msvcr,Win10系统打开软件提示丢失msvcr110.dll如何解决
  11. 中小型企业无线网络设计
  12. 教你看懂MOSFET数据手册
  13. 一致性算法 - Distro协议在Nacos的实践
  14. 计算机网络和internet选项,小编教你电脑ie的internet选项在哪
  15. 轻松输入并注音生僻字
  16. eNSP-配置单臂路由与静态路由实验
  17. c语言数组相同字符主元素,C语言数组考点归纳
  18. 清华大学出版社大数据可视化技术与应用第六章Tableau实训
  19. 区块链安全初探（二）：区块链的层次
  20. 【译】什么是响应式编程

热门文章

  1. 见过最好的《禁闭岛》影评和解析
  2. QWebEngine
  3. 全球各国家.NET域名注册总量统计：中国排名第三
  4. EXCEL中删除多余的sheet 和 杀死Excel的进程
  5. kill excel病毒的查杀
  6. [随缘一题]-LintCode-有效三角形
  7. Ubuntu使用技巧：WinQQ自动隐藏解决
  8. jmeter导出jtl文件和report文件夹
  9. influxdb 插入数据_Influxdb 数据写入流程
  10. python正则group()与groups()用法