一.JML理论基础及应用工具链

1.理论基础

• 原子表达式
  • \result:表示一个非void的方法执行后的返回值。
  • \old(expr):表示一个表达式expr在执行相应方法前的取值
  • \not_assigned(x, y, ...):表示括号内的变量在方法执行过程中是否被赋值。没有被赋值则返回true；否则返回false
  • \not_modified(x, y, ...):类似not_assigned，区别是表示变量取值是否变化
  • \type(type):返回类型type对应的Class
• 量化表达式
  • \forall:全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应约束
  • \exists:存在量词修饰的表达式，表达对于给定范围内的元素，存在某个元素满足相应的约束
  • \sum:返回给定范围内的表达式的和
  • \max和min:分别返回给定范围内表达式的最大和最小值
• 方法规格
  • 前置条件：前置条件通过requires子句来表示：requires P，即要求确保条件P为真
  • 后置条件：后置条件通过ensures子句来表示：ensures P，即要求确保方法执行返回结果一定满足谓词P
  • 副作用限定：通过assignable和modifiable，分别表示可赋值、可修改
• 类型规格
  • 不变式invariant：是要求在所有可见状态下都必须满足的特性，invariant P
  • 状态变化约束constraint：对前序可见状态和当前可见状态的关系进行约束

 

2.工具链应用

1.OpenJML：可以检查JML文档规格语法，其中SMT Solver可以验证代码是否符合规格

2.JMLUnitNG：一款基于JML的单元测试工具，可以自动生成测试用例

3.Junit：用于进行单元测试，可编写和可重复运行的自动化测试。

二.JMLUNITNG

　　按照焦同学的博客，我输入了以下四条代码：

