一、作业概览
我们这一单元的主题是JML，即按照给定的JML规格实现具有要求功能的类，实现共3次编程作业，3次难度递进式增长，但每一次作业对前一次的作业有所继承和拓展。
- 第一次作业的任务是实现两个容器类Path和PathContainer，目标是JML规格入门级的理解和代码实现。
- 第二次作业的任务是
（一）JML理论基础
1.表达式
JML中的表达式包括原子表达式、量化表达式、集合表达式以及操作符等，下面按照作业中部分方法的规格对几种常用的表达式进行解释说明。
- esult 这个表达式表明了方法执行后的返回值，其类型和方法返回值的类型一致。
- old(expr) 这个表达式用来表示一个表达式在执行相应方法前的取值。
- forall 全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
- exists 存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
- max 给定范围内的表达式的最大值。
- min 给定范围内的表达式的最小值。
- ==> 推理操作符，用来表示两个表达式之间的蕴含关系，（expr1 ==> expr2，即表达式1蕴含表达式2）。
- <==> 等价操作符，用来表示两个表达式之间的等价关系。
2.方法规格
方法规格的核心包括前置条件、后置条件和副作用，为了区分方法的正常功能行为和异常行为，JML还提供了区分机制。
- equires 这个操作符规定了方法需要满足的前置条件（pre-condition）。
- assignable 这个操作符限定了方法可能产生的副作用，即规定了方法可以对什么变量进行修改。
- ensures 这个操作符规定了方法需要满足的后置条件（post-condition）。
- public normal_behavior 规定方法的正常功能的规格。
- public exceptional_behavior 规定方法的异常功能的规格。
- pure 访问性方法的标志，不会对对象的状态做出改变。
3类型规格
类型规格指针对Java程序中定义的数据类型所设计的限制规则，一般而言，就是指针对类或接口所设计的约束规则。
- 不变式invariant 要求在所有可见状态下必须满足的特性。
- 状态变化约束constraint 对前序可见状态和当前可见状态的关系进行约束。
下面用一个例子来说明以上内容的实际应用。
1 /*@ requires path != null; 2 @ assignable othing; 3 @ ensures esult == (exists int i; 0 <= i && i < pList.length; 4 @ pList[i].equals(path)); 5 @*/ 6 public /*@pure@*/ boolean containsPath(Path path);
在这个例子中，前置条件是输入的path不为空，因为是纯粹的访问性方法，不会对对象的状态做出改变，因此无副作用，后置条件是返回的结果应满足在我们用来储存path的容器中如果存在输入的路径则返回结果为真，否则为假。仿造对这个例子的解释，相信大家和我一样，能够理解JML规格带个程序的约束和好处。
（二）JML应用工具链
我所了解到的JML相关的工具有以下两个。
- Openjml：可以编译带有jml的代码，检查是否有语法错误，并检测是否存在错误隐患。
- JMLUnitNG/JMLUnit：可以根据代码生成测试的框架，自动化测试代码中存在的问题。
三、OpenJML和JMLUnitNG的使用
在使用这两个工具时，我遇到数不胜数的坑点，经过了漫长的踩坑填坑，我总算是可以跑起一份作业中最简单的Path类，下面我来梳理一下工具使用的流程和需要归避的问题。
（一）OpenJML
- 首先，我们在GitHub上下载得到OpenJML的压缩包，解压至喜欢的文件夹（路径上的文件夹的命名不可以是中文，我直接放在了D盘根目录）。
- 然后，我们根据自己的系统选择运行的SMT Slovers，我这里使用的是Win10系统。我们来写一个bat脚本，命名为openjml.bat（命名无所谓，按照功能命名比较好记忆），脚本中包含以下两行代码。
1 @echo off 2 java -jar D:openjml-0.8.42-20190401openjml.jar -prover cvc4 -exec D:openjml-0.8.42-20190401Solvers-windowscvc4-1.6.exe %*
第一行是为了使接下来执行的代码不显示命令行，在这个脚本中实际作用不大（可有可无），第二行是较为关键的代码，-jar参数后面的是openjml.jar的路径，cvc4是我们用到的SMT Slover，-exec参数后面的是我们的可执行文件的路径，最后的 %* 是我们要在控制台输入的参数（即之后要进行测试的文件）。
- 修改jml规格后，我们就可以愉快的使用openjml了。
1.首先用-check检测有没有语法错误
openjml -cp specs-homework-1-1.1-raw-jar-with-dependencies.jar -check test2/MyPath.java
运行的结果就是——没有结果，这说明你的jml是符合规格要求的，这里需要注意的是不要忘记包依赖关系。
2.接下来用-esc检测规格错误
openjml -cp specs-homework-1-1.1-raw-jar-with-dependencies.jar -esc test2/MyPath.java
这个在控制台运行时非常慢，而且会报出很多的warning，好像在IDEA中会运行的较快，但我并没有进行尝试，下面仅展示部分运行结果。
然而此时仍然没有运行完，这里不做过多解释。
（二）JMLUnitNG
- 首先，我们从讨论区获得jmlunitng.jar（附上链接：http://insttech.secretninjaformalmethods.org/software/jmlunitng/assets/jmlunitng.jar），把他放在我们上一步解压后openjml的文件夹下。
- 我们仿造前面的，再写一个bat脚本，命名为jmlunitng.bat，脚本中包含以下两行代码。
1 @echo off 2 java -jar D:openjml-0.8.42-20190401jmlunitng.jar %*
这里不再重复解释其意义。
- 然后我们就可以用jmlunitng生成测试样例了。
我们依次运行下方代码。
1 jmlunitng -cp specs-homework-1-1.1-raw-jar-with-dependencies.jar test2/MyPath.java 2 javac -cp jmlunitng.jar;specs-homework-1-1.1-raw-jar-with-dependencies.jar test2/*.java test2/MyPath_JML_Data/*.java 3 openjml -cp specs-homework-1-1.1-raw-jar-with-dependencies.jar -rac test2/MyPath.java
第一行代码的作用是用JMLUnitNG生成测试文件，第二行代码的作用是对生成的测试文件进行编译，最后一行代码的作用是用jmlc编译自己的文件。
- 最后，我们运行生成的TestNG的主文件。
java -cp jmlunitng.jar;specs-homework-1-1.1-raw-jar-with-dependencies.jar test2.MyPath_JML_Test
得到下图的结果。
到这里，Openjml和JMLUnitNG的使用告一段落。
四、架构设计
不得不承认，经过了前两个单元的洗礼，我的架构能力得到了极大的提升，每一次作业都可以在前一次作业的基础上进行新的修改，而不需要大费周折的重构，这就让我这一单元的体验好了许多。当然，JML带来的规范化也使我编码的目的更加明确，在写代码之前先明白自己想得到的输出，而不是直接在算法层面进行思考。下面我来对我三次作业中的设计进行阐述。
（一）第一次作业
第一次作业类图
在这一次的作业中，我们的目的是设计两个容器类，一个是Path类，另一个是PathContainer类。在设计的过程中，我们不仅要满足JML规格规定的内容，我们还必须满足“游戏规则”内给我们提出的更高的要求，尽可能降低方法的复杂度，尤其是那些没有单独限制条数的查询类操作，例如getDistinctNodeCount()方法，这个方法的复杂度高可以高至o(n2)，低也可以低至o(1)，这一现象为我的三次作业定下了一个基调——在避免多余操作的前提下，尽可能保存可以用于查询的对象，在这次作业中我就将一条path中的不同节点用一个数据结构存起来，这就避免了每次查询带来过大的时间开销。
上图为我第一次作业的类图，忽略掉MypathTest和MyPathContainerTest两个用junit测试方法的类，可以明显的看出第一次的两个容器类直接无依赖关系，单独存在，满足了JML规格的要求。
（二）第二次作业
第二次作业类图
在这一次的作业中，我们的目标是设计一个容器类Path和一个数据结构类Graph，其中Graph类继承了第一次作业中的MyPathContainer类。由于Path类和第一次作业中无任何改动，因此我直接将第一次作业中的Path类copy了过来，只是简单的更改了接口，Graph类我没有选择继承第一次的MyPathContainer类，而是将其中的代码copy了过来，去实现新增的几个方法，这是我在这次作业中的不足之处。
这次的重点依然是我们如何在满足正确性的前提下去降低方法的复杂度，这次我们要完成的图类，顾名思义是要建立一张图，分析需求可知，我们要建立的是一张无向图，且每条边的边权为1（权值相等），在这种条件下BFS（宽度优先搜索）无疑是较快的求最短路的方法，但即使其复杂度只有o(n)（采用建立邻接表的方式），如果每次查询都执行一次BFS的话依然会导致大量的时间开销，这里我们像第一次作业中存储不同点一样，在每次图结构更新的时候将所有点到其他点的最短通路求出来，保存在一个容器之中，在之后的查询过程中就可以快速得到结果了。至于是否含某条边，同样在更新图结构时进行维护即可。
上图为我第二次作业的类图，忽略掉用junit测试方法的类，可以明显的看出这次的两个类也没有依赖关系，各自单独存在，满足了JML规格的要求。
（三）第三次作业
第三次作业类图
在这一次的作业中，我们的目标是设计一个容器类Path和一个地铁系统类RailwaySystem，其中RailwaySystem类继承了第二次作业中的Graph类。这次的作业比之前两次的作业复杂了不少，因此更加需要合理的设计，一不小心就可能出现问题。新增的要求为求这个地铁系统内的连通块的数目（要求我们返回这个系统内连通图的个数），以及最小换乘、最低票价、最低不满意度的计算（要求我们返回按一定规定给每条边赋权值的带权图中的最短路径）。
分析完需求后，我们来考虑具体的实现，对于连通块的数目，我们仍沿用上两次作业中对不同节点数目、图中是否包含某条边的处理办法，在每次图结构变更时，进行更新，维护一个承载着联通块的容器。我们重点来考虑最短路的求法，我在处理时，首先是仿造真实的地铁，建立了一个站台类，每一个站台包含该站台的节点的id和所属路径的id，这样一来，我们成功将同一path上的节点id不同的站以及不同path上节点id相同的站区分开。我们建立邻接表，对应每个站台所有相邻的站台以及他们之间的权值，同一path上相邻站台权值为1，不同路径节点id相同的站权值为2。建立好邻接表，我们就可以考虑求最短路的算法了，这里我用的是堆优化的dijkstra算法，复杂度为o(nlogn)，显然我们不能每次都搜索一次，但我们这次不采用在图结构更新时更新所有最短路，而是在每次搜索时更新出发点到其他所有可达点的最短路并存起来（事实上第二次的作业也可以这样做），在图结构更新时清空缓存。按照前述方法，我顺利完成本次作业。
上图为我第三次作业的类图，忽略掉用junit测试方法的类，这次只用两个类单独实现会使得结构非常混乱，因此我新建了很多个新的类用来辅助实现，同时我这次的RailwaySystem类选择了继承上次作业中的Graph类，而不是简单粗暴的Ctrl-C，Ctrl-V，这使得整体的结构较为清晰。
五、bug分析及收获
值得开心的是，这三次的作业我在强测和互测中均未出现bug，除了自身能力的提升，按规格写代码确实带来一定增益。
oo的课程已经结束了3个单元，从一开始的继承、接口、多态到第二单元的多线程，再到这一单元的JML，我能感受到自己的进步，至少写出来的代码越来越可读，也更能理清自身的逻辑，对面向对象的思想也有了更深的理解。
期待在接下来的学习中能有更多收获。