一、JML语言的理论基础与应用工具链
JML是Java模块的行为接口规范语言。JML提供了语义来正式描述Java模块的行为，从而避免了有关模块设计者意图的歧义。其目标是提供严格的形式语义，同时仍然可供任何Java程序员访问。可以利用JML的行为规范的各种工具。因为规范可以作为注释写在Java程序文件中，或者存储在单独的规范文件中，所以具有JML规范的Java模块可以使用任何Java编译器进行编译。
JML语法
| 关键字 | 含义 |
|---|---|
| requires | 为该方法定义一个前提条件。 |
| ensures | 为该方法定义一个后置条件。 |
| signals | 定义一个引发异常的条件。 |
| signals_only | 定义在给定的前提条件成立时可能引发的异常。 |
| assignable | 定义该方法允许更改的变量 。 |
| pure | 声明一个不会产生副作用的方法。 |
| invarian | 定义类的不变属性。 |
| loop_invariant | 定义循环不变式。 |
| also | 用于合并规范用例。 |
| assert | 定义一个jml断言。 |
| spec_public | 声明出于规范目的的受保护或私有变量public。 |
还有以下表达式：
| 表达式 | 含义 |
|---|---|
| esult | 表示该方法的返回值。 |
| old( |
表示在使用expression之前的值。 |
| (forall |
全称量词 |
| (exists |
存在量词。 |
| a ==> b | 由a推出b。 |
| a <== b | a由b推出。 |
| a <==> b | a等价于b。 |
由以上表达式，就可以定义出一个方法的规格，方便理解。
二、JMLUnitNG/JMLUnit
第一次测试，显示有部分错误。HashMap需要写上完整说明，而第二个则是由于改变量名称时把方法名一起改了。
重新编译：
测试成功：
通过查看数据可以发现，自动生成的测试数据还是不够强，覆盖情况也不够广泛。自己在测试的时候还是使用了自己构造数据和随机生成数据的测试方法，随机还是很好用的。
三、作业分析
第一次作业
第一次作业要求较为简单。方法多为简单的查询数值，只有isCircle涉及了bfs的使用。
复杂度问题不大。
第二次作业
第二次作业开始显露这一单元的阴险狡诈。
刚开始还是按照上次的思路直接就写了，后来经人提醒改掉了所有的双循环，将可以在添加Person或Relation时计算的变量直接保存，就省去了每次循环计算的时间。
然后在互测的时候看到双循环就hack，一hack一个准。
第三次作业
捡起被遗忘的算法。
在查询双连通的时候用到了tarjan，由于自己使用样例的问题，以为可以直接通过low值判断是否双连通，最后证明前人搞这么麻烦必然是有他们的道理的。然后在截止前两小时极限改代码，好在没出大问题。
总结
这三次作业没有太多架构可以分析。各个方法之间都是独立的，如果要说设计，首先为了避免循环将可以存储的数值设为变量；然后自己觉得HashMap使用更方便，所以容器都采用了该类型。
四、bug与修复
第一次作业刚开始把bfs写错了，而且在使用HashMap的containsValue的时候没有重写hashcode和equals，后来还是使用了containsKey；第二次作业改掉双重循环后也没什么大问题；第三次作业里面主要就是自己对tarjan算法理解出了错。不过都在强测之前改掉了，强测与互测都没有出问题。
五、心得体会
感觉这次作业读JML不是主要问题，还是需要完全理解意思后进行设计，例如选择合适的容器、合适的算法。
例如在第二次作业中，同样是使用双重循环，有的同学就可以通过强测，根据后来的分析判断，还是使用容器的问题。ArrayList没能通过强测，而hashmap就没有问题。
自己在使用容器的时候还是因为HashMap的查找和遍历比较方便，考虑到id不同，就选择了HashMap。实际上对这些容器性能的差异还是不够了解。没有因为容器被卡，算是运气比较好。