JML规格编程——BUAA OO第三单元做业总结

时间  2019-12-18
标签 jml 规格 编程 buaa 第三 单元 总结 繁體版
原文   原文链接

总体概述

这个单元总体围绕Java Model Language(JML)展开，经过学习JML规格了解契约式编程的过程，课上实验中进行了JML规格的简要编写，课下实验主要经过阅读规格并按照规格的要求正确编写程序实现相应的接口。java

JML入门

JML做为一种建模语言，主要的功能就是经过逻辑推演的方式对程序的表现进行限制，使用JML建模的程序实现起来只要知足JML的表达式就能够认为程序知足的需求。所以，从设计层面看，这既是对天然语言的一种转换也是从天然语言需求到计算机代码之间的桥梁，可以帮助使用者更好地对需求进行定义。同时，经过使用SMT solver以及junitNG等工具还能够很好地验证程序的正确性，甚至自动生成测试样例进行机动化测试。node

  1. JML语言基础linux

    本单元中咱们使用到的JML语言成分主要有：git

    关键字 说明
    normal_behavior 正常表现
    requires 前置条件
    ensures 后置条件
    invariant 类不变式
    assignable 约束后置条件中哪些变量可变
    exceptional_behavior 异常表现
    signals 异常描述

    使用以上语言成分就能够对Java程序中常见的程序表现进行建模，规定某个类、函数的使用条件和不一样输入状况下的表现。此外，在JML中能够用来表达的逻辑关系有：程序员

    关键字 说明
    && 逻辑与
    || 逻辑或
    ! 逻辑非
    == 相等关系
    ==> 逻辑蕴含
    <==> 逻辑等价
    \forall 全称量词
    \exists 存在量词

    使用以上的逻辑关键词就能够准确且无二义性的表示程序须要完成的需求表现，严格规定程序的责任关系。同时，JML还提供了\old表示同一变量修改以前的值，\result表示函数的返回值等进行建模。github

  2. 规格描述

    • 类的数据规格算法

      类的数据规格主要经过不变式invatiant和constraint进行约束，表示一个类在建立时应有怎样的数据表现，以及进行相应的修改操做时应该知足怎样的条件。针对层次关系则须要知足：
      • 子类继承父类的规则，子类能够重写父类的方法规格
      • 子类不能违反父类的规则，具体表现为：前置条件只能减弱，后置条件只能增强。

    • 方法的规格描述编程

      JML的建模主要集中在对类方法的行为约束上，而JML的约束又主要体如今数据约束上，即：经过指明数据须要知足的逻辑条件来规范程序的表现。建模时须要考虑的过程有：
      • 参数与输入状态：即调用函数以前须要知足requires前置条件的约束
      • 输出与返回的表现：即返回以前应该使得数据知足ensures后置条件以及类不变式的要求
      • 异常行为：异常行为经过exceptional_behavior指定
      • 是否修改类的相关数据：方法是pure的查询方法，仍是包含assignable能够修改类中的相关数据的？

    经过以上的过程就能实现使用JML的严格建模。windows

JML相关工具的使用

SML Solver

SML Solver是一个通用的自动化求解技术，能够用来证实程序的等价，从而直接从逻辑上验证程序的正肯定，避免了繁琐的测试过程。实践中，我使用了Z3 Theorem Prover与OpenJML结合的方式进行验证。bash

命令行使用

在下载完两项工具以后，为了使OpenJML调用到正确的Z3，须要修改openjml.properties文件：

openjml.defaultProver=z3_4_3
openjml.prover.z3_4_3=D:\\Document\\ProgramHome\\z3-4.3.2-x64-win\\bin\\z3.exe

为了不每次启动都要切换目录并写jar路径，能够创建脚本运行（linux平台方式不少，这里只记录下我在windows下的实践）:

@REM openjml.cmd
@"C:\Program Files (x86)\Common Files\Oracle\Java\javapath\java.exe" -jar D:\Document\ProgramHome\openjml-0.8.42-20190401\openjml.jar -properties D:\Document\ProgramHome\openjml-0.8.42-20190401\openjml.properties %*

