OO第三单元做业小结

1、JML理论基础及应用工具链状况

理论基础

1.JML表达式

\result：表示方法执行后的返回值。

\old(expr)：表示一个表达式expr在相应方法执行前的取值。

\foall：全称量词修饰的表达式。

\exists：存在量词修饰的表达式。

<==>：等价关系操做符。

==>：推理操做符。

\nothing：变量引用操做符，指示一个空集。

\everything：变量引用操做符，指示一个全集。

2.方法规格

requires：表示前置条件(pre-condition)。

ensures：表示后置条件(post-condition)。

assignable：表示反作用范围限定(side-effects)。

3.类型规格

invariant：不变式，要求在全部可见状态下都必须知足的特性。

constraint：状态变化约束，对前序可见状态和当前可见状态的关系进行约束。

应用工具链

OpenJML能够对规格进行检查，包括语法正确性检查、静态检查、运行时检查。

JMLUnitNG能够根据规格自动生成测试样例，检测程序的正确性。

2、部署JMLUnitNG/JMLUnit，实现自动生成测试用例

 测试程序：

测试过程及结果：

测试样例主要是针对数据的边界状况，三个没有经过的测试点都是由减法溢出致使的。

3、按照做业梳理本身的架构设计，并特别分析迭代中对架构的重构

第一次做业

MyPath类里，用一个arraylist来存路径中的全部点，以及一个hashmap来存全部不一样的点。方法都是按照规格完成，值得一提的是从大佬那里学来了简单的重写hashCode()的方法——直接return类中arraylist的hashCode()，由于对于arraylist来讲，相同内容的两个arraylist，它们的hashCode是相同的。

MyPathContainer类里，因为MyPath重写了hashCode()方法，直接创建以id做为key、path做为value和以path做为key、id做为value的双向hashmap。另外对于全部不一样点的个数，创建一个以点的id做为key，点的出现次数做为value的hashmap，在add和remove path时，对这一hashmap进行维护，将增长或删除的路径中的全部点的出现次数在这一hashmap中的value值进行加或减，次数为0时直接删除，这样在获取不一样点个数时就能够直接return这一hashmap的size()。

第二次做业

第二次做业采用的是floyd算法求最短路径，每次add或者remove，都根据graph中存储的全部path创建一个二维矩阵，而后用floyd算法求解。

第三次做业

第三次做业仍采用floyd算法，基本方法参考讨论区大佬的不拆点方法（这方法真的太强了），维护四个二维矩阵，而且对于每一个路径的不满意度和票价矩阵都用一次floyd，最后在每一次add和remove时，都从新初始化四个矩阵并各自floyd，以获得最终结果。

这三次做业其实基本上没有太多重构，由于第二三次都是用的floyd算法，其余的方法基本上都是沿用上一次的方法。

4、按照做业分析代码实现的bug和修复状况

第一次做业比较简单，没有出现bug。

第二次做业强测wa了两个测试点，互测被刀了两刀，都是源于同一处bug。因为路径中的点并非从0开始递增，在创建二维数组时，须要创建一个从点的id到递增天然数的一个映射，以表示数组的index。我在每一次add和remove时，都会先将二维数组初始化，而忘记将储存映射关系的hashmap也初始化，这就致使删除了某些点以后，它的映射关系仍储存在hashmap中，会出现数组越界的错误。

第三次做业也吸收了第二次做业的教训，没有出现bug。

5、阐述对规格撰写和理解上的心得体会

 在规格撰写方面，在几回上机以及理论课上的练习中，感受撰写规格要比理解规格难一些，感受一次性很难完整写出一个方法的规格。

至于规格理解，就要简单不少，在熟悉JML各类表达式及规格以后，对于规格要求的理解基本上不会存在误差。

其实本单元的做业，主要难点仍是在于算法及架构设计上，因为CPU时间作出了要求，咱们必须充分考虑选择算法的时间复杂度，而第三次做业增长的票价、不满意度等计算，进一步加大了代码设计的难度。

总的来讲，规格仍是颇有用的，它能很好地规范代码，并且能帮助程序员养成良好的代码编写习惯。