OO第三单元JML总结

目录

目录一、JML语言的理论基础二、应用工具链三、部署SMT Solver四、部署JMLUnitNG/JMLUnit五、三次作业分析第一次作业第二次作业第三次作业六、总结与心得体会

一、JML语言的理论基础

　　JML（Java Modeling Language）是一种形式化的、面向Java的行为接口规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。BLSL提供了对方法和类型的规格定义手段。它允许在规格中混合使用Java语法成分和JML引入的语法成分。JML使用Javadoc的注释方式，通过一些符号描述方法的预期功能，而不管它如何实现。JML将过程性的思考延伸到方法设计中，从而扩展了面向对象设计的这个原则。

　　JML引入了大量描述行为的结构，如前置条件、后置条件、模型域、正常行为、异常行为等，这些结构使得JML非常强大。更多JML行为结构参考JML Level0手册。

　　下面列举常用JML语法。

• Precondition

  • /@ requires P; @/

• Postcondition

  • /@ ensures P; @/

• Side-Effects

  • /@ assignable list;@/

• Exception

  • /@ signal (Exception e) P;@/

• Invariant

  • /@ invariant P; @/

• Constraint

  • /@ constraint P; @/

• method result reference

  • esult

• Previous expression value

  • old(E)

• Using private fields in specifications

  • private /@ spec_public @/ Type property;

• Fields not null

  • Private /@ not_null @/ Type property;

• Declare spec variable

  • //@ public model Type x;

• Quantifiers

  • Iterating over all variables

    • (forall T x; R(x); P(x))

  • Verifying if exist variables

    • (exists T x; R(x); P(x))

  • Num of elements

    • ( um_of T x; R(x); P(x))

  • Sum of expression

    • (sum T x; R(x); E)

　　

二、应用工具链

• OpenJML使用SMT Solver规格验证

• JMLUnitNG生成TestNG测试用例进行测试

• ...

三、部署SMT Solver

　　本节openjml的学习参考了伦佬的贴子：OpenJML 基本使用，采用的SMT Solver为z4-4.7.1。

• 符合规格但代码中存在漏洞

  如下是一份符合规格但含有减法溢出的代码

  

  　　运行静态检查结果如下

  

  　　成功检测出了减法溢出错误

• 不符合规格的检测

  如下代码逻辑与规格不符

  

  　　检测结果如下

  

• 符合规格要求且无漏洞的检测

  

  　　检测结果如下（没有结果就是好的结果

  

四、部署JMLUnitNG/JMLUnit

　　本节参考了伦佬的贴子：使用 JMLUnitNG 生成 TestNG 测试样例

　　以第十次作业为例，采用maven文件结构。

• 初始文件目录树

• 使用jmlunitng生成测试文件