将以上代码保存为openjml.cmd并放在任意一个Path中的路径便可被命令行检索到并能够直接使用。经过：

openjml -check -cp JarLib SourceFile.java

能够实现针对JML语言的语法检查

openjml -esc -cp JarLib SourceFile.java
openjml -esc -cp JarLib SourceFile.java -nowarn

能够实现代码的静态检查，给出程序中可能出现的潜在问题，使用-nowarn能够消除不关心的warning输出

配合Eclipse使用

OpenJML的命令行使用方式输出确实不太友好，所以我还尝试了在Eclipse下安装相应的插件进行检查，安装过程很简单，经过http://jmlspecs.sourceforge.net/openjml-updatesite便可安装jml插件，而后在Window->Preferences下对SMT Solver的位置进行一下简单设置：

jmlspec preferences

就能够正常使用了，使用时首先选择一个文件，而后在JML->TypeCheck JML能够检查JML的正确性，JML->Static Check (ESC)能够进行代码的静态检查，JML->*RAC*相关操做能够生成运行时检查须要的class文件。我使用这个工具对MyPath.java进行检查的结果为：

MyPath_esc

compareTo方法出现INVALID彷佛是由于输入为null时出现了错误，可是这个在compareTo的前置条件中已经排除了null的状况，equals方法彷佛也是由于类型问题被断定为了INVALID；MyPath构造函数中，JML要求实现的能够被断定为VALID，被断定为INVALID的是我额外实现了另外一种构造方式；getUnpleasantValue函数出现了ERROR：

Error occurred while checking method: homework.flymin.MyPath.getUnpleasantValue(int)
错误: ESC could not be attempted because of a failure in typechecking or AST transformation: getUnpleasantValue

我经过查阅资料，并无发现这个error的有效解决办法，同时我也检查了typechecking过程是没有问题的，所以问题应该就是出如今AST transformation中，目前我还没太搞明白。

JMLUnitNG

JMLUnitNG是openjml结合Junit的产物，能够针对给定的代码自动生成须要的测试代码，运行单元测试。但我从网上搜索到的JMLUnitNG相关的资料很是少，所以这部分不少操做尚未太明白，主要操做流程为：

  1. 首先准备待测代码

    testng/
├── IntPair.java
├── MyContainer.java
├── MyGraph.java
├── MyPath.java
├── MyPathExtend.java
├── MyRailwaySystem.java
├── Node.java
├── NodeSet.java
└── TicketNode.java

  2. 使用openjml生成动态测试文件(rac)备用：

    cp -r testng testng-o
