一、JML的理解与梳理
1.1 JAVA建模语言
Java建模语言（Java Modeling Language，JML）是一种进行详细设计的符号语言，它鼓励程序员用一种全新的方式来看待Java的类和方法。面向对象的分析和设计（OOAD）的一个重要原则就是过程性的思考应该尽可能地推迟，不过遵循这个原则的大多数人也不过是把这个原则适用到方法实现这个级别上。一旦设计好了类和接口，下面的事情自然就是实现其中定义的方法。
JML在Java代码中增加了一些符号，这些符号用来标识一个方法是干什么的，却并不关心它的实现。如果使用JML的话，我们就能够描述一个方法的预期的功能而不管他如何实现。通过这种方式，JML把过程性的思考延迟到方法设计中，从而扩展了面向对象设计的这个原则。JML引入了大量用于描述行为的结构，比如有模型域、量词、断言可视范围、预处理、后处理、条件继承以及正常行为（与异常行为相对）规范等等——这些结构使得JML非常强大。
个人认为JML的强大之处在于高度的抽象以及封装层次——如何形式化的证明一个程序是正确的？一般而言这个问题很难回答，因为程序因人而异，面对的应用场景也千差万别。但是一旦能从理论上统一对程序定量描述和抽象，就能在此基础上衍生出更好更可靠的程序理论。这就好像机械设计，有了零件和模块的理论描述，就能依据运动学、动力学理论设计出可靠又复杂的系统。我们一般而言的JML的优点，例如方便拓展和调试，保证正确性的继承等等都是这一逻辑特性的具体表现，个人认为其潜能应该不止于此。
1.2 JML工具链
开源的JML编译器如OpenJML可以编译含有JML标记的代码。
JML UnitNG可以生成一个Java类文件测试的框架，基于JML并结合Openjml的-rac运行时检查选项，实现对代码的自动化测试。据观察，这种测试主要是边界测试。
JMLdoc工具与Javadoc工具类似，可在生成的HTML格式文档中包含JML规范。
二、JMLUnitNG/JMLUnit的部署
使用JunitNG和OpenJML可以实现简单的程序测试和验证，下载好对应的jar包后，执行下列指令就可以实现自动测试。
java -jar JMLUnitNG.jar -cp specs-homework-2-1.2-raw-jar-with-dependencies.jar MyPath.java
javac -cp JMLUnitNG.jar;MyPath_JML_Test.java
java -jar .openjml-0.8.42-20190401openjml.jar -exec .openjml-0.8.42-20190401Solvers-windowsz3-4.7.1.exe -cp specs-homework-1-1.1-raw-jar-with-dependencies.jar -rac MyPath.java
java -cp .;JMLUnitNG.jar;specs-homework-1-1.1-raw-jar-with-dependencies.jar MyPath_JML_Test
其中为了使程序较为顺利的进行，改写MyPath.java如下：
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Iterator;
import java.util.stream.Collectors;
import java.util.stream.IntStream;
public class MyPath{
//@ public instance model non_null int[] nodes;
private int [] nodes;
public MyPath(int... nodeList) {
nodes = nodeList;
}
//@ ensures
esult == nodes.length;
public /*@pure@*/int size() {
return nodes.length;
}
/*@ requires index >= 0 && index < size();
@ assignable
othing;
@ ensures
esult == nodes[index];
@*/
public /*@pure@*/int getNode(int index) {
return nodes[index];
}
public static void main(String[] args) {
MyPath demo=new MyPath(1,2,3);
System.out.println(demo.size());
System.out.println(demo.getNode(1));
}
}
运行结果如下图：
可以看到程序检测出来的设计的简易程序中会出现的问题，例如non_null型变量可能在构造方法中指定为null值，程序还检测了边界情况。
三、架构设计与代码重构
3.1 第一次作业
第一次作业我本着“看规说话，合规即美”的思想，简单的根据JML实现最朴素的逻辑（算法都谈不上），错误的低估了课程组的要求。强测时很多点出现了TLE的问题，现在反思，主要有以下原因：
- 没有充分认识到题目的现实背景：现实中大部分查询系统都是多查少改的结构，每次查询都重新计算有失一个计算机专业学生的素质（尤其是已经学过缓存等等概念了）
- 没有认真结合数据结构的内容：数据结构是依附算法的一个很重要的程序设计内容，一味的使用简单粗暴的数组是初学者干的事情，程序不仅完成任务，更要完成好任务
3.2 第二次作业
有了第一次作业的教训，第二次作业我认真阅读数据点的类型，专门设计了加速的结构和算法。相比第一次作业无脑的思想，有以下改进：
- 优化数据结构，必要时增加成员变量和方法：在Path中设计HashSet，保证插入时直接去重，查找点数量时效率变高；使用HashMap保存path和pid的关系，由于path插入的顺序不重要，这样可以加速二者的对应
- 保存计算结果：在没有修改图结构前，每次都缓存之前已经计算的结果，如果没有对应的缓存，再重新计算，同时在BFS计算源点到目的点的距离时，保存中间结果
当然，这次作业有一些做的不好的地方，Graph类可以专门实现一个通用的图类，这样才能把图算法与其他计算独立，方便扩展。
3.3 第三次作业
第三次作业很明显有很多不同类型的图，同时点和边均有权重的概念，如何统一和抽象这些内容是本次作业的重点。一般而言，解决换乘类最短问题有两个想法：
1、拆点，即把不同路线的同名站点看作不同的点（这很合理，因为从一个地铁线站台到另一个地铁线站台是有距离的），但是带来的问题就是题目的输入没有给出乘客是在哪条地铁线的站点上车或者下车，什么时候站点要看做不同的，什么时候要看做相同的需要仔细考虑。我认为这样设计出的图不够通用——一个朴素的图类不应该带有过多和实际背景相关的信息，如果依靠拆点实现，势必要在图类里添加很多映射，计算最短路的算法里也得考虑各种情况。
2、加边，即把所有地铁子图看成全连接的，同时为每条边增加换乘的代价权值（即每次走图的一条边一定代表一次换乘），这样最后的最短路的边的个数一定是换乘的次数加一（因为如果有非换乘点，那么在该路线上一定有直接连接且更短的边）。我最后选择了这种算法，因为其中的图只是普通的带权无向图，结构上与一般图的模型一致，只是与实际的线路图有所区别。
这样要做的只是设计一个有用的图类UndirectedGraph，支持加边加点、计算最短路和连通块、缓存结果并管理。设计好后只需要根据票价、不满意度等规划图结构即可。
由于各个图建图过程极为相似，只有边权不同，我还加入了枚举类，一个方法可以根据枚举对象判断权值应为多少，从而提高代码重用度：
enum GraphType {
price, pleasant, transfer
}
四、BUG的分析与感想
这次的作业总的来说没有上次复杂，但是BUG还是存在的，总的可以分为以下两个方面：
-
看懂了规格但没有充分理解：最典型的例子就是自环和删边的问题，
1 1 2 3这样的输入，站点1和自己什么时候看作有边，什么时候看作没有？对于不同路线的同一条边或同一个点，删除一个路线是不是需要保证边或点仍然存在？一个点哪怕不在图里了，是不是还需记录一些它的信息？这些问题都可以从JML中找到答案，但是想要在看JML时想到这些问题可就没那么简单了。 -
细节把握的不够好：第二次作业我有一个十分致命和隐蔽的问题，足足DEBUG了9小时才找出来：
private void removeRefresh(Path path) { Integer previous = -1; for (Integer i : path) { if (nodeToNum.get(i) == 1) { nodeToNum.remove(i); } else { nodeToNum.replace(i, nodeToNum.get(i) - 1); } if (previous != -1) { removeEdge(i, previous); removeEdge(previous, i); } previous = i; } distance.clear(); }这段代码乍一看毫无问题，只是想通过一遍遍历同时修改点和边的信息。遍历边的逻辑是从第二个点开始处理当前点和前一个点的边，为此需要跳过第一个点。所以开始时变量
previous置为-1，当第一轮结束previous值被更新，进入边处理内容。然而我初值选用的-1，地铁站点的值也可能是-1（哪个地铁站会用-1当站号！），导致误判，这里初值完全可以使用null。这问题看着很蠢，可是在没给测试数据的情况下简直是穿着超级吉利服。痛定思痛，测试点的范围问题应当认真考虑。仔细分析，这也和没有充分阅读理解Path的规格描述有关。
再一次地，纸上得来终觉浅，绝知此事要躬行。程序规格咋一看很像一个把简单的问题强行说复杂的东西，然而其实它很像一个隐形的守护者（肖途），我们往往只能看到一个事物导致的结果，而往往容易忽视一个事物避免的结果——父母管束孩子会让孩子闷闷不乐一直惦记，但是孩子看不到没有父母自己会面对多少困难。程序规格守护着程序的正确性和严谨性，认真研究其框架对大型系统的开发或者多人协同的任务大有裨益。