BUAA_OO 第三单元JML作业总结
一、 作业总结
这三次作业是关于面向对象的规格的练习。这三次作业主要是关于一个社交网络的一个构建，作业主要任务就是按照JML规格对给出的一些函数进行完善。以下是针对三次JML的一些总结。
1.JML理论基础及应用工具链：
JML表达式：
原子表达式
esult表达式：表示一个非void 类型的方法执行所获得的结果，即方法执行后的返回值。
old( expr )表达式：用来表示一个表达式expr 在相应方法执行前的取值。
ot_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。
ot_modified(x,y,...)表达式：限制括号中的变量在方法执行期间的取值未发生变化。
onnullelements( container )表达式：表示container 对象中存储的对象不会有null
ype(type)表达式：返回类型type对应的类型(Class)
ypeof(expr)表达式：该表达式返回expr对应的准确类型
量化表达式
forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束
exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束
sum表达式：返回给定范围内的表达式的和
product表达式：返回给定范围内的表达式的连乘结果
max表达式：返回给定范围内的表达式的最大值
min表达式：返回给定范围内的表达式的最小值
um_of表达式：返回指定变量中满足相应条件的取值个数
操作符
子类型关系操作符： E1<:E2 ，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。如果E1和E2是相同的类型，该表达式的结果也为真
等价关系操作符： b_expr1<==>b_expr2 或者b_expr1<=!=>b_expr2 ，其中b_expr1和b_expr2都是布尔表达式，这两个表达式的意思是b_expr1==b_expr2 或者b_expr1 != b_expr2
推理操作符： b_expr1==>b_expr2 或者b_expr2<==b_expr1 。对于表达式b_expr1 ==> b_expr2而言，当b_expr1==false ，或者b_expr1==true 且b_expr2==true 时，整个表达式的值为true
方法规格：
前置条件(requires)：描述方法输入数据的要求。
后置条件(ensures)：方法执行结果满足的约束。
作用范围(assignable)：方法能够修改的类成员属性。
应用工具链：
在这次作业之中用到的JML相关的工具有OpenJML和JMLUnitNG。OpenJML是用来检查JML代码的完整性。JMLUnitNG则是根据JML自动生成测试文件。
2.JMLUnit
JMLUnit可以生成测试文件来对代码进行检查。由于我的编译器版本等各种问题，在此次作业之中我并没有用这个来检查自己的代码。
二、bug分析
1.Bug修复
第一次作业强测中我没有出现bug。第二次作业的强测和互测则出现了一个CPU超时的问题，这个是由于在执行Group类getRelationSum和getValueSum方法时利用双重遍历造成的超时。由于第二次作业对于性能的要求较为严格，这类指令的多次运行而多次使用双重循环而大大增加CPU运行时间。针对这个问题我在bug修复时像之前一样利用缓冲来解决这个问题。而第三次作业中则出现了一个小细节导致的巨大的问题，在强测和互测之中我都因为一些图的查询方法出现了CPU超时的问题。我开始一度以为是图的算法问题不够优化导致的，但是在bug修复中我多次进行这方面的优化发现并没有起到很好的效果。后来，通过不断地尝试，我终于发现了问题所在。这个问题并不是出在与图相关的MyNetwork类，而是MyPerson类。这个问题出现是因为我在对这个类中储存person的HashMap初始化时定义了一个5000的大小。开始这样做是为了节约hashmap扩容的时间，但是这样做的话就会导致开始遍历person时会遍历许多空的从而导致浪费了许多时间。没有想到找了一整天的bug居然只需要删掉这个就好了。
2.互测
这三次作业我主要是在第三次作业互测时进行了hack。我这次hack主要针对的点是对Network类queryStrongLinked方法。这个方法是查询两人之间是否成环。由于性能的要求，我造了大量的测试数据，对一些利用dfs方法来处理这个问题的代码进行了hack。
三、创建模式分析
这三次作业都是针对一个社交网络模型利用JMl规格来进行代码的完善。这三次作业没有重构的地方，但是在不同的作业针对一些方法、接口进行了一些容器上的和算法上的优化。由于对性能的要求，我此次采用的容器多是查找速度较快的Hashmap和Hashset来储存。而在完成第三次作业关于图部分的方法，我采用了查询最短路径的迪杰斯特拉算法，在连通块上我则利用了并查集来处理这个问题。这里贴出我第三次作业的类图与代码度量。
四、心得体会
这一次作业单元的主题是JML。而完成这个单元的作业之后，我觉得这次作业的重点不仅仅是关于JMl的。首先我们这次作业的代码完善的基础就是看懂JML。在实验课上我们也有写过JML，而想要完善这些代码，我们就先要通过看懂JML来明白一个方法所实现的功能。而在写这个方法的时候也要时刻注意JML中对这个方法做出的规范。而抛开JML，这次作业其实对图论和算法都有着较高的要求。这次作业的背景是社交网络，涉及到网络就涉及到了图。而关于图的一些概念则需要用到许多的算法，在上述的文字之中也有所提及。关于图的部分，或多或少的在离散数学之中有学到过。但是放到一个实际的环境之中就有了不同的要求和使用方法。在和同学进行一些交流和一些资料的查询后，我对不同的方法运用了不同的算法来解决。通过这次作业，我认识到了自己在算法上的一些缺乏，之后要多多积累，多多总结。而再看这次出现的bug，其实还是在做作业的时候思考不够，对一些自己写的代码考虑的不是很全面，在作业迭代的过程之中不能盲目的相信之前的代码，毕竟迭代的过程的要求不同，在做一次作业时不仅仅要完成这次作业的内容，还要检查之前的部分。