JML理论基础
JML是对Java程序进行规格化设计的一种表示语言。
一般而言，JML有两种主要的用法：
- 开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
- 针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
下面对这几次上机中常用的表达式进行梳理。
JML表达式
原子表达式
esult表达式：表示一个非void类型的方法执行所获得的结果，即方法执行后的返回值。
old(expr)表达式：用来表示一个表达式expr在相应方法执行前的取值。
ot_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。
ot_modified(x,y,...)表达式：与上面的 ot_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取值未发生变化。
量化表达式
forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
操作符
推理操作符：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)：方法能够修改的类成员属性。
类型规格
约束(constraint)：主要描述数据状态变化应该满足的要求。
不变式(incariant)：主要描述数据状态应该满足的要求。
应用工具链
官方给出的工具只有OpenJML，用于检查JML注释的完整性。不过我只运行成功了一些比较简单的jml，并没有太深的体会。
JMLUnitNG/JMLUnit
架构设计
说起来有些惭愧，这三次的作业每次都是直接把上一次作业给复制过来然后新增东西。并没有做什么重构。
第一次作业
MyPath类用hashSet维护所有的点的集合，用ArrayList存储路径。
MyPathContainer类主要是使用了两个hashMap完成道路和编号的互相映射，在统计不同节点个数的时候用一个hashMap维护了一下节点的出现次数从而动态统计答案。
第二次作业
第二次作业就是将第一次作业中的边连成了一个图结构。为了方便，我将编号离散化，同时引入编号回收再利用机制保证了编号不会超过250。
if (buffer.isEmpty()) {
newId = ++nid;
} else {
newId = buffer.poll();
}
将编号离散化后，很多地方我直接使用了静态数组，虽然这样不是很好，但是写习惯了也就这样写了。因为对图结构改变的指令很少，每次都可以暴力重新构图。同时所有边边权相等，在最短路的时候可以使用又快有好写的Bfs。
第三次作业
第三次作业多了四个新的询问，在前两次作业的基础上，我增加了并查集来解决联通块个数问题。剩下三个问题本质上是一个问题，仅有的区别是边权不同，我通过传入不同的参数来生成这三种图，每种图独立的跑dij算法就行了。
private void reBuild() {
g0.constructGraph(pa2id, 0, id);
g1.constructGraph(pa2id, 1, id);
g2.constructGraph(pa2id, 2, id);
}
bug与测试
笔者三次作业在公测与互测中均没有被发现bug。
在测试的时候使用随机+对拍，既检查了极限数据下的时间和正确性，也检查了小数据情况下的正确性，让程序得到充分的测试。
心得体会
简单的撰写规格在几次上机中感觉没有什么特别大的问题，而且每次都能让我对规格有一些更深的理解，写的也尽量的完善。我感觉写jml花的时间可能会比较多，效率比较低，不如直接完成程序或者使用自然语言。不过架构设计其实是一种思维方式，重要的是学习一种规范编程的思维。
这一单元作业由官方给出了接口，让我们能更好的感受架构。它的可扩展性、可维护性等都很好，总体来说体验极佳。
最后祝OO越来越好！