1、JML理论基础
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言（Behavior Interface Specifification Language，BISL），基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的满足情况。
以上内容摘自JML level0 手册。至于我个人理解的JML，则更像是一种描述代码实现者和使用者之间契约的形式化语言。根据各种JML语句的约束，可以直接从形式层面上验证代码实现的正确性。所以JML不仅可以协调调用者和实现者，还可以使得代码检验的效率更高。
这里关于JML的语法部分就不过多叙述，更详细内容可以参考上文中提到的JML手册。
2、JML应用工具链
这里首先要反省一下自己，本单元编写代码的过程中，除了官方要求的Junit测试以外，自己并未使用包括下文中的任何JML的工具。可能这种懒惰也是自己本单元bug百出的重要原因吧。
-
OpenJML
OpenJML主要功能包括三种：Parsing and Type-checking、Extended Static Checking、以及Runtime Assertion Checking。分别对应着对JML语法的检查和对代码的静态、动态检查。总的来说，可以对JML语言及其实现做一个比较全面的验证。
-
JMLUnitNG
JMLUnitNG主要起到一个针对JML的实现自动生成测试样例的作用，下文中将会有具体应用。
二、基于SMT Solver的验证
感谢讨论区同学提供的帖子：https://www.cnblogs.com/pekopekopeko/p/12920417.html
根据检验，出现了很莫名其妙的JML语法错误。询问运行成功的同学发现根本没有相同的情况，根据自己的判断，这次运行应该是有问题的。。。。然而由于网上关于OpenJML的SMT solver资料实在是很少，而且经过同学的讨论也不能得出一个很好的结果，因此只能遗憾地结束这部分的验证。查阅其他同学的总结，我发现大部分同学在这部分验证时都会碰到各种各样的玄学bug，最后只能进行一些十分简单方法的验证。故在此我想对此工具的实用性提出自己的疑问。。。（仅代表个人观点
三、JMLUnitNG自动测试样例的生成
生成关于Group接口及其实现的JMLUnitNG的自动测试如下图：
简单分析，发现equals(null)和addPerson(null)这个几个测试样例发生了fail。经检查，本人的addPerson实现确实并未考虑到添加空指针的情况，故应加以改进。但至于equals(null)发生错误，便令我感觉云里雾里了。经过使用junit进行测验，发现针对这种情况的test是正确的。那么原因到底是什么呢？经过与同学简单交流，发现大家都有各种花里胡哨的bug，最后问题可能只能归结到JMLUnitNG测试样例生成的内部实现上了。简单来说，就是两个字——玄学。
四、代码架构分析
本人在本单元的架构上的思考基本为0，错误地以为只要按照课程组给的jml去实现代码，而不用去考虑架构。所以我顺利地成为了典型反例，并成功地导致了代码性能上的极大损失。
在这里，我也无颜再谈什么分析架构，只是想做出些自我反省——我的视线一味地放在了jml的实现和有关算法上，而忽略了代码最基础的东西——架构。这就好像建房子忘了打地基一样，是极其愚蠢的行径。其余的话也不必再多说，只是希望以后写代码不要再一根筋，眼里只有那一部分内容，而是要将所学的所有知识方方面面结合起来，加以运用。
五、作业bug分析
说到本单元产生的bug，别的同学可能就是一句”三次作业均未发现bug“，而我就很有发言权了。下面是我的bug血泪史，希望这些bug能在日后时刻警醒自己。
1、容器容器容器
我在难度不大的HW2中栽了个大跟头。原因是我在优化代码性能时只是蠢蠢地去研究算法，而忽视了数据的载体——容器。以前我一直不重视这个东西，直到这次作业位置，都以为”万物皆可ArrayList“。终于，我对ArrayList的”独宠“迎来了报复——由于第二次作业强测有大量的查询操作，而ArrayList查询的复杂度远大于HashMap，所以我的性能迎来了大爆炸。同样的问题还出在HW3的计算最短路径方法中：我tm在记录每条边的长度时，又用了ArrayList，而不是堆优化的优先队列，再一次成功跳进了坑里。所以，我发誓以后再也不会用ArrayList。所以，我们在使用java中各类好用的容器时，还要多多考虑它们底层实现的性能。当你与敌国交战时，不知道手下将领的底细就随意给予重任，可能下一秒你就被内奸刀了。
2、算法算法算法
算法，这个我没有的东西。就像HW3中的计算点双连通分量的方法。如果真的掌握了Tarjan的话，谁有会暴力导致性能爆炸呢？就像计算最短路径的方法。如果真的知道堆优化dijkstra算法，谁有会写出那么臭的代码呢？归根到底，还是本人算法基础薄弱，又疏于联系的缘故。我可真是个five呢！没啥好说的，希望大家引以为戒。
六、个人心得体会
通过这个单元的学习，我第一次近距离接触到了形式化描述与验证这一块的内容。我发现，无论是实验课上撰写规格还是作业中完美地实现规格都不像我原以为的那么简单，它们都需要你先对整个工程和各部分之间的关系有个清晰的认识。而这个单元也让头脑简单、后知后觉的我数次折戟。
这个单元的核心是规格，但这只是核心，不是全部。如本文开头所述，规格确实是一份非常重要的契约，但其只是在形式化的抽象层次上进行了约束，而在具体实现上其实是有一定自由度的。如果我们在实现的时候也过于死板，照着这个约束来一步一步干，而不考虑如架构，算法等其他部分的话，那跟啥也不做又有什么区别呢？最后希望这单元给我带来的教训能化作我日后的经验吧。