java -jar ../openjml-0.8.42-20190401/openjml.jar -rac -cp ../specs-homework-3-1.3-raw-jar-with-dependencies.jar testng-o/*.java

  3. 针对待测代码生成测试代码的java文件，命令为：

    java -jar ../JMLUnitNG.jar -cp ../specs-homework-3-1.3-raw-jar-with-dependencies.jar testng/*.java

    执行以后目录结构为：

    testng
├── IntPair.java
├── MyContainer.java
├── MyContainer_InstanceStrategy.java
├── MyContainer_JML_Test.java
├── MyGraph.java
├── MyGraph_InstanceStrategy.java
├── MyGraph_JML_Data
│   ├── ClassStrategy_com_oocourse_specs3_models_Path.java
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_int1DArray.java
│   ├── ClassStrategy_int2DArray.java
│   ├── addPath__Path_path__27__path.java
│   ├── containsEdge__int_fromNodeId__int_toNodeId__0__fromNodeId.java
│   ├── containsEdge__int_fromNodeId__int_toNodeId__0__toNodeId.java
│   ├── containsNode__int_nodeId__0__nodeId.java
│   ├── floidPath__int_size__int2DArray_distance__0__distance.java
│   ├── floidPath__int_size__int2DArray_distance__0__size.java
│   ├── getShortestPathLength__int_fromNodeId__int_toNodeId__0__fromNodeId.java
│   ├── getShortestPathLength__int_fromNodeId__int_toNodeId__0__toNodeId.java
│   ├── isConnected__int_fromNodeId__int_toNodeId__0__fromNodeId.java
│   ├── isConnected__int_fromNodeId__int_toNodeId__0__toNodeId.java
│   ├── removePathById__int_pathId__0__pathId.java
│   └── removePath__Path_path__27__path.java
├── MyGraph_JML_Test.java
├── MyPath.java
├── MyPathExtend.java
├── MyPath_InstanceStrategy.java
├── MyPath_JML_Data
│   ├── ClassStrategy_com_oocourse_specs3_models_Path.java
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_int1DArray.java
│   ├── ClassStrategy_java_lang_Object.java
│   ├── MyPath__Path_path__27__path.java
│   ├── MyPath__int1DArray_nodeList__0__nodeList.java
│   ├── compareTo__Path_another__27__another.java
│   ├── containsNode__int_nodeId__0__nodeId.java
│   ├── equals__Object_obj__10__obj.java
│   ├── getNode__int_index__0__index.java
│   └── getUnpleasantValue__int_nodeId__0__nodeId.java
├── MyPath_JML_Test.java
├── MyRailwaySystem.java
├── MyRailwaySystem_InstanceStrategy.java
├── MyRailwaySystem_JML_Data
│   ├── ClassStrategy_com_oocourse_specs3_models_Path.java
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_testng_TicketNode.java
│   ├── addPath__Path_path__27__path.java
│   ├── getLeastTicketPrice__int_fromNodeId__int_toNodeId__0__fromNodeId.java
│   ├── getLeastTicketPrice__int_fromNodeId__int_toNodeId__0__toNodeId.java
│   ├── getLeastTransferCount__int_fromNodeId__int_toNodeId__0__fromNodeId.java
│   ├── getLeastTransferCount__int_fromNodeId__int_toNodeId__0__toNodeId.java
│   ├── getLeastUnpleasantValue__int_fromNodeId__int_toNodeId__0__fromNodeId.java
│   ├── getLeastUnpleasantValue__int_fromNodeId__int_toNodeId__0__toNodeId.java
│   ├── getUnpleasantValue__Path_path__int_fromIndex__int_toIndex__27__fromIndex.java
│   ├── getUnpleasantValue__Path_path__int_fromIndex__int_toIndex__27__path.java
│   ├── getUnpleasantValue__Path_path__int_fromIndex__int_toIndex__27__toIndex.java
│   ├── removeNode__TicketNode_node__7__node.java
│   ├── removePathById__int_pathId__0__pathId.java
│   └── removePath__Path_path__27__path.java
├── MyRailwaySystem_JML_Test.java
├── Node.java
├── NodeSet.java
├── NodeSet_InstanceStrategy.java
├── NodeSet_JML_Data
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_testng_Node.java
│   ├── getNode__int_nodeId__0__nodeId.java
│   ├── putNode__int_nodeId__0__nodeId.java
│   └── safeRemoveNode__Node_node__7__node.java
├── NodeSet_JML_Test.java
├── Node_InstanceStrategy.java
├── Node_JML_Data
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_java_lang_Object.java
│   ├── ClassStrategy_testng_Node.java
│   ├── ClassStrategy_testng_Node1DArray.java
│   ├── Node__int_id__0__id.java
│   ├── addNeighbor__Node_node__7__node.java
│   ├── addreachable__Node_node__int_len__7__len.java
│   ├── addreachable__Node_node__int_len__7__node.java
│   ├── equals__Object_obj__10__obj.java
│   ├── getShortestPathLen__Node_another__7__another.java
│   ├── isNeighbor__Node_another__7__another.java
│   ├── reachable__Node_another__7__another.java
│   └── removeNeighbor__Node1DArray_nodes__7__nodes.java
├── Node_JML_Test.java
├── PackageStrategy_com_oocourse_specs3_models_Path.java
├── PackageStrategy_int.java
├── PackageStrategy_int1DArray.java
├── PackageStrategy_int2DArray.java
├── PackageStrategy_java_lang_Object.java
├── PackageStrategy_testng_Node.java
├── PackageStrategy_testng_Node1DArray.java
├── PackageStrategy_testng_TicketNode.java
└── TicketNode.java
    即针对每个方法都生成了相应的测试代码和数据文件

  4. 而后编译上述文件，并替换待测代码对应的class为openjml rac编译的class

    javac -cp ../JMLUnitNG.jar:../specs-homework-3-1.3-raw-jar-with-dependencies.jar testng/*.java testng/*/*.java
