JML单元总结

JML理论基础及应用工具链

理论基础

JML设计源自契约式设计的需要，我个人的理解是它是一种功能要求的表述，要求写程序的人按照这个要求去实现功能。

1.方法规格

• 前置条件：requires
• 后置条件：ensures
• 副作用：放在 assignable之后，表示需要被修改的对象属性及类静态变量
• pure方法：使用/*@pure@*/，表示该方法可以被其他方法的JML引用
• 正常行为：normal_behavior
• 异常行为： exceptional_behavior

2.数据规格

• 不变式：invariant :成员变量在处于可见状态下时必须满足的特性。
• 约束：constraint：某操作执行前与执行后该数据需要满足的关系

类中的数据在任意时刻都需要满足不变式与约束

3.类规格

在类中利用规格变量对类的数据结构进行抽象描述，与具体实现无关。同时回个支持类的层次化设计，子类可以对于父类的规格进行适当的扩充，但需要保证：

• 子类重写父类方法时不能与父类的方法时不能与父类的方法规格冲突
• 子类新增和拓展的数据规格不能与父类的数据规格相冲突

对于子类的重写方法，可以对父类的方法规格进行的改变有：

• 减弱父类方法规定的requires
• 加强父类方法规定的ensures

4. 相关语法

• \result方法的返回值

• <==>, <==, ==>推理表达式

• \forall, \exists等价于数理逻辑的全称量词和存在量词

• \old(x)某一属性变量(x)在方法执行前的值

• \sum, \max, \min返回给定范围内表达式的和/最大值/最小值

工具链测试

1.openJML

openJML是对JML规范性的检查，比较静态。我在本单元的作业中并没有使用这个进行检查，了解也较少，真正使用之后，感觉体验.......

在安装过程首先花费了大量的时间，而我最后的最后也只会用命令行对简单的java文件进行检查，其间还有各种找不到符号等报错。。。最终，我将代码改错（求平均年龄没有对除0进行特殊判断），他检测出了这个错误。

但整体感觉检测效果一般。

2.JMLunitNG

对MyGroup自动生成测试样例进行测试，运行效果如下：

[TestNG] Running:
  Command line suite

Failed: racEnabled()
Passed: constructor MyGroup(0)
Passed: constructor MyGroup(-2147483648)
Passed: constructor MyGroup(2147483647)
Passed: <<MyGroup@31639250>>.equals(null)
Passed: <<MyGroup@57179d81>>.equals(null)
Passed: <<MyGroup@14719726>.equals(null)
Passed: <<MyGroup@5c07468a>>.getId()
Passed: <<MyGroup@902fa6e3>>.getId()
Passed: <<MyGroup@6fd54415>>.getId()
Failed: <<MyGroup@0814c36d>>.addPerson(null)
Failed: <<MyGroup@72d38918>>.addPerson(null)
Failed: <<MyGroup@b8f35237>>.addPerson(null)
Passed: <<MyGroup@7a75622d>>.addPerson(java.lang.Object@9f590b16)
Passed: <<MyGroup@024171c6>>.addPerson(java.lang.Object@9b28d564)
Passed: <<MyGroup@0158772e>>.addPerson(java.lang.Object@08ca323d)
Passed: <<MyGroup@e359270b>>.equals(java.lang.Object@a516d58f)
Passed: <<MyGroup@9bf2963e>>.equals(java.lang.Object@cd890715)
Passed: <<MyGroup@6a1c1953>>.equals(java.lang.Object@37529975)
Passed: <<MyGroup@a829ef53>>.getConflictSum()
Passed: <<MyGroup@c3881647>>.getConflictSum()
Passed: <<MyGroup@bd50e573>>.getConflictSum()
Passed: <<MyGroup@740eb64c>>.getRelationSum()
Passed: <<MyGroup@2cd12150>>.getRelationSum()
Passed: <<MyGroup@62705b49>>.getRelationSum()
Passed: <<MyGroup@28764b6f>>.getValueSum()
Passed: <<MyGroup@96059213>>.getValueSum()
Passed: <<MyGroup@7328b538>>.getValueSum()
Passed: <<MyGroup@a7467d6f>>.getAgeMean()
Passed: <<MyGroup@2ad2690c>>.getAgeMean()
Passed: <<MyGroup@d9203a70>>.getAgeMean()
Passed: <<MyGroup@5c0783e9>>.getAgeVar()
Passed: <<MyGroup@e1460972>>.getAgeVar()
Passed: <<MyGroup@073f2340>>.getAgeVar()

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

由于我们的netWork对于null以及一些边界情况进行了特殊判断，所以其实程序本身不会出现调用netWork输入null对象的情况，但是随机生成的测试用例不会顾及全局程序，它就是无脑随机测试，所以会出现一些乌龙，整体来说，可以让我们的程序更全面、规范、严谨，也对我们写代码有一个提示作用吧。

3.SMT Solver

可以通过JML描述对代码进行检测，我在这里没有使用，但是和使用的朋友交流，感觉效果也不是很好。个人更倾向于junit检查以及自己写数据随机生成程序和别人对拍检测。

程序设计

本单元三次作业的设计都比较固定，按照JML的描述展开设计，一般可以保证正确性，但是在代码性能上应该稍微花一点心思，研究一下图论算法会对强测和互测带来较大的帮助。

第一次作业

