一、JML理论基础
1.1 JML的用法
JML是用于对Java程序进行规格化设计的一种表示语言。JML有两种主要的用法：
（1）开展规格化设计。例如本单元的三次作业；
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。例如本单元的课上实验。
1.2 JML的注释结构
1 行注释： 2 //@annotation 3 4 块注释： 5 /* @ annotation @*/
1.3 JML表达式
| \result | 表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值 |
| \old( expr ) | 用来表示一个表达式 expr 在相应方法执行前的取值 |
| \not_assigned(x,y,...) | 用来表示括号中的变量是否在方法执行过程中被赋值 |
| \not_modified(x,y,...) |
与上面的\not_assigned表达式类似，该表达式限制括号中的变量在方法 |
| \nonnullelements( container ) | 表示 container 对象中存储的对象不会有 null |
| \type(type) | 返回类型type对应的类型(Class) |
| \typeof(expr) | 该表达式返回expr对应的准确类型 |
| \forall | 全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束 |
| \exists | 存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束 |
| \sum | 返回给定范围内的表达式的和 |
| \product | 返回给定范围内的表达式的连乘结果 |
| \max | 返回给定范围内的表达式的最大值 |
| \min | 返回给定范围内的表达式的最小值 |
| \num_of | 返回指定变量中满足相应条件的取值个数 |
| 子类型关系操作符 | E1<:E2表示类型E1是类型E2的子类型 |
| 等价关系操作符 | b_expr1<==>b_expr2 或者 b_expr1<=!=>b_expr2 |
| 推理操作符 | b_expr1==>b_expr2 或者 b_expr2<==b_expr1 |
| 变量引用操作符 | 例如\nothing指示一个空集，\everything指示一个全集 |
1.4 方法规格
| 前置条件 | 通过requires子句表示 |
| 后置条件 | 通过ensures子句表示 |
| 副作用范围限定 |
使用关键词assignable或者modifiable |
| 异常行为 | 通过signals子句表示 |
1.5 类型规格
| 不变式invariant | 要求在所有可见状态下都必须满足的特性 |
| 状态变化约束constraint |
对前序可见状态和当前可见状态的关系进行约束 |
二、JML应用工具链
OpenJML：使用OpenJML可以对JML代码实现静态语法检查和运行时检查；
JMLUnitNG：根据JML语言自动生成TestNG测试文件检查代码正确性；
JMLUnit：根据JML语言构造测试方法和测试用例，检验相应JML规格和代码实现的正确性；
……
三、JMLUnitNG测试部署
我选用JML工具链中的JMLUnitNG，对第十一次作业中Group接口和实现该接口的MyGroup.java文件自动生成测试文件和测试用例，最后通过运行MyGroup_JML_Test.java文件实现自动化测试。
获取jmlunitng.jar包，在命令行界面依次输入以下命令：
java -jar jmlunitng.jar MyGroup.java javac -cp jmlunitng.jar *.java java -cp jmlunitng.jar MyGroup_JML_Test
测试结果：
[TestNG] Running: Command line suite Failed: racEnabled() Passed: constructor MyGroup(-2147483648) Passed: constructor MyGroup(0) Passed: constructor MyGroup(2147483647) Failed: <<MyGroup@75dcdbd>>.addPerson(null) Failed: <<MyGroup@195d5c15>>.addPerson(null) Failed: <<MyGroup@449b2c27>>.addPerson(null) Failed: <<MyGroup@540a1e3f>>.delPerson(null) Failed: <<MyGroup@27d44f06>>.delPerson(null) Failed: <<MyGroup@6b133a5c>>.delPerson(null) Passed: <<MyGroup@7bf0d12c>>.equals(null) Passed: <<MyGroup@42d3a50a>>.equals(null) Passed: <<MyGroup@24573305>>.equals(null) Passed: <<MyGroup@5b2b2b87>>.equals(java.lang.Object@4ca5f779) Passed: <<MyGroup@102c22f3>>.equals(java.lang.Object@11e85a8) Passed: <<MyGroup@35c2ce>>.equals(java.lang.Object@5c56dbf4) Passed: <<MyGroup@23e52c67>>.getAgeMean() Passed: <<MyGroup@52d485b8>>.getAgeMean() Passed: <<MyGroup@375d235d>>.getAgeMean() Passed: <<MyGroup@662ace9>>.getAgeVar() Passed: <<MyGroup@76cc9116>>.getAgeVar() Passed: <<MyGroup@6aceb1a5>>.getAgeVar() Passed: <<MyGroup@2d6d8735>>.getConflictSum() Passed: <<MyGroup@ba4d54>>.getConflictSum() Passed: <<MyGroup@12bc6874>>.getConflictSum() Passed: <<MyGroup@de0a01f>>.getId() Passed: <<MyGroup@4c75cab9>>.getId() Passed: <<MyGroup@1efcfe8e>>.getId() Passed: <<MyGroup@67147f44>>.getRelationSum() Passed: <<MyGroup@5d3411d>>.getRelationSum() Passed: <<MyGroup@2471cca7>>.getRelationSum() Passed: <<MyGroup@5fe5c6f>>.getSize() Passed: <<MyGroup@5159e8cb>>.getSize() Passed: <<MyGroup@863d9750>>.getSize() Passed: <<MyGroup@5c0369c4>>.getValueSum() Passed: <<MyGroup@2be94b0f>>.getValueSum() Passed: <<MyGroup@d70c109>>.getValueSum() Failed: <<MyGroup@05c27366>>.hasPerson(null) Failed: <<MyGroup@50675990>>.hasPerson(null) Failed: <<MyGroup@32b7dea0>>.hasPerson(null)
=============================================== Command line suite Total tests run: 43, Failures: 10, Skips: 0 ===============================================
通过对测试结果的分析可知，JMLUnitNG能够对Group接口的每个方法进行自动测试，尤其能帮助我们测试意想不到的边界条件，在软件测试环节提供有效的帮助和补充。我在测试中未通过的测试点就是因为我照搬照抄规格，而忽视了对null等异常情况的处理。我不禁由衷赞叹：JMLUnitNG大法好！
四、作业架构设计
4.1 第九次作业
和前两单元的作业相比，本单元作业简单不少，开发背景是十分贴进日常生活的社交网络问题，程序架构和输入输出接口已基本给出，只需要照着jml规格愉快地做代码填空题即可，但是坑点较多。第九次作业只需要实现Person和Network两个接口和为数不多的几个方法。我在实现接口过程中我选用了hashmap容器，查找较为便捷。方法中稍难一些的是Network接口中的isCircle方法，仔细阅读规格后发现是图的连通问题，自然是我们熟悉并喜爱的数据结构和离散数学知识了。我原先采用dfs遍历，亲测发现多层递归极易爆栈，遂改用bfs，以为万事大吉。我第九次作业的架构设计图如下。
4.2 第十次作业
第十次作业在延续第九次作业设计架构基础上新增加了一个需要实现的Group接口和与之有关的若干方法，想必是为了实现我系同学喜闻乐见的“群聊”功能。注意要看清楚规格，用好数学公式，对一些较复杂的方法缓存一定量的数据，避免重复计算的冗余和浪费。我的第十次作业设计架构图如下。
4.3 第十一次作业
本单元三次作业的架构都具有较好的可扩展性，是真正意义上的迭代开发。第十一次作业没有增加新的接口，但是新增了一些方法，尤其以queryMinPath、queryStrongLinked、queryBlockSum三者为最难。我理解规格后又温习了许多数据结构和算法知识，与同学反复讨论研究，最终分别采用堆优化Dijkstar算法、tarjan算法和并查集算法实现了这三个方法，为了实现他们的功能也不得不增加一些新的类，尤其是Edge类用来存储每条边的信息。整体的设计架构却并不复杂，详见下图。
五、bug与修复情况
虽然看起来本单元作业比前两个单元简单许多，但我竟然连续3次中计翻车，屡战屡败屡败屡战，出现致命的bug。痛定思痛，痛何如哉。
5.1 第九次作业
第九次作业的bug出在addRelation方法，我有眼无珠，活生生地漏掉了id1 == id2 && contains(id1)这种情况，错误地抛出了异常，在强测和互测中都因此损失惨重。我在写代码时按自己的理解想当然了，没有仔细阅读jml规格，也没有在课下做充足的测试，甚至当我在看第一份互测代码时就意识到了自己的bug，人为刀俎我为鱼肉耳。
5.2 第十次作业
第十次作业的bug就是众人苦之久矣的求均值和方差时的除0异常，也让我付出了最惨痛的代价，我在强测结果公布后第一次心生大势已去之感。我不仅没有吸取上次的教训，反而继续囫囵吞枣不求甚解，看到比较长的jml规格就一目十行草草了事，漏掉了people.length == 0情况，错误原因与上次几乎如出一辙。当我看互测代码醒悟过来后立即提交了一份数据，hack到了同房间和我有一样bug的三名同学，为我们的粗心和麻痹大意造成的致命错误感到十分遗憾。
5.3 第十一次作业
这次作业我不敢再有丝毫的疏忽懈怠，反复阅读比对确认jml规格，认真学习打磨算法，queryMinPath、queryStrongLinked、queryBlockSum三个算法都是已知最优的，并且大量开展junit和对拍测试，发现了很多bug。我以为万无一失，没想到强测还是出现了令人沮丧的CTLE，尽人事听天命，我认了。所幸我每个点超时都不多，我没有屈服没有自暴自弃，首先把范围缩小到queryMinPath的锅，又经过分析才发现隐藏至今的危险——hashmap容器keySet遍历的复杂度极高，这暴露我对java底层实现的部分还存在很多的知识盲区，基础不牢地动山摇。在bug修复环节，我删去了queryMinPath中容器的初始化部分代码，又优化了容器和部分算法，亡羊补牢为时不晚，通过了强测CTLE的测试点。
六、心得体会
JML是实现规格化程序设计的重要手段。JML仿佛我们和软件需求方签订的一纸契约，又好像各国各公司程序员通行的“世界语言”。JML高度明确了类和方法的功能，提供了规格化测试的手段和方法。相比作业中的按JML写代码，我认为根据代码功能设计JML是更难的，我在两次课上实验都显得捉襟见肘原形毕露，我非常敬佩为我们写出如此多符合规范的JML的助教大佬。我为我自己没有珍视课程组的劳动成果、不仔细阅读学习JML而犯的错而感到无比惭愧。
我沉醉于JML周密严谨的理论逻辑，也深感我离散数学等知识的不足，为我之前几门课摸过的鱼后悔不已。对一名程序员来说，我应该苦练基本功，贯彻学习面向对象思想，在余下数周的oo课程和未来漫长的程序人生中洗心革面，及时勉励，学无止境，更上层楼。
庚子初夏 于金陵