一、JML语法总结
JML（Java Modeling Language）是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口 规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。BISL提供了对 方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。
一般而言，JML有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻 辑严格的规格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面 具有特别重要的意义。
level0是最核心的语言特征，也是我们这单元作业的基础，以下总结一些常见的JML语法：
| 原子表达式 | |
| esult | 有返回值方法执行后的返回值 |
| old(expr) | expr在方法执行前的取值 |
| ot_assigned(x,y...) | 表示x，y等在方法中未被赋值 |
| ype(type) | 返回值对应的类型 |
| 量化表达式 | |
| forall表达式 | 全称量词，给定范围内所有满足条件的元素 |
| exists表达式 | 存在量词，给定范围内存在元素满足条件约束 |
| sum表达式 | 给定范围内满足条件的表达式的和 |
| product表达式 | 给定范围内表达式的连乘结果 |
| max表达式 | 给定范围内表达式的最大值 |
| min表达式 | 给定范围内表达式的最小值 |
| um_of表达式 | 给定范围内满足条件的元素个数 |
| 操作符 | |
| <==> | 等价关系操作符 |
| ==> | 推理操作符 |
| othing | 空集 |
| everything | 全集 |
| 方法规格 | |
| equires | 前置条件 |
| ensures | 后置条件 |
| assignable | 副作用限定 |
二、使用JMLUnitNG进行测试
JMLUnitNG下载：http://insttech.secretninjaformalmethods.org/software/jmlunitng/assets/jmlunitng.jar
下载后使用如下命令：
java -jar jmlunitng.jar test/Group.java javac -cp jmlunitng.jar test/*.java java -jar openjml.jar -rac test/Group.java test/Person.java java -cp jmlunitng.jar test.Group_JML_Test
得到的测试结果：
其中第一条指令未响应，第二条指令会生成class文件，第三条指令如图：
提示警告信息，第四条指令无法执行。找了半天问题，去讨论区看了所有注意事项，还是没能成功。
三、作业设计
第一次作业：
UML图：
本次作业作为JML入门的作业，JML规格读起来不是很难懂，配合着函数名称可以很清楚的知道每一个方法需要实现的功能，唯一难点可能是isCircle函数，通过讨论区得知可以使用BFS或者DFS，这次作业使用的是BFS，算法实现没问题，但是保存遍历元素的数组没能在每一次遍历之前清空，导致错误。自己本地测试的时候没能够想到建立多个关系群分别进行测试，只简单测试了一下，翻车翻得不冤。
第二次作业
UML图：
第二次作业设计的时候没有考虑效率，被卡了很多数据点，没办法，只得以空间换取时间，建立两个链表，一个ArrayList负责遍历,一个HashMap负责查找，这样效率的到很大的提升，但还没完全过，只能去问了同学，发现是卡在queryGroupValueSum这个函数，由于每调用一次就需要双循环，耗时太多，所以需要使用缓存机制，跟最开始一个单元很像，当人员增加以及关系增添的时候更新ValueSum，就不会导致在具体使用时耗费时间。
第三次作业
UML图：
第三次作业仍然沿用第二次作业的框架，只不过多了许多需要算法实现的东西，本人学艺不精，只能慢慢摸索，现后尝试了许多算法，最后用没有堆优化的Dijkstra算法实现了queryMinPath，queryStrongLinked函数我是使用的一个笨方法，找到两点之间的左右路径，然后判断是否存在两条没有交点的路径，如果有那么就是true，否则false。看网上的Tarjan算法看的自己头疼，也读不懂。不过研讨课上有同学做了讲解，现在只是似懂非懂的阶段。
四、Bug测试
本单元作业的测试我是使用Junit（前两次），自己创造测试用例（前两次效果不佳，第三次）来进行测试的，可惜的是刚才做UML图的时候把第三次的生成测试数据的代码删除了，大致实现是自己创造两个文件test.txt和result.txt,然后成对的对两个文件写入指令和结果，一定保证正确。然后自己魔改一下Runner运行test.txt，将生成的myresult.txt与result.txt进行对比。不算很高明的做法，但是经过测试后的qsl指令除了超时没有出现错误。
五、体会与感想
本单元规格化设计思想可能在未来的工作中发挥比较大的作用，各个部门之间不仅需要这样的数据约束，而且通过简化细节使得方法的实现上需要花大功夫，本单元JML规格读懂和实现不是大问题，关键还需要满足性能的要求，课程可能存在一些目的与实践相分离的问题（规格化算法设计），但是这单元作业收获还是挺多的，包括各种算法以及JML的简单使用。
比较遗憾的是上边说到的工具链，包括没提到的Junit测试，使用起来还是不够熟练，使用的限制太多了，技术不够成熟。作为教学内容来讲的话，还是有些不足。
整体来讲，JML单元是需要我们理解规格化设计的思想，在实际工程中一定存在一些实现上的限制，这时候一种规范性的约束是比较好用的工具。