cp testng-o/*.class testng

  5. 运行测试（这里运行了较为简单的MyPath）

    gaoruiyuan@THINK-X1E:/mnt/d/Document/ProgramHome/Java$ java -cp ./:../JMLUnitNG.jar:../specs-homework-3-1.3-raw-jar-with-dependencies.jar testng.MyPath_JML_Test
[Parser] Running:
Command line suite

Passed: racEnabled()
Passed: constructor MyPath(null)
Passed: constructor MyPath(null)
Passed: constructor MyPath({})
Failed: <<testng.MyPath@2f333739>>.compareTo(null)
Passed: <<testng.MyPath@4cc77c2e>>.containsNode(-2147483648)
Passed: <<testng.MyPath@7a7b0070>>.containsNode(0)
Passed: <<testng.MyPath@71bc1ae4>>.containsNode(2147483647)
Passed: <<testng.MyPath@2437c6dc>>.equals(null)
Passed: <<testng.MyPath@299a06ac>>.equals(java.lang.Object@383534aa)
Passed: <<testng.MyPath@6bc168e5>>.getDistinctNodeCount()
Failed: <<testng.MyPath@7b3300e5>>.getNode(-2147483648)
Failed: <<testng.MyPath@2e5c649>>.getNode(0)
Failed: <<testng.MyPath@136432db>>.getNode(2147483647)
Passed: <<testng.MyPath@3caeaf62>>.getUnpleasantValue(-2147483648)
Passed: <<testng.MyPath@e6ea0c6>>.getUnpleasantValue(0)
Passed: <<testng.MyPath@6a38e57f>>.getUnpleasantValue(2147483647)
Passed: <<testng.MyPath@5577140b>>.isValid()
Passed: <<testng.MyPath@1c6b6478>>.iterator()
Passed: <<testng.MyPath@67f89fa3>>.size()

===============================================
Command line suite
Total tests run: 20, Failures: 4, Skips: 0
===============================================

能够看到出现了几处Failed，对于compareTo方法，测试中仍旧是在传入null时出现了错误，返回测试代码进行了相应的修改，getNode方法须要实例知足某个状态才能正确表现，这里暂时跳过了这个方法；compareTo方法及其检测方法中加上了对null的响应操做，以后再次运行测试：

gaoruiyuan@THINK-X1E:/mnt/d/Document/ProgramHome/Java$ java -cp ./:../JMLUnitNG.jar:../specs-homework-3-1.3-raw-jar-with-dependencies.jar testng.MyPath_JML_Test
[Parser] Running:
  Command line suite

Passed: racEnabled()
Passed: constructor MyPath(null)
Passed: constructor MyPath(null)
Passed: constructor MyPath({})
Passed: <<testng.MyPath@2f333739>>.compareTo(null)
Passed: <<testng.MyPath@4cc77c2e>>.containsNode(-2147483648)
Passed: <<testng.MyPath@7a7b0070>>.containsNode(0)
Passed: <<testng.MyPath@71bc1ae4>>.containsNode(2147483647)
Passed: <<testng.MyPath@2437c6dc>>.equals(null)
Passed: <<testng.MyPath@299a06ac>>.equals(java.lang.Object@383534aa)
Passed: <<testng.MyPath@6bc168e5>>.getDistinctNodeCount()
Skipped: <<testng.MyPath@7b3300e5>>.getNode(-2147483648)
Skipped: <<testng.MyPath@2e5c649>>.getNode(0)
Skipped: <<testng.MyPath@136432db>>.getNode(2147483647)
Passed: <<testng.MyPath@3caeaf62>>.getUnpleasantValue(-2147483648)
Passed: <<testng.MyPath@e6ea0c6>>.getUnpleasantValue(0)
Passed: <<testng.MyPath@6a38e57f>>.getUnpleasantValue(2147483647)
Passed: <<testng.MyPath@5577140b>>.isValid()
Passed: <<testng.MyPath@1c6b6478>>.iterator()
Passed: <<testng.MyPath@67f89fa3>>.size()

===============================================
Command line suite
Total tests run: 20, Failures: 0, Skips: 3
===============================================

这个结果目前来看是比较和理想中相符的了。

架构设计与重构分析

继承式增量设计

由于这个单元的代码做业是给出JML的，咱们须要作的是给出相应的代码实现，因此能够理解为相应的总体架构在JML中已经肯定了，所以三次代码做业下来我并无作太多重构性的工做。其实官方仓库给出的规格也是继承式的，所以我也按照一致的思路，每次继承上一次的设计再在其基础上拓展功能实现新的接扩方法。因此，这个单元的做业在我看来一直是一种增量使得设计，只要保证方法的独立性，即方法、类实现之间没有相互依赖，就可以保证在需求增长时能够直接扩展而没必要要所有从新设计。这一点也可以经过类图来体现：

第一次

第一次做业不管从JML规格仍是实现方法来说我都没有作太复杂的操做，固然，想的太简单的也是要付出代价的。但从类图里面能够看出，Path和PathContainer之间是没有任何直接联系的，因此我保证了只要是按照JML实现的代码，对于个人实现方式来讲都是能够兼容替换的。

第二次

第二次做业针对PathContainer进行了扩展，创建了图结构，我就在完善第一次做业的代码的基础上，直接继承了MyPath造成了MyGraph，只是将相关的发放进行了重写，同时增长了新的方法，并无破坏原代码的结构。另外，这样作的好处就是我能够把和图运算相关的操做所有保留在MyGraph中，很天然的就能够和原来的运算分离开，没必要担忧这两部分相互之间出现问题。能够看出，在此次做业中，MyPath仍旧是独立的结构，这与其定义的初衷相吻合。实现中，我对于NodeSet使用了单例模式保证其成为一个全局可访问的节点集合，这样的分离设计也使得出错的可能性大为下降。

第三次

第三次做业个人思路仍然没有变，我依旧是扩展了第二次做业的类设计，在继承原来的类的基础上加上了新的功能。但此次为了实现getUnpleasantValue方法同时尽力保持MyPath类本来的独立性，我在继承这个类的基础上进行了扩展，实现了MyPahtExtend类，增长了一些创建局部图计算最短加权路径的算法，即便这样，MyPath类相对的独立性也没有受到影响。

算法与数据结构

数据结构上，我三次做业采用的都是邻接表的结构存储图节点，节点自己使用一个HashSet，但由于Set集合并不能随机读，所以后来我改为了HashMap，在保证没有重复的同时也可以堆积访问节点Id到节点对象的映射。对于可达节点我仿照邻居节点处理，也作成了一个Map，表示可达节点以及相应的最短路径。

值得一提的时，在第三次做业中我须要用到一个无序的Pair结构做为Map的Key，但Java好像并无提供这样的机制，所以我本身建立了一份IntPair类做为索引，由于无须，因此能够减小一半的冗余存储（对于无向图）。

算法方面，我一直采用了Floyid全局最短路的算法，第三单元中，我将重复节点拆开存储建图，而后继续使用全局最短路。这样的算法在图结构较小时效果不错，当图结构庞大并且点没法进行合并时复杂度会急剧上升。我在进行第三单元测试的时候忽视了这一点，知道DDL前一小时才发现，根据需求给出来的数据量，若是节点不进行合并数据规模很容易上千，而这样的数据量是根本没法再规定的时间内跑完$O(n^3)$的Floyid算法的，但已经来不及改了，所以第三次做业也出现了大量的超时。

bug与代码分析

bug分析

这三次做业下来我没有什么逻辑上的bug，出现的问题基本都是超时错误。第一次做业中我没有进行任何基本的优化，致使超时；做业二我吸收教训作了很多优化，所以获得了满分；但做业三我觉得做业二的算法依旧适用，所以没有更换算法，致使出现了更大面积的TLE。

代码分析

此次的度量分析我只针对第三次做业给出，由于每次都是在前一次的基础上进行扩展，因此最后一次做业实际上涵盖了全部三次的代码实现。

  • 代码量分析

code

从数据中能够看出，由于每次只须要作增量设计，因此类的长度仍是比较合理的。但即便是继承，也免不了须要重写方法，所以最长的MyRailwaySystem有334行代码，规模也算不小了。

  • 方法复杂度分析

    这单元做业的方法复杂度分析以下，存在两个复杂的条件判断，三个复杂的方法，这三个复杂的方法的循环复杂度均为9，是计算最短路径的三个主要方法，其余方法的复杂度都不高，循环复杂度（CC）平均值为2.067。方法的平均代码行数为8.78，能够说这个水平对于缩小函数长度来讲仍是比较理想的。

Type Name Method Name Code Smell
MyContainer getPathId Complex Conditional
MyGraph removePath Complex Conditional
MyGraph calShortestPathLength Complex Method
MyRailwaySystem calTicket Complex Method
MyRailwaySystem calChange Complex Method

  • 类复杂度分析

    总体来看经过集成实现的设计方法使得类之间的复杂性控制的仍是比较均衡的，最复杂的那几个类不出所料的集中在MyContainer、MyGraph和MyRailwayStation。部分图算法为了提升相同片断的复用性被放在了TicketNode类中，所以也让这个类显得有些复杂，但实际上并无太多本身的运算——这可能就是复杂点的工程设置util的重要性吧。

Type Name NOF(属性数量) NOM(方法数) NOPM(public方法数) LOC(行数) WMC(加权方法复杂度) LCOM(方法之间缺少聚协力的程度)
IntPair 2 3 2 33 6 0
Main 0 1 1 15 1 -1
MyContainer 3 13 13 50 15 0.462
MyGraph 2 13 10 216 35 0.692
MyPath 2 11 11 90 24 0.364
MyPathExtend 1 3 2 56 10 0.667
MyRailwaySystem 9 17 10 288 61 0.235
Node 3 14 14 107 23 0
NodeSet 2 8 8 64 12 0.25
TestMain 0 1 1 10 1 -1
TicketNode 6 21 19 141 29 0.143

单元感悟

经过这个单元的学习，我体会到了使用JML进行代码约束的方便，有了JML，实现与需求之间的交互变得明朗起来，并且困扰程序员好久的程序正确性证实也有了好的出口。更关键的是，JML的使用不只在工程师交付环节起到关键做用，在模式设计、合做任务分配时也会有十分重要的应用，遵照JML进行编程可以使得不一样来源的程序得到最好的兼容性，并且不须要阅读代码就能清楚的知道责任划分（如前置条件和后置条件），从而在一开始就避免可能出现的bug。我有一个很深的体会就只以前写代码时并无一个很强的总体感，基本是一边想一边写，这样虽然能很快动手，可是代码量一多就会发现随着相互的调用关系变得负责，函数之间的责任划分变得不那么明确，这时候为了保证正确性不得不作不少冗余的check工做，而使用JML正好能够避免这个问题，辅助咱们在一开始就作好设计并在设计完成后给出合理的验证。

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