BUAA_OO_博客做业3——规格

时间  2020-05-05
标签 buaa 博客 规格 繁體版
原文   原文链接

BUAA_OO_博客做业3——规格

 

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

JML是java modeling language的缩写，是一种描述性质的语言。有必定的语法规则。java

这种语言被用来描述一段代码的具体行为，好比前置条件、反作用、后置条件等。node

JML的语法能够用专门的工具来检测是否合乎规范。算法

应用工具链

OpenJML数组

官网：http://www.openjml.org/downloads/数据结构

JMLUnitNG架构

官网：http://insttech.secretninjaformalmethods.org/software/jmlunitng/dom

jar连接：http://insttech.secretninjaformalmethods.org/software/jmlunitng/assets/jmlunitng.jaride

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

未解决：工具

C:\Users\LiTianYu>java -jar E:\tmp\JMLUnitNG.jar E:\tmp\MyPath1.java
JMLUnitNG exited because of an irrecoverable error:
org.jmlspecs.jmlunitng.JMLUnitNGError: Encountered 5 compilation errors:
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/ArrayList.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/AbstractList.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/AbstractCollection.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Object.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/Collection.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Iterable.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/List.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/AbstractList$ListItr.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/AbstractList$Itr.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/RandomAccess.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Cloneable.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/io/Serializable.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/ArrayList$ArrayListSpliterator.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/ArrayList$SubList.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/ArrayList$ListItr.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/ArrayList$Itr.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/Iterator.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Integer.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Number.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Comparable.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Integer$IntegerCache.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
E:\tmp\MyPath1.java:5: 错误: 已在类 MyPath1中定义了变量 nodes
        //@ public instance model non_null int[] nodes;
                                                 ^
E:\tmp\MyPath1.java:5: 错误: The field nodes in the specification matches a Java field MyPath1.nodes with different modifiers: public private
        //@ public instance model non_null int[] nodes;
                                                 ^
E:\tmp\MyPath1.java:5: 错误: The field nodes in the specification matches a Java field MyPath1.nodes but they have different types: int[] vs. ArrayList<Integer>
        //@ public instance model non_null int[] nodes;
                                              ^
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/ArrayList.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()': 找不到jdk.Profile+Annotation的类文件
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/AbstractList.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/AbstractCollection.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Object.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/Collection.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Iterable.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/List.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/RandomAccess.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Cloneable.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/io/Serializable.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/Iterator.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Integer.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Number.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Comparable.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
警告: E:\tmp\jmlruntime.jar(org/jmlspecs/annotation/Instance.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Annotation.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: E:\tmp\jmlruntime.jar(org/jmlspecs/annotation/Model.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: E:\tmp\jmlruntime.jar(org/jmlspecs/annotation/NonNull.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Retention.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/RetentionPolicy.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Annotation.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Target.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/ElementType.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Retention.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/RetentionPolicy.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Target.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/ElementType.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/AutoCloseable.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/AutoCloseable.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Byte.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Byte.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Character.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Character.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Short.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Short.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'
E:\tmp\MyPath1.java:74: 错误: An identifier with private visibility may not be used in a ensures clause with public visibility
      @ ensures \result == nodes[index];
                           ^
E:\tmp\MyPath1.java:74: 错误: 须要数组, 但找到ArrayList<Integer>
      @ ensures \result == nodes[index];
                                ^
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/RuntimeException.class): 主版本 52 比 51 新, 此编译器支持最新的主版本。
  建议升级此编译器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/RuntimeException.class): 警告: 没法找到类型 'Profile+Annotation' 的注释方法 'value()'

        at org.jmlspecs.jmlunitng.JMLUnitNG.processAllCompilationUnits(JMLUnitNG.java:527)
        at org.jmlspecs.jmlunitng.JMLUnitNG.run(JMLUnitNG.java:414)
        at org.jmlspecs.jmlunitng.JMLUnitNG.main(JMLUnitNG.java:177)

 规格中//@ public instance model non_null int[] nodes;实际实现为ArrayList学习

报错须要数组，不太明白应当怎么解决

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

这三次做业主要构建了路径，路径容器、图、地铁图；

个人设计中都使用了Java原有的一些容器（包括ArrayList和HashMap）；

因为第一次做业在时间上爆炸了，因此我后两次的做业使用了冗余数据和更好的数据结构来方便访问、查询等；

整体架构上，Path的变更不大，由于Path在第一次做业写得时候就已经写成比较优秀的状态了，因此后续不太须要变更。

变更主要体如今三次依次加深的部分。因为三次逐渐增长了功能，致使原有数据结构使用不便，因此后来进行了数据结构方面的重构。

在后两次次做业中，我使用了顶点集、边集来模拟无向图、地铁图。其中查询功能分散到顶点集、边集或者路径的数据结构中。

顶点集主要负责查询点的存在性、数量等；路径的数据结构负责根据id查路径或者根据路径查id；边集负责其余复杂的计算（如最短路等）。

须要提到的是，在计算最短路、连通块数时，边集须要使用到顶点集，这也是我设计中的一个缺陷。我不得不把顶点集做为参数传给边集。

具体的算法实现主要是采用了BFS、迪杰斯特拉和并查集。

第一次做业类图：

 

第二次做业类图：

 

第三次做业类图：

 三次做业复杂程度逐渐增长；其中能够看出第二次和第三次的设计存在一些缺陷（如边集和点集应当封装到一个图类里等）

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

实际上第一次和第二次都没有逻辑上的bug，第一次在强测时候的时间复杂度上被卡了25分；

第二次就使用HashMap代替了原用的ArrayList而且有多个冗余的HashMap来方便根据不一样的Key查询不一样的Value；

值得一提的是，我在写完第二次做业以后得意忘形，忘记修复第一次做业的bug了（划掉）

第三次做业真真正正出现了所谓的逻辑上的bug。这个bug出现的实际缘由是由于我使用了PriorityQueue，优先队列。

然而我并无搞懂它自动维护顺序的机制，误觉得一旦修改容器内的对象，容器也会自动维护。

如今想一想这个想法也太搞笑了。实际修复花费的时间主要在思考bug出现的缘由上。发现这个缘由以后，仅仅添加6行就完成了修复。

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

我认为规格的撰写是为了较大型的软件开发或者团队开发而诞生的。

在整体上，有一个总的规划，先确保总的逻辑正确性，再分别实现小的部分，这很OO。

也就是说，每一个对象（或者方法），都假设别人完成了别人的工做，而后本身也确保本身完成本身应有的工做，那么整个系统就能协调地运行了。

我的理解，规格的给出就相似于架构师，而具体实现则是“码农”的工做。架构师负责整体架构设计，码农负责细节处理。各司其职，各背其锅。

须要注意的是，规格中常常有对于数据结构的一个临时性描述，而实际上并非必须使用这种数据结构。

这样设计一个描述性的数据结构只是为了JML描述方便而已，实际实现应当考虑需求而设计合适的实现方法。（好比考虑响应时间或者内存占用等）

撰写一个大项目的JML并非一个容易的事情，是须要锻炼的。所以咱们也不能止步于当前的这一点点学习，更应该向长远将来看去，锻炼本身升华本身。

相关文章
相关标签/搜索
每日一句
    每一个你不满意的现在，都有一个你没有努力的曾经。
本站公众号
   欢迎关注本站公众号,获取更多信息
联系我们 最近搜索 最新文章 沪ICP备13005482号-10 MyBatis教程 SQL 教程 MySQL教程 Java 教程 Thymeleaf 教程 Hibernate教程 Spring教程 Redis教程