OO第三单元总结——JML
JML理论基础及工具链梳理
JML语言简介
JML(Java Modeling Language)是一种用于对JAVA程序进行规格化设计的语言，其通过定义接口所包含方法的行为，来约束实现接口的类的行为。用于逻辑化规约代码实现人员与调用者，同时提高代码的可维护性与复用性。
JML语法
- 使用Javadoc的注释语法，即 /*@ JML @*/。
- JML表达式
原子表达式
esult:表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
old(expr):用来表示一个表达式 expr 在相应方法执行前的取值。
ot_assigned(x,y,...):用来表示括号中的变量是否在方法执行过程中被赋值。如果没有被赋值，返回为 true ，否则返回 false 。实际上，该表达式主要用于后置条件的约束表示上，
即限制一个方法的实现不能对列表中的变量进行赋值。量化表达式
forall:全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
exists:存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
sum:返回给定范围内的表达式的和。
JML工具链
- OpenJML：用于检查JML语法。
- JMLUnitNG：用于自动生成测试用例。
- Junit：用于手动构造测试用例，进行单元测试。
JMLUnitNG的部署及使用
通过以下四条语句使用JMLUnitNG：
- java -jar jmlunitng.jar test/MyGroup.java
- javac -cp jmlunitng.jar test/*.java
- java -jar openjml.jar -rac test/MyGroup.java test/Person.java test/Group.java test/MyPerson.java
- java -cp jmlunitng.jar test.MyGroup_JML_Test
结果如图：
可以看出，JMLUnitNG主要针对一些边界数据进行测试，如int的最大/最小值、0值、对象的null值等，不具有普适性。
作业分析
第一次作业
架构设计
第一次作业中，难点主要在isCircle()方法上，而在isLinked()方法中有一个坑，即自己和自己也需要判定为连通。在数据容器上，我选择了HashMap进行Network中id与Person的对应存储，以及Person中Person与value的对应存储。UML图如下。
bug分析
本次作业在强测中出现了isCircle中死循环，以及没有考虑到isLinked包括自己与自己这一点两个bug，直接导致强测只过了一个点5分，没有进入互测。通过将isCircle从递归dfs改为bfs已经修复。
第二次作业
架构设计
第二次作业中，难点为Group的几个查询方法中的超时问题。我在大部分方法中采用了在向组内加人时进行更新的方法，避免了超时问题。UML图如下。
bug分析
本次作业在强测中出现了查询年龄时除0的问题。其原因是我在将查询年龄的方法改为上述加人时更新的时候忘记了考虑组里为空的情况，导致对一个空的Group进行查询就会出现RE，强测只过了4个点20分，勉强进了互测。互测中出现了一个isCircle的超时问题，也没有找到什么方法优化。
第三次作业
架构设计
第三次作业中，难点为新加入的qsl、qbs、qmp三个方法，其本质分别为图论中的判断点双连通、求连通分量数、求最短路径。我分别使用了Tarjan算法、bfs遍历和Dijkstra算法进行解决。UML图如下。
bug分析
本次作业在强测中获得了70分，出现了以下几个问题：1，qmp的超时问题，目前还未想出优化方法；2，qsl出现了一个WA，但在本地没能复现问题，很迷惑；3，qbs的超时问题，通过在加人及加关系时更新已经修复。在互测中，也出现了两次被hack超时，也在上述三个bug之中。
心(chen)得(tong)体(fan)会(si)
本单元对规格及JML的学习我认为并不成功。在第一单元刚接触JML和规格时，它给我的感觉就是各个方法已经用伪代码写好了，只需要翻译成Java语言即可。在看了一些讨论之后，我开始认识到JML规格和我想象的不一样。它只是给了一个输入和输出的规范，内部过程仍然需要自己编写。而在本单元学习之后，我发现自己就是老师多次提及的提交的代码中只有MyGroup、MyNetwork、MyPerson和主类四个类的那类同学，说明我对JML规格的理解仍然有很大的问题。即使给了JML规格，也同样需要思考程序架构，而不是割裂开去完成一个个方法。
此外，测试能力的欠缺也同样致命。第一次作业中，由于没有仔细看中（ruo）测的数据，以为已经没什么大问题了就没有再进行测试，结果大翻车。第二次作业中当我下定决心要测试时，我却发现不知道该怎么测。尝试编写JUnit单元测试样例，发现写不出有效的测试，只会测一些最最简单的情形，最终只是进行了一些黑盒测试，也没能测出除0的bug。第三次作业中也同样没能做全面的覆盖性测试，所幸用黑盒测试测出了大部分错误。
第三则是数据结构和算法方面，在第三次作业中尤其明显。Tarjan算法是现学的，也出了很多bug，其中大部分都在本地测出并修复了，强测又测出了一个bug，但是本地没能复现。Dijkstra算法在实现上可能也有点问题，出现了超时。这说明在数据结构与算法方面还略显薄弱。
总之，本单元的学习体验很好（所花费的时间大大缩短），但结果却很差。但同样也总归是检验出了一些问题，需要在之后的学习中一一解决。