第一次作业总体比较简单，按照JML书写不会有太大问题。在指导书最后说时间比较宽裕，但当时，我不相信课程组那么善良，总觉得isCircle的判断用bfs或者dfs复杂度较高，因此，采用了自己理解的并查集。在MyNetwork中用一个HashMap存储每个人以他对应的圈子，在添加人时候，将这个新人对应的圈子初始化为只有他自己的圈子，在添加关系进行判断+合并，在判断isCircle时，判断两个人对应的是不是一个圈子即可。实现上比较简单，也有较高的效率。

第二次作业

这次作业，我们都注意到了指令数的骤然增加，因此我对于每一个方法的查找进行了容器方面的优化。查找均用HashMap或者HashSet，遍历都用ArrayList，所以有可能出现有的成员变量用两种容器表示，牺牲了一定的内存，但是赢得了时间，较适用于本次的强测和互测。

本次作业新增加的方法就是组，对于组内的一些属性查询，我采取的是缓存机制，将关系数目以及平均年龄、年龄方差等变成了group的属性，采用改变时更新地方式，这样可以节省时间，获得较好的性能。

第三次作业

这次作业新增了一些比较复杂的方法，好在仁慈的课程组没有增加删除关系的方法，只是增加了组内删人的操作。因此，我们还是可以像组内加人一样，更新我们的一些属性，较好实现。本次作业的难点在于时间的控制上。两个方法是实现比较困难的：minPath + strongLinked。可能对于学过离散的蛇院朋友来说，这可能是图论的一些常规操作。可是高工的孩子只学过马散，我们只学会了如何运行python代码，这两个方法的实现还是有点费力的。

在经过和小伙伴的讨论后，我最终确定了minPath采用堆优化的迪杰斯特拉，strongLinked采用dfs标记+bfs删除的方式（经过一定优化的暴力删点）：对于isCircle的两个点，先找到两个点之间的一条路径，并对路径经过的中间点进行标记，之后分别删除这条路径之间的点，采用bfs删除，若都连通即可返回true，否则返回false。基于课程组善良的20条指令，加上这个方法本身的好实现，不易出错，该方法在我的朋友间得到了推广，直到——我发现，讨论区有大佬发了帖子，原来还可以用更高级的算法......下次，写代码可以把流程颠倒一下，先看帖子再去实现。

以下是我的UML类图

从图中可以看出，我的netWork类的方法数目较多，其实可以创建新的图类来分担其方法，虽然代码量并不大，但还可以让程序更加均衡美观，这也是我以后需要改进的地方。

bug发现及修复

这单元作业由于输出的确定性，评测可以采用对拍的形式，于是，码友圈开始了互相对拍的操作。大家互相传阅编译好的代码包，然后对拍，来保证自己的程序正确性。当然，这个办法是我们被OS以及建模比赛挤压的没有办法的办法了。在研讨课上，听了有同学分享，我才知道原来还可以直接用python中的包（python真香）。据说下单元还是图，如果不是被期末复习压榨的话，可能会尝试。

由于大家对拍的范围非常广，于是互测时码友圈出现了这样的对话：

A：B的代码被hack了，我当时和他对了20000组数据呢，慌了；

C：啊，可是咱俩当时也对了那么多组数据，岂不是要一起凉？

D、E、F.......

然而，事实证明，可能哪一个hack恰巧就是一个特殊的超时点，一人被hack，一圈人虚惊一场。

那么这单元都有哪些bug呢？

第一单元：在自己的程序中没有发现什么bug；但是在别人的代码中发现了对于isLinked的理解偏差的bug，当然，这都是不认真阅读JML导致的。

第二单元：本次作业遇到较多的是对于方差公式的变形。由于我们的年龄均值是int型表示，他不是一个精确值，因此方差公式不能照搬等价表述，需要进行一个简单的推导，否则在面对较多的数据时会直接死亡（和正确值永远差1的神必输出）；此外对于除0错误也是非常低级的错误，在阅读JML时就应当思考到的。

另外，由于这次的数据量较大，ctle也是经常出现的。我们的数据生成模式是有针对互测超时hack的，但是像我这种有原则的人，面对超时bug，我只hack一次，不会频繁hack（怕解除匿名后被打死.....）

第三单元：本单元主要就是一些不看讨论区的人，误用双dfs或者bfs，导致qsl判断错误，以及最短路径实现细节没有处理好（比如没有提前退出，坚持找到所有点的最短路径才退出）。而且，很多同学的代码存在侥幸心理，对于一些简单方法的实现严格按照JML，而不考虑性能，导致积累下来的时间较长，最后超时。

体会与感想

本单元作业让我们更加近距离接触了规格化设计。最初，我认为本单元是比较简单的，感觉JML给了，方法就很清晰，实现就是分块的，就不用去太在意框架。但到第二次作业，我发现虽然JML规定了方法的执行效果，但是给我们很大的设计空间。不同的实现方法可能会导致性能上的较大差别。

此外，JML对我们的细心程度提出了更高的要求，有时候一个条件的不注意，就导致满江红。因此，我们在设计之前要无比认真地思考每一个方法，并且可以一边写程序一边测试，这样也可以更好地保证自己的程序正确性。

这一单元，讨论区大家的讨论也让我有很大的收获，一些易错点的分析可以对我们有提醒作用；一些实现方法的交流，帮助我们积累的算法，提升程序性能。

OO课程接近尾声，最后一单元也要更加认真，希望可以给OO画上圆满的句号。