目录
面向对象第三单元总结
JML语言
理论基础
简介
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。也是一种行为接口规格语言，基于Larch方法构建。提供了对方法和类型的规格定义手段。
JML有两种主要的用法：
-
开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是严格的规格。
-
针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。
注释结构
- requires子句定义该方法的前置条件(precondition)。
- 副作用范围限定，assignable列出这个方法能够修改的类成员属性，\nothing是个关键词，表示这个方法不对任何成员属性进行修改。
- ensures子句定义了后置条件。
JML表达式
- \forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
- \exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
- \sum表达式：返回给定范围内的表达式的和。
- \product表达式：返回给定范围内的表达式的连乘结果。
- \max表达式：返回给定范围内的表达式的最大值。
- \min表达式：返回给定范围内的表达式的最小值。
- \num_of表达式：返回指定变量中满足相应条件的取值个数。
- \result表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
- \old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。
- \not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。
- \type(type)表达式：返回类型type对应的类型(Class)。
方法规格
- 前置条件(pre-condition)：通过requires子句来表示，可以有多个requires子句，是并列关系。
- 后置条件(post-condition)：通过ensures子句来表示，可以有多个ensures 子句，是并列关系。
- 副作用范围限定(side-effects)：副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来 影响。从方法规格的角度，必须要明确给出副作用范围。
- 行为区分机制： public normal_behavior 表示接下来的部分对方法的正常功能给出 规格，一般指输入或方法关联this对象的状态在正常范围内时所指向的功能。public exceptional_behavior 表示异常功能的规格。其中的public 指相应的规格在所在包范围内的所有其他规格处都可见。
类型规格
- 不变式（invariant）是要求在所有可见状态下都必须满足的特性，语法上定义 invariant P。在方法执行期间，属于不可见状态对象的不变式有可能不满足。JML区分两类不变式，静态不变式和实例不变式 。其中静态不变式只针对类中的静态成员变量取值进行约束，而实例不变式则可以 针对静态成员变量和非静态成员变量的取值进行约束。
- 状态变化约束（constraint）是对前序可见状态和当前可见状态的关系进行约束，对象的状态在变化时往往也许满足一些约束，这种约束本质上也是一种不变式。
工具链
- openjml：对JML注释进行静态语法的完整性进行检查。
- JMLUnitNG：根据JML注释自动生成测试样例进行测试检查实现正确性。
- SMT Solver：检查代码规格，生成运行时测试样例。
JMLUnitNG测试
[TestNG] Running:
Command line suite
Failed: racEnabled()
Passed: constructor MyGroup(-2147483648)
Passed: constructor MyGroup(0)
Passed: constructor MyGroup(2147483647)
Passed: <MyGroup@80000000>.addPerson(null)
Passed: <MyGroup@0>.addPerson(null)
Passed: <MyGroup@7fffffff>.addPerson(null)
Passed: <MyGroup@80000000>.updateRelation(-2147483648)
Passed: <MyGroup@0>.updateRelation(-2147483648)
Passed: <MyGroup@7fffffff>.updateRelation(-2147483648)
Passed: <MyGroup@80000000>.updateRelation(0)
Passed: <MyGroup@0>.updateRelation(0)
Passed: <MyGroup@7fffffff>.updateRelation(0)
Passed: <MyGroup@80000000>.updateRelation(2147483647)
Passed: <MyGroup@0>.updateRelation(2147483647)
Passed: <MyGroup@7fffffff>.updateRelation(2147483647)
Passed: <MyGroup@80000000>.equals(null)
Passed: <MyGroup@0>.equals(null)
Passed: <MyGroup@7fffffff>.equals(null)
Passed: <MyGroup@80000000>.equals(java.lang.Object@61baa894)
Passed: <MyGroup@0>.equals(java.lang.Object@b065c63)
Passed: <MyGroup@7fffffff>.equals(java.lang.Object@768debd)
Passed: <MyGroup@80000000>.getAgeMean()
Passed: <MyGroup@0>.getAgeMean()
Passed: <MyGroup@7fffffff>.getAgeMean()
Passed: <MyGroup@80000000>.getAgeVar()
Passed: <MyGroup@0>.getAgeVar()
Passed: <MyGroup@7fffffff>.getAgeVar()
Passed: <MyGroup@80000000>.getConflictSum()
Passed: <MyGroup@0>.getConflictSum()
Passed: <MyGroup@7fffffff>.getConflictSum()
Passed: <MyGroup@80000000>.getId()
Passed: <MyGroup@0>.getId()
Passed: <MyGroup@7fffffff>.getId()
Passed: <MyGroup@80000000>.getRelationSum()
Passed: <MyGroup@0>.getRelationSum()
Passed: <MyGroup@7fffffff>.getRelationSum()
Passed: <MyGroup@80000000>.getValueSum()
Passed: <MyGroup@0>.getValueSum()
Passed: <MyGroup@7fffffff>.getValueSum()
Passed: <MyGroup@80000000>.hasPerson(null)
Passed: <MyGroup@0>.hasPerson(null)
Passed: <MyGroup@7fffffff>.hasPerson(null)
Passed: <MyGroup@80000000>.hashCode()
Passed: <MyGroup@0>.hashCode()
Passed: <MyGroup@7fffffff>.hashCode()
===============================================
通过数据可以看出JMLUnitNG基本都是通过边界数据或者null测试方法的正确性，比较极端。我认为测试还是应该通过Junit或者自动生成测试样例进行对拍，正确性测试应该更加充分。但核心思想还是要多测试，通过再多组的数据也未必是对的，程序的完全正确性无法保证，还是要尽量保证严谨性，严格实现JML规格。
架构设计
Homework 1
第一次作业是JML语言的熟悉，结构较为简单，新建的Set类为对并查集实现的封装，便于进行测试和修改，MyNetwork和MyPerson为主要的实现类，并且分别根据JML注释实现其中的方法。
Homework 2
第二次作业最大的变化是新加的MyGroup类，MyPerson与第一次相比完全不用改变，MyNetwork中新添加很多与MyGroup类相关的方法，本次强测上限100000条，多个方法JML描述的双重循环实现的方法我通过在更新其中本地变量状态时更新对应方法需要的临时变量，在调用方法时就不用每次重新计算结果浪费时间。
Homework 3
第三次作业重点在于MyNetwork类中新添加的很多关于图的算法实现，架构本身并没有改变，MinPath类是对其中queryMinPath()方法求最短路的代码的封装实现，便于进行测试，Node类则是MinPath求解最短路需要的临时数据结构。
bug修复
Homework 1
本次作业是JML入门的作业，熟悉了JML语言的语法和阅读，实现上也没有过多的限制，在认真阅读JML规格并实现后没有在强测和互测中出现bug。
Homework 2
前文的架构设计提到笔者在实现一些方法比如getRelationSum()、getValueSum()、getConflictSum()等通过缓存的方法实现，但MyGroup类中数据更新通过是addPerson()，笔者只有在该方法调用时才更新缓存数据，没有考虑MyGroup中的MyPerson的数据会在MyNetwork中调用addRelation()更新，所以在以下类似样例：
ap 1 jack 1 100
ap 2 mark 1 100
ag 1
atg 1 1
atg 2 1
ar 1 2 100
qgvs 1
都会出错，因为MyGroup中的数据没有更新，修复则是在MyGroup中添加updataRelation()方法，并在MyNetwork中addRelation()时调用该方法，bug得到了修复。
Homework 3
本次作业强测多点爆掉，互测中也被hack了3个点，bug修复*发现4个bug如下：
-
queryMinPath()方法我使用正常的dijskra算法没有使用任何优化，导致时间复杂度过高，修复是通过priorityQueue进行时间优化。 -
queryBlockSum()方法使用二重循环实现，也是导致时间复杂度过高，修复中通过并查集实现，主要是并没有理解该方法求的是什么，后续知道了是求解连通块数。 -
queryStrongLinked()方法我通过寻找两点之间所有的路径实现，在实现过程中由于没有判断数组下标的范围导致会数组越界访问出现RE问题。 -
queryStrongLinked()方法的寻找所有路径复杂度过高，比如如果图中出现较多环路就会导致两点之间路径数极多，全部寻找时间复杂度过高。bug修复重新实现了该方法，即去掉图中任意一个点后，两点依然连通，则返回true，否则返回false。
在bug修复后我进行了反思，笔者的最大问题一是对时间复杂度的估计与计算不够严谨和精确，二是没有良好的阅读讨论区的习惯，讨论区中很多优秀的帖子都提到了相关问题和解决思路，还有大家的多种想法也可以开拓思维，本次作业的bug也让我收获很多。
心得体会
本单元的JML学习让我第一次了解到了规格的作用，以前的很多课程作业写代码笔者都是对着需求直接实现代码，但在多人协同开发或者工程量较大时就会出现很多问题，规格就可以帮助非开发者对代码的阅读，不需要了解其中具体的实现方法，规格对项目的开发作用巨大。在三次作业对JML规格的阅读和实现中，笔者最大的收获是发现了自己的诸多问题，三次作业都没有进行充分的测试，也是由于对CTLE方面测试的不熟悉，需要严格的限制CPU的时间，还有就是应该多看看讨论区大家的想法，也很感谢很多大佬在讨论区发表自己的想法和见解，不能固步自封。十分感谢助教在本单元的作业设计和JML注释描述等多个部分的工作，感觉JML很多时候比代码实现都难写，JML规格的工具链在用起来感觉总有诸多问题，可能也是该规格还有待完善的地方，OO课程竟然已经到了最后一单元了，可以说OO课程是我这学期收获最大的一门课程没有之一，也希望能够在最后一单元有更多的收获和历练。