一、JML语言的理论基础、应用工具链情况
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。JML主要由Leavens教授在Larch上的工作，并融入了Betrand Meyer， John Guttag等人关于Design by Contract的研究成果。近年来，JML持续受到关注，为严格的程序设计提供了一套行之有效的方法。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的满足情况。
一般而言，JML有两种主要的用法：（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
JML三大要素：注释结构、表达式、方法规格。
注释结构：JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式为//@annotation，块注释的方式为/* @ annotation @*/。按照Javadoc习惯，JML注释一般放在被注释成分的紧邻上部。
表达式：JML的表达式是对Java表达式的扩展，新增了一些操作符和原子表达式。同样JML表达式中的操作符也有优先级的概念。分为原子表达式、量化表达式、集合表达式和操作符。
方法规格：方法规格的核心内容包括三个方面，前置条件、后置条件和副作用约定。其中前置条件是对方法输入参数的限制，如果不满足前置条件，方法执行结果不可预测，或者说不保证方法执行结果的正确性；后置条件是对方法执行结果的限制，如果执行结果满足后置条件，则表示方法执行正确，否则执行错误。副作用指方法在执行过程中对输入对象或this对象进行了修改（对其成员变量进行了赋值，或者调用其修改方法）。
JML 工具链主要有 JMLUnitNG，OpenJML 等。
二、JMLUnitNG测试
这个我就自己写了个小demo（equal函数）
public static boolean eq(int l, int r) { return l==r; }
结果如下：
[TestNG] Running:
Command line suite
Failed: racEnabled()
Passed: constructor Main()
Passed: static main(null)
Passed: static main({})
Passed: static eq(-2147483648, -2147483648)
Passed: static eq(0, -2147483648)
Passed: static eq(2147483647, -2147483648)
Passed: static eq(-2147483648, 0)
Passed: static eq(0, 0)
Passed: static eq(2147483647, 0)
Passed: static eq(-2147483648, 2147483647)
Passed: static eq(0, 2147483647)
Passed: static eq(2147483647, 2147483647)
结果他只能测一测边缘数据？那对于庞大的作业代码来说，他这个自动测试是没什么意义的。
三、架构设计
本单元作业，笔者并没有能够完成解耦设计，而是严格照着规格写代码，使几个类变得十分臃肿，并且为低性能埋下了隐患。
第一次作业
架构设计：照搬规格，数组变arraylist。因此整个作业只有iscircle函数需要自己设计内容。我用的是深度优先算法。沿着树的深度遍历树的节点，尽可能深的搜索树的分支。当节点v的所在边都己被探寻过或者在搜寻时结点不满足条件，搜索将回溯到发现节点v的那条边的起始节点。整个进程反复进行直到所有节点都被访问为止。
第二次作业
架构设计：和之前一样照搬了规格，但这次就吃了性能的亏了。首先查找算法不应该照搬规格的循环，应该用hashmap来存储键值对，用hash查找可以提升效率。并且group的查询算法都要设置缓存的，这样可以不用每次都重新查找，可以大大提升效率。因此addrelation时要判断连个人是否在一个group里，若是则进行更新。
第三次作业
架构设计：只是吸取了第二次的教训，但是队于dij算法的编写出了问题，采用加标志位的办法导致性能比较差。
关于queryBlockSum：查询连通块个数操作。使用并查集是一个更好的选择，添加人与关系时可以实现高效的维护，查询结果时可直接返回结果。
关于queryMinPath：最短路径查询算法，我才用的是dij算法，且在编写时的标志位设置是愚蠢的。
关于queryStrongLinked：使用使用tarjan算法，但代码能力捉急，出现了很多bug，甚是难受。
四、bug情况
第一次作业：查询路径算法编写有误，由于采用递归形式的算法，在返回指定设计上出现了纰漏，导致有时路径查询不到。并且在抛出异常的逻辑上，没有做到与规格完全一致，导致出现了该抛出异常没抛出的问题。
第二次作业：性能问题导致超时。arraylist的容器设计奠定了失败的基础，后改为hashmap并拆掉循环结果大有改善。并且再加入group各数值的缓存后性能达到要求。此外开始年龄平均数除零也没有考虑到。
第三次作业：dij算法和tarjan算法与hashmap存储结构的结合上出现了问题，导致程序出现bug。
五、心得体会
JML让我体会到 了代码的纪律性所在。但是感觉JML规格在编写方面也太复杂了吧，就拿第一次作业来说，好多规格的代码量是实现的十倍，这种东西如果让我来写规格的话我会很不爽，就一个return size却要写的很复杂。当然我知道这是为了其他复杂算法的简化表达不得不做出的牺牲，但是期待jml能够有更好的优化，减轻编写规格的人的负担。另外，dij和tarjan算法上出现问题，说明数据结构还是没打好基础，在面向对象这门课上露馅了，以后代码能力还是要加强。
对于代码实现者来说，最重要的就是不能照着规格来写代码，规格只是需求，我们要分析需求，从面向对象的角度出发寻找最好的解决办法。