java -jar jmlunitng.jar jmlunit/MyGroup.java
javac -cp jmlunitng.jar jmlunit/*.java
java -jar openjml.jar -rac jmlunit/MyGroup.java
java -cp jmlunitng.jar jmlunit.MyGroup_JML_Test

 

　　得到的结果如下：

[TestNG] Running:
  Command line suite

Passed: racEnabled()
Passed: constructor MyGroup(-2147483648)
Passed: constructor MyGroup(0)
Passed: constructor MyGroup(2147483647)
Failed: <<MyGroup@4ebba42a>>.addPerson(null)
Failed: <<MyGroup@467eca23>>.addPerson(null)
Passed: <<MyGroup@66133adc>>.delPerson(null)
Failed: <<MyGroup@287534f5>>.delPerson(null)
Failed: <<MyGroup@ba4d4a7e>>.delPerson(null)
Passed:<<MyGroup@5c0e39b3>>.equals(null)
Passed:<<MyGroup@d793cb21>>.equals(null)
Passed:<<MyGroup@508a4bba>>.equals(null)
Passed: <<MyGroup@a2b1398c>>.equals(java.lang.Object@574caa3f)
Passed: <<MyGroup@63bcaa71>>.equals(java.lang.Object@64cee07)
Passed: <<MyGroup@2d7f89e3>>.equals(java.lang.Object@1761e840)
Passed: <<MyGroup@23fea612>>.getAgeMean()
Passed: <<MyGroup@b45e2fa7>>.getAgeMean()
Passed: <<MyGroup@685b3ad2>>.getAgeVar()
Passed: <<MyGroup@3536c874>>.getAgeVar()
Passed: <<MyGroup@c2f309a6>>.getAgeVar()
Passed: <<MyGroup@ab27c89c>>.getConflictSum()
Passed: <<MyGroup@1ef7015a>>.getConflictSum()
Passed: <<MyGroup@74b8b58f>>.getConflictSum()
Passed: <<MyGroup@1c56bc89>>.getId()
Passed: <<MyGroup@445a8ca1>>.getId()
Passed: <<MyGroup@38b6c32a>>.getId()
Passed: <<MyGroup@3ae8b12a>>.getRelationSum()
Passed: <<MyGroup@3e2851ac>>.getRelationSum()
Passed: <<MyGroup@a93c83c7>>.getValueSum()
Passed: <<MyGroup@721f0239>>.getValueSum()
Passed: <<MyGroup@6ab01c56>>.getValueSum()
Failed: <<MyGroup@1f6ff78c>>.hasPerson(null)
Failed: <<MyGroup@c81f7a90>>.hasPerson(null)
Failed: <<MyGroup@48e75ac0>>.hasPerson(null)
Passed: <<MyGroup@5e876f2a>>.updatePerson(null)
Passed: <<MyGroup@6f91e371>>.updatePerson(null)
Passed: <<MyGroup@b274b4d7>>.updatePerson(null)
Passed: <<MyGroup@13fa6a7b>>.downloadPerson(null)
Passed: <<MyGroup@49a3b226>>.downloadPerson(null)
Passed: <<MyGroup@6821a38b>>.downloadPerson(null)
Failed: <<MyGroup@21ab83e5>>.updateLink(null, null)
Failed: <<MyGroup@48e2ff12>>.updateLink(null, null)
Failed: <<MyGroup@67a8815e>>.updateLink(null, null)

===============================================
Command line suite
Total tests run: 43, Failures: 12, Skips: 0
===============================================

 

　　感觉jmlunitn*生的数据都非常极端，实用性很弱。而且不得不说，部署solver和jmlunitng非常麻烦而且容易出各种各样的玄学问题，总之，我觉得确实实用性不强。

三.作业的架构设计

1.第一次作业

 第一次作业比较简单，使用bfs防止爆栈即可。

2.第二次作业

 主要优化方向是使用缓存优化双层循环。

3.第三次作业

四.bug分析

1.第一次作业

　　第一次作业较为简单，在强测和互测中均未出现bug。

2.第二次作业

　　我在第二次作业的强测与互测中也并未出现任何bug。hack其他人的点都为超时bug，有的同学并未使用缓存机制来储存合适的状态值从而节省计算的时间，或许由于在强测中运气比较好进入了A屋，然后再互测中显然不可能幸免于难。因为二层循环的复杂度显然太高，如果想卡的话并不困难。

3.第三次作业

• 我在第三次作业的强测和互测中被卡了超时。由于我在课下使用了普通的Dijkstra算法，而没有使用缓存和堆优化来加速，所以确实复杂度比较高，很容易超时。我在强测中有5个点都超时了。
• 在互测中有人判断点双连通是通过枚举所有路径来完成的，而我构建出了一个路径数目非常多的图形，导致使用此方法的同学的时间复杂度会很高，很容易超时。

五.相关感想

 1.我个人觉得本单元的debug方法与前面两个单元确有很大不同。

主要的debug方法我觉得主要有以下几种：

• junit
• 找到一份大佬代码，随机生成测试数据，然后对拍
• 使用python专门的图论库networkx
• jmlunitng,solver等

　　几种方法中我觉得相对最不靠谱的是junit。junit虽然在迭代开发TDD时确实非常方便，但是junit的测试样例是我们自己编写的 ，据我所知，这个单元的很多bug都是因为没有看清规格导致的，而junit显然无法解决这样的问题。

　　和大佬代码对拍这个方法我个人比较推崇，首先我自己就是这么做的，其次确实非常有效，我帮别人和自己都发现了bug。最关键的是，本单元的对拍很好写，以为结果的判定是唯一的，不像电梯单元那样有很多个正确答案导致对拍写起来就会比较复杂。

　　networkx库这个方法我觉得也很不错，这个图论库不得不说非常强大，很多作业中最复杂的几个函数胡只用python 的一条语句就可以很好地检验了。

　　jmlunitng,solver等我觉得配置繁杂而且基本起不到debug的功效，很不推荐。

2.python库neyworkx

正如上文中所说，有一些很复杂的函数只需要一条语句就可以比较完美地检验，比如：

• 判断连通：nx.haspath()

•  

  最短路：nx.shortestpath() 

•  

   

  求割点：nx.articulation_points(G)

• 点双连通：nx.biconnected_components(G)

• 求出所有不连通子图：connected_components(G)。 

我觉得nerworkx与matlabplot混合使用非常好，比如强测或者互测中被hack的点的图形比较复杂，如果拿手画显然不太现实，这时可以综合应用这两个工具画出清晰美丽的图形，如下图所示：