JML语言的理论基础、应用工具链情况
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。可以通过开展规格化设计，而给代码实现者以明确、严谨的设计需求；也可以针对已有的代码给出规格，以提高代码的维护性。
结合Junit、OpenJML、SMT Solver等工具，可以对代码进行单元测试，检测其对规格的满足情况。但随着Java版本、IDE的迅速更新，一些工具难以继续维护，在使用时常常需要面对重重困难，对规格的检测也往往只能满足一些基本的测试需求（边界数据等），不能够完全保证代码的正确性。
总的来说，JML通过采用javadoc的方式，通过一系列语句来表示规格，可以严格规定方法实现的前置条件(pre-condition)、后置条件(post-condition)、副作用范围限定(side-effects)以及类的规格等。逻辑严谨、清晰。
部署JMLUnitNG生成测试用例
尝试多次还是无法成功部署，但结合成功的样例来看，生成的数据也只是一些边界数据（0，MAX_VALUE) 等，只能实现很基本的测试。
架构设计
本次作业通过迭代开发实现了一个社交网络（Network），里面有不同的成员（Person），成员之间互有联系，并且有属于他们的群组（Group）。抽象的来看就是一个无向带权图，多个方法也采用了图相关的算法。
代码实现的bug和修复情况
homework9
第一次上手JML规格的实现，相对比较简单。只有一个isCirle的联通判断的算法稍难一些，也没有复杂度相关的考虑。在强测中得到了100分，在互测中没有hack出别人，也没有被hack。
homework10
增添了Group类，其中的一些查询方法很可能会因复杂度过高而超时。测试中我的qgrs和qgvs头铁采用了每次查询时都双重循环遍历，妥妥收到了教训，强测95分，互测被hack多次，但都是这一个点。修复时改为设置dirty位的方法，避免每次查询时都进行遍历，仅在需要更新时进行遍历，成功解决了超时问题。
homework11
主要是在Network类中增加了查询联通块、最短路、点双联通的方法，很明显实现不当就会超时。在强测中我的qmp果然超时，主要是没有采用更合适hash容器，导致查询已访问过的结点时过慢。令我意外的是在互测中被hack出来2个正确性的bug。一个是ar是设置dirty位的判断，这算是上次作业的遗留问题，但在hw10中没有测出来，我自己也没有发现；一个是qsl少考虑了对于仅有两个人的图的特殊情况。
总结
这三次作业我均采用了特殊数据构造+随机数据测试的方式，但由于没有加入对cputime的统计、数据构造不够完善、以及实现时没有对代码时间复杂度的充分的分析，导致自己错误频出。
心得体会
- JML规格的确能给出逻辑较为严谨、清晰的要求，对代码的具体实现十分有利。但自己在实现的具体过程中，由于自己产生了“我照着规格写代码，岂不是就能满分了”的想法，仅仅把实现的重点放在了正确性上（虽然这一点在最后也没有得到保证），而没有对时间复杂度给出足够合理的估计和优化。
- JML的工具链还有待于进一步的完善，不能指望仅利用这些工具来保证代码的正确性，还是需要结合充足的单元测试。
- 我在代码的设计与实现分离这方面做的还是不够好。在设计较为完善的情况下，如何以保证规格设计的正确性为前提的同时，实现优雅、高效的代码，仍是我需要进一步提升的能力。