JML这一单元是真的有含金量，很有难度。而且这难点和前两单元完全不同，前两单元是容易架构混乱导致细节出问题，JML单元是读不懂JML规格的话架构都构不出来，以及即使能够读懂JML规格了，让自己写规格的时候又蒙圈了（大哭.jpg)。以及部署JML相关工具的时候能够比以上都令人崩溃（暴风哭泣.jpg)。
一、JML语言及工具
JML语言
JML（java Modeling Language）是用于对Java程序进行规格化设计的一种表示语言。其利用前置条件、后置条件、不变式等约束语法，描述了Java程序的数据、方法和类的规格，是一种契约式程序设计的实现工具。
1.原子表达式
esult: 方法（非void类型）执行后的返回值。
old(expr): 表达一个表达式expr相应方法执行前的取值。
2.量化表达式
forall: 全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
exists: 存在量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
sum: 返回给定范围内的表达式的和。
3.操作符
<==>, <=!=>: 等价关系操作符
== >,< ==: 推理操作符
othing, everything: 变量引用操作符
4.方法规格
requires: 前置条件
ensures: 后置条件
assignable, modifiable, pure: 副作用范围限定
signals, signals_only: 异常抛出语句
5.类型规格
invariant: 不变式
constraint: 变化约束
以上仅是对JML最简单且最常用语法等的梳理。其次，仅仅知晓这些基础语法是不够的，一定要多看代码，多书写JML规格进行练习（否则就会在要求写JML的时候大翻车）。
工具部分
- OpenJML： 对JML进行规范性检查
- JMLUnitNg： 结合OpenJml可实现对代码的自动化测试。
二、SMT Solver验证
对于OpenJml的部署，参考了学长的这篇博客https://www.cnblogs.com/lutingwang/p/openjml_basic.html（可以不用添加环境变量，直接命令行到对应文件夹下运行openjml命令即可）。下面是我的测试经过……
略过出现这个结果的各种报错，终于算是弄出来一个稍微能看的结果，此处报错显示Person类的缺失，然后我放入Person类进行测试……
（上图*.java仅包含Person类和Group类，均为官方第三次作业接口代码）然后出现了这个错，然后表示看不懂以及弄不懂了之后，遂放弃使用openjml进行进一步测试。
三、JMLUnitNg测试
此处工具的部署参考J哥的博客https://www.cnblogs.com/pekopekopeko/p/12920417.html
在其流程上修改为对自己的MyGroup类的测试（将Group的规格扔进了MyGroup类），同时魔改了Person类避免各种恼人的报错。
上图为成功运行时文件内容。
C:xxxxxxxjml>java -cp jmlunitng.jar test.MyGroup_JML_Test
[TestNG] Running:
Command line suite
Failed: racEnabled()
Passed: constructor MyGroup(-2147483648)
Passed: constructor MyGroup(0)
Passed: constructor MyGroup(2147483647)
Failed: <<test.MyGroup@6842775d>>.addPerson(null)
Passed: <<test.MyGroup@6c629d6e>>.addRelation(-2147483648, -2147483648, -2147483648)
Passed: <<test.MyGroup@27abe2cd>>.addRelation(0, -2147483648, -2147483648)
Passed: <<test.MyGroup@51016012>>.addRelation(2147483647, -2147483648, -2147483648)
Passed: <<test.MyGroup@1517365b>>.addRelation(-2147483648, 0, -2147483648)
Passed: <<test.MyGroup@60215eee>>.addRelation(0, 0, -2147483648)
Passed: <<test.MyGroup@768debd>>.addRelation(2147483647, 0, -2147483648)
Passed: <<test.MyGroup@449b2d27>>.addRelation(-2147483648, 2147483647, -2147483648)
Passed: <<test.MyGroup@66133adc>>.addRelation(0, 2147483647, -2147483648)
Passed: <<test.MyGroup@24273305>>.addRelation(2147483647, 2147483647, -2147483648)
Passed: <<test.MyGroup@1c2c22f3>>.addRelation(-2147483648, -2147483648, 0)
Passed: <<test.MyGroup@5a42bbf4>>.addRelation(0, -2147483648, 0)
Passed: <<test.MyGroup@4f4a7090>>.addRelation(2147483647, -2147483648, 0)
Passed: <<test.MyGroup@769c9116>>.addRelation(-2147483648, 0, 0)
Passed: <<test.MyGroup@12bc6874>>.addRelation(0, 0, 0)
Passed: <<test.MyGroup@1ef7fe8e>>.addRelation(2147483647, 0, 0)
Passed: <<test.MyGroup@5d3411d>>.addRelation(-2147483648, 2147483647, 0)
Passed: <<test.MyGroup@6979e8cb>>.addRelation(0, 2147483647, 0)
Passed: <<test.MyGroup@2be94b0f>>.addRelation(2147483647, 2147483647, 0)
Passed: <<test.MyGroup@50675690>>.addRelation(-2147483648, -2147483648, 2147483647)
Passed: <<test.MyGroup@47d384ee>>.addRelation(0, -2147483648, 2147483647)
Passed: <<test.MyGroup@3930015a>>.addRelation(2147483647, -2147483648, 2147483647)
Passed: <<test.MyGroup@1ff8b8f>>.addRelation(-2147483648, 0, 2147483647)
Passed: <<test.MyGroup@c39f790>>.addRelation(0, 0, 2147483647)
Passed: <<test.MyGroup@5f150435>>.addRelation(2147483647, 0, 2147483647)
Passed: <<test.MyGroup@75412c2f>>.addRelation(-2147483648, 2147483647, 2147483647)
Passed: <<test.MyGroup@f5f2bb7>>.addRelation(0, 2147483647, 2147483647)
Passed: <<test.MyGroup@3ecf72fd>>.addRelation(2147483647, 2147483647, 2147483647)
Failed: <<test.MyGroup@77f03bb1>>.delPerson(null)
Passed: <<test.MyGroup@7a92922>>.equals(null)
Passed: <<test.MyGroup@5474c6c>>.equals(java.lang.Object@4b6995df)
Passed: <<test.MyGroup@445b84c0>>.getAgeMean()
Passed: <<test.MyGroup@63d4e2ba>>.getAgeVar()
Passed: <<test.MyGroup@7006c658>>.getConflictSum()
Passed: <<test.MyGroup@7cdbc5d3>>.getId()
Passed: <<test.MyGroup@3834d63f>>.getPeopleSum()
Passed: <<test.MyGroup@34340fab>>.getRelationSum()
Passed: <<test.MyGroup@3ab39c39>>.getValueSum()
Failed: <<test.MyGroup@546a03af>>.hasPerson(null)
===============================================
Command line suite
Total tests run: 121, Failures: 10, Skips: 0
===============================================
上图为MyGroup类的实际测试效果（已删除部分测试代码）。由上图具体测试数据分析可知，JMLUnitNg测试数据几乎全部都是边界数据、0和null对象，感觉这样的测试意义也不太大，不具有普适性，不能起到很好的效果。
使用上面所述的工具的整体感受就是，这些工具真的很不完善，以及太鸡肋了，感觉意义不大。
四、作业架构分析
从总结课上知晓了这次作业的实际意图是让我们抽象出图结构，明晰代码的层次架构，从而更好的理解面向对象的思想。但是emmmmmm感觉自己的大多数时候其实是照着规格写代码，虽然抽象出了一定的图结构从而使用一定的图算法来优化，但是感觉还是离这一单元真正的目标有点差距。
三次作业的迭代关系和递进关系很明显，Person类即为一个节点，relation为边，在整个network里，将所有的person抽象为一幅图，在图中进行操作。Group类似于network的子图，其拥有完全不同于network的功能。
第一次作业：
第一次作业，基本按照规格实现，难点在于对规格的理解和对细节的掌握。在将架构抽象为图之后即可按照图的算法来解决iscircle问题，在此我选用的bfs算法，虽然不会超时，但是还是没有以后作业用的并查集香。
第二次作业
第二次作业增加了Group类，并且对于network类增加和Group类交互的功能，对于新增功能的实现都是按部就班的根据规格实现即可，但是由于测试数据集的增加，就要求我们在实现的时候要注意效率。所以我在Group内缓存了group类需求的所有数据，极大的节省了时间。其实感觉group类更像是节点的集合，并且维护集合内节点的共同属性。
第三次作业
第三次作业，对group新增del_person方法，对netwerk类新增更多的方法。其中group类的新增方法要求我们对缓存数据的更新需要更加小心，否则会wa的很惨。其次，network的新增方法抽象来看就是求连通块数目，求最短路径，判断两点是否强联通，这些都是图论的算法，这些方法的增加就要求了我们对这一单元作业的架构的抽象和理解。在理解了架构之后基本按照图论算法按部就班的写代码即可。
对于连通块数目的判断，我采用的并查集方式，同时也更新了iscircle方法，进一步节省了时间。
求最短路径采用了堆优化的迪杰斯特拉算法。
两点强联通我开始用的是暴力删点进行bfs判断联通的方法，但是中测结束前和同学对拍被暴打之后，遂花费一天的时间研究了一波tarjan算法，极大的缩短了时间（但是tarjan算法真的太容易错了，不然我也不会花费一天的时间了），虽然最后助教说暴力解法能过，但是至少多收获了一种算法。
第三次作业本质是大一数据结构的复（huan）习（zhai）作业。（bushi
五、代码实现的bug
在三次强测和互测中均未出现问题。
由于这一单元作业我强迫自己缓慢并且认真读规格，所以除开第三次算法部分，其余都是一次性过关，但是在和室友对拍的时候，室友总会冒出各种各样的小细节问题，同时也顺便给自己重新检查了一次，以及对作业的坑点有了进一步的了解。（虽然和室友对拍了很多，但是室友好像偶尔还是在强测或者互测出点问题，遗憾没能大家一起满分）
在前两次的互测中，由于屋内都是大佬，所以在测试完几个易错点和部分朴实数据之后就放弃了。当然最终结果还是屋内一直安静到底。但是在第三次互测中，由于自己摸了点鱼，评测机的数据针对性不强，所有在大部分人都hack了一个点的情况下，我的评测机毫无收获（我和我的评测机都太菜了）。
六、心得体会
虽然仅仅接触JML了三四周，但是确实也感受了契约式编程的优点和魅力，以及写的好的JML的无歧义是真的比普通的语言描述简洁而且舒服多了。但是JML也是真的难写（手动捂脸），非常容易描述不全，描述不清楚，和对情况的考虑的不完整……考虑的事情和细节太多太杂了，此处感谢此单元助教的辛苦付出（
其次，这一单元帮我复习了很多了图论的算法，迪杰斯特拉算法、bfs、dfs还新学了tarjan算法，收获颇丰。同时对算法的复习，也让我对程序性能有了更进一步的理解。总的来说这一单元的体验是真的不错，此处再次感谢老师和助教和付出。