jmlunitng -cp specs-homework-2-1.2-raw-jar-with-dependencies.jar -d test/java/ main/java/*.java

　　生成测试文件后的文件目录树如下（由于生成的文件比较多，只展示部分）

• 在IDEA中创建TestNG运行配置并运行测试

　　测试结果如下（居然没有一个类完全pass。。。）。以及对于第一行的报错信息，参考伦佬的解释：“测试结果的第一行是 racEnabled 的测试，意在检测我们的主文件是否带有 JML 的运行时检查。”

• 部分测试结果分析

　　以下提取MyGraph的测试结果进行分析。

　　第一个被检测出的错误是addPath()方法传入空Path时的错误

　　本人的MyGraph.addPath()源代码如下

　　该方法调用了父类（本人的MyGraph类继承了第一次作业中的MyPathContainer类）的addPath方法，本以为考虑了path为null的情况，却忘记MyPathContainer.addPath()在path为null时返回的是0，而path为null并没有终止MyGraph.addPath()的行为，故有可能产生错误。

　　　之后还有一排齐刷刷的报错，但实际上不是getShortestPath()模块中的错误，而是由于按照JML要求抛出了相关异常被捕获报的错（isConnected()方法调用了getShortestPath()，有是否有最短路判断是否连通，故也有报错）。由于Jmlunitng产生的测试用例是单元测试用例，捕捉到异常会报错，而不经过课程提供的I/O接口，所以才会出现这些让人看了极度不适却又无可奈何的报错。

• 小结

　　Jmluning是个十分得力的助手，或许由于没有深入挖掘，看法可能还比较片面。

　　Jmlunitng生成的都是一些边缘数据，如int的边界值，null等，对于程序中一些微小的、无法察觉的bug爆破还是有十分可观的作用的。但对于复杂逻辑、模块间依赖的检测，也许就帮不上什么大忙，甚至是帮倒忙（比如上述getShortestPath()抓到本应该抛出的NodeIdNotFound异常，却直接给我Test failed了。。。也许之后随着使用的深入，能够发现它更多的优点，或者是成为改进它的一员。

五、三次作业分析

第一次作业

1. 架构设计

　　第一次作业较为简单，但由于没有充分考虑数据结构对时间复杂度的影响，因此在阴沟里翻了船。 　　第一次作业在MyPath类中用两个ArrayList分别存储路径中所有的结点和不同的结点，在MyPathContainer中采用双HashMap的形式存储路径Map与路径IdMap，并用一个distinctNodeNum域存储不同的结点数，在每次增删时更新（由于更新时采用ArrayList作为存储中间结果的数据结构，导致了TLE，详细分分析在下文叙述）。

2. 类图

3. 经典OO度量

	ev(G)	iv(G)	v(G)
Total	36	35	47

     其中MyPath.compareTo和MyPath.equals方法复杂度较高，原因是在其中使用了许多条件判断语句判断路径等价或大小，后两次作业由于保留了MyPath类，故也保留了这两个高复杂度的方法。

4. Bug修复

　　本次作业中强测CTLE了一半的数据，原因是MyPathContainer.countDistinctNodes()方法中使用了不合理的中间数据结构存储不同的结点。

　　在该方法中采用ArrayList来临时存储路径中不同的结点，遍历了MyPathContainer中所有的路径，并遍历路径中所有的结点，用ArrayList.contains()方法判断是否已有该点，没有则加入。而问题就出在contains()方法上，它需要遍历ArrayList中的所有元素。总共三层循环，导致了cpu时间的爆炸

　　改进方法是将存储中间结果的数据结构改为HashSet，它的contains()方法是O(1)的，且其实不需要调用contains()，HashSet.add()会排除重复元素，最终只需两层循环（遍历路径与遍历结点）即可完成distinctNode的计数。

第二次作业

1. 架构设计

　　第二次作业为了能够满足课程教学中类型层次迭代的设计，没有选择重构，而是在修复第一次作业的Bug的基础上采用继承的方式实现MyGraph。

　　在MyGraph类中配置了图计算类MyGraphCalc的对象进行相关图类运算，以及boolean型成员latest记录图计算对象中数据的更新状态。MyGraph中增删路径时对图计算类做相应的更新，获取图相关数据（最短路径、连通状态等）时，先判断数据是否是最新状态，若没有则更新图计算对象，后再从中获取数据。

　　MyGraphCalc图计算类采用HashMap<Integer, HashMap<Integer, Integer>>的双层HashMap形式存储图的邻接矩阵、最短路径矩阵，并配置更新、访问方法。考虑到图更新指令数远小于图访问指令数，最短路径的算法选择了Floyd，一劳永逸。

2. 类图

3. 经典OO度量

	ev(G)	iv(G)	v(G)
Total	60	63	86

4. Bug修复

　　强测中虽然有幸没有TLE，但有几组数据居然跑到了15s+的惊人CPU时间，得知HashMap的增删可能比较耗时，遂在MyGraphCalc中采用静态数组存储数据，并配置一个HashMap做下标转换，在Bug修复中预览测试后发现，那几组差点跑崩的数据的CPU时间都减少到了5s左右。

第三次作业

1. 架构设计

　　第三次作业依靠讨论区大神给出的不拆点的方法完成（贴子)，并使用了Maven创建项目。

　　文件目录树如下：

　　本次需实现的MyRailwaySystem仍采用继承的方式，在第二次作业的基础上继续填充。在MyRailwaySystem类中仍配置得力助手MyRailwayCalc负责地铁相关数据的存储与运算，他们的协同方式仍如第二次作业一样，MyRailwaySystem接受Path，并提交给MyRailwayCalc进行存储与运算，在申请数据时从MyRailwayCalc中获取。区别在于，本次作业将数据更新状态交由MyRailwayCalc维护，而MyRailwaySystem只行驶领导的职责，分配任务，而不必管工作进度。

　　由于本次作业有4种主要数据需要计算，即ConnectBlock, LeastTicketPrice, LeastTransfer, LeastUnpleasant，故将这4种数据抽象为类，并统一继承抽象类RailData。抽象类RailData制定了地铁数据的行为纲领：初始化与更新策略。

　　连通块数的运算采用路径压缩的并查集算法实现，三种最短路都采用Floyd最短路算法（Floyd作为静态方法封装在MyGraphCalc中），且都需要在路径内建图获取单条路径内的最短路。对于最少换乘，路径内建图只需将路径变为完全图；对于最少票数，路径内建图边权为最短路，故采用第二次作业已实现的MyGraphCalc进行路径内建图；对于最少不满意度，由于边权运算较复杂，故开了一个新类MyGraphCalcWithWeight继承MyGraphCalc，进行最少不满意度的路径内建图。三个最短路问题都采用静态数组存储数据，并统一使用MYGraphCalc中的下标转换方法进行转换。

2. 类图

• 总类图

• calculator包

• container包

• raildata包

3. 经典OO度量

	ev(G)	iv(G)	v(G)
Total	129	145	182

4. Bug修复

　　本次作业强测与互测均未被发现Bug。

　　本次尝试了Junit单元测试，在强测前达到了96%的代码覆盖率，剩余未覆盖代码为逻辑无法到达的地带，或是无需实现的方法。

六、总结与心得体会

　　本单元的三次作业都是在给定规格的基础上，实现代码的填充。总的来说，拥有JML所规约的框架之后，无论是设计的合理性还是正确性的保证，都不会有太大的偏差。

　　但是实现JML规格的过程中也面临了一个问题，也就是个人对方法功能的实现与规格规约之间的矛盾。规格采用某种数据结构来描述行为，但是个人实现方法时采用另一种实现功能的逻辑，虽然没有按照规格的逻辑，但完成了相同的功能，此时就无法按照规格的逻辑去检验正确性，使用外部工具（如openjml）也会疯狂报错，这也就失去了规格通过逻辑检验代码正确性的初衷。

　　其次，由于需要通过数理逻辑去描述一个模块的功能，在复杂程序设计的过程中，JML规格就变成了一种“加密“，设计者花费心力描述大段规格，实现者也要花费同等甚至更多的时间精力去”解密“这些规格，最后得出这个模块的功能，无疑增加了项目完成的时间成本。对于本人而言，第三次作业的四个大问题更多的是参照指导书给出的解释完成模块的功能，时间与个人能力不允许我去完整阅读所有规格代码之后再去动手实现。

　　以上的看法还是比较片面，仅是一个JML初学者的观点。也许在深入学习之后，会发现JML的更多不可思议的强大之处。