一、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可以根据规格自动生成测试样例，检测程序的正确性。

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

 测试程序：

测试过程及结果：

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

三、按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构

第一次作业

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算法，其他的方法基本上都是沿用上一次的方法。

四、按照作业分析代码实现的bug和修复情况

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

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

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

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

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

至于规格理解，就要简单很多，在熟悉JML各种表达式及规格之后，对于规格要求的理解基本上不会存在偏差。

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

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