前言
在这单元的作业中，主要是根据规格化需求jml规格，实现相应的功能的类，难度层层递进。如果不需要考虑代码运行的cpu时间，时间复杂度的话，代码实现会叫容易一些。但是……现实总是很骨感，不幸的是，不顾时间复杂度，直接莽的话，只会收到一堆TLE。然而，在进行一堆优化之后，将痛苦地发现bug无处不在，尤其是第三次作业，一不小心，就会各种bug井喷。所以掌握好规格化测试的重要性不言而喻。
本文从JML语言梳理、部署SMT Solver进行验证、部署JML UnitNG并针对Graph接口的实现进行测试、梳理架构设计以及分析代码实现的bug和修复情况等三个方面对此单元进行总结，并阐述对规格撰写和理解上的心得体会。
一、JML语言梳理
1、JML语言的理论基础
据查询资料得，Java 建模语言(JML)将注释添加到 Java 代码中，这样我们就可以确定方法所执行的内容，而不必说明它们如何做到这一点。有了 JML，我们就可以描述方法预期的功能，无需考虑实现。通过这种方法，JML 将延迟过程设想的面向对象原则扩展到了方法设计阶段。
JML 为说明性的描述行为引入了许多构造。这些构造包括模型字段、量词、断言的可见度范围、前提条件、后置条件、不变量、合同继承以及正常行为与异常行为的规范。这些构造使得 JML 的功能变得非常强大
JML语言主要分为五个类型
①需求和职责
前提条件和后置条件
JML 关键字 requires 用于前提条件。 前提条件(precondition)指的是在调用方法之前必须要满足的条件。清单 1 指出 pop() 的前提条件是 isEmpty() 返回 false ;也就是说，队列中至少要包含一项。
方法的 后置条件(postcondition)指定该方法的职责;也就是说，当方法返回时，后置条件应当是 true
public 关键字的意义和在 Java 语言中的意义是一样的。 public 表示该 JML 规范对于应用程序中的其它所有类都是可见的。公共规范只能涉及公共方法和成员变量。JML 还允许规范拥有 private 、 protected 或 package 级别的作用域。JML 的作用域规则与 Java 语言中的相应规则类似。
normal_behavior 关键字表示该规范描述了 pop() 正常返回而没有抛出异常的情况。
exceptional_behavior
assignable ：方法的副作用
②模型字段
模型字段类似于只能在行为规范中使用的成员变量。下面有一个在 PriorityQueue 中使用的模型字段声明示例：
//@ public model instance JMLObjectBag elementsInQueue;
类级不变量
我们已经看到 JML 允许我们指定方法的前提条件和后置条件。它还允许我们指定类级不变量-实际上便为不变式与限制条件，类级不变量满足在类中每个方法的入口和出口处这些条件都必须为 true。例如， //@ public instance invariant elementsInQueue != null; 是 PriorityQueue 的类级不变量，在 PriorityQueue 的类中的所有函数返回之后， elementsInQueue 无论何时都不能是 null。
③关于继承
JML 规范是由实现接口的子类和类继承的(不同于 J2SE 1.4 中的断言语句)。JML 关键字 also 指出规范是与从祖先类继承的规范和从实现的接口继承的规范合并在一起的。除此之外，子类重写方法的前置条件只能宽于或者等于父类的方法，后置条件窄于或者等于父类方法的后置条件。
④最小堆和最大堆
BinaryHeap 允许客户机通过构造函数中的一个参数来指定它应当用作最小堆还是最大堆。我们使用布尔模型变量 isMinimumHeap 来指出 BinaryHeap 是用作最小堆还是最大堆。
量词
\forall， \exists 、 \sum 和 \min 。
⑤模型字段如何获取值
JML 使用 represents 子句来将模型字段和具体实现字段相关联，无论 JML 运行时断言检查器何时需要该模型字段的值，它都会查看 represents 子句中 <- 右边的代码段。
2、应用工具链
①开源的JML编译器，比如OpenJml，编译含有JML标记的代码。
②使用Openjml -check 选项可以对生成的类文件进行JML规范检查。
③利用Openjml中的SMT Solver，对代码等价性进行验证。
④通过Openjml -esc选项不依赖JML对代码的静态验证，SMT Solver会自动整理JML
⑤JML UnitNG可以生成一个Java类文件测试的框架，基于JML并结合Openjml的-rac运行时检查选项，实现对代码的自动化测试。主要是边界化数据测试。
二、部署JMLUnitNG/JMLUnit
本题主要的要求是针对Graph接口的实现自动生成测试用例（简单方法即可，如果依然存在困难的话尽力而为即可，具体见更新通告帖）， 并结合规格对生成的测试用例和数据进行简要分析
由于graph类实在有点复杂，不少人反馈一直报错，我决定转向Mypath类，但是，经我两个小时的操作，最后得到效果如下图，崩溃，从ArrayList 开始报错，绝望ing。
只能怂了，观摩大佬的教程，部署了一个简单的JMLUNintNG文件进行了测试，测试代码，测试过程和测试结果如下：
测试代码
public class Div {
//@ requires a > 0;
//@ requires b != 0;
//@ ensures \result == a/b;
public static int div(int a, int b){
return a/b;
}
public static void main(String args[]){
System.out.println(div(2,3));
}
}
测试过程如下：
测试结果如下：
可以看出jUNIT在程序中没有对b=0这一特例进行处理，导致fail。
三、架构设计梳理
第一次作业
设计思路
第一次作业要求较为简单，主要是设计一个path类，pathcontainer类实现简单的增删改查：
主要按照规格实现相应的功能，为了避免tle的问题，在原有的基础上增添private HashMap<Integer, Integer> disNode;
disnode键值集合为pathcontainer中所有不同点集合，值为对应不同点在pathcontainer中出现的次数。
注意点：在addPath,removePath,removePathById中对disNode进行相应的维护，即可降低getDistinctNode方法的复杂度，转换为直接获取disNode键集合大小的问题。将时间复杂度降为o（1）。
基于度量来分析自己的程序结构
程序结构
结果比较简单，基本上按照规格设计的
度量分析
总体来说，各种复杂度都比较好，主要是compareTo,,equals,GetDistinctNode的复杂度略高,主要原因是其多次调用Path中的变量。
第二次作业
设计思路
第二次作业中在第一次作业的基础上主要增添了最短路径和判断相应的点的连通的问题
解决方法：主要通过增添各边的邻接表，最主要的便是在addPath ，removePath,removePathById中进行相应的维护问题，其它便不太会出现问题。
最短路径的获取——public int getShortestPathLength(int fromNodeId, int toNodeId)
利用广度优先搜索即可实现获得目标点之间的最短路径。
连通的判断——public boolean isConnected(int fromNodeId, int toNodeId)
在同样应用bfs的情况下找不到最短路径的情况下，即判别这两个点事不连通的，即可实现第二次作业新增的功能。
基于度量来分析自己的程序结构
程序结构
程序结构也主要是按照规格化设计的，较为简单
度量分析
复杂度与第一次作业类似。
第三次作业
设计思路
重点来了，单元作业难度最高峰，对比第二次作业，真不是只升了一个阶层（数据结构没学好的我只能哭晕在厕所了），经多次观摩大佬的帖子，发现可以在求解最短路径，最少换乘次数，最少票价，最低不满意度，均可通过DIj实现，只不过传入的边矩阵中的权值不同，求解连通块的问题即转换为地铁图至少能够转换为多少个dij获得的点不相交path的问题，
本次作业最重要的便是换乘的判断，我的想法如下：
拿最少换乘次数举个栗子：
在Dij中初始化一个pathid的hashMap,键值为每个点转换的一一映射的下标值，value为最短路径中到达该点的pathid集合，
其中初始化pathid[indexof(fromNode)赋为fromNode所在的所有的pathid;
在传统的Dij中判断当前的点需不需要换乘，则变为当前的点与前一个pre所构成的边与pathid[pre]的交集是否为空，如果为空，判断是否对应的flag显示已经进行过换乘操作过了，如果没有则判断为换乘，并长度在原有的基础上+1，并置flag再次进入循环，否则则说明，在换乘的基础上此时仍是最短的距离，则把pathid进行修改为对应边的pathid.
基于度量来分析自己的程序结构
程序结构
java文件个数很少，文件达到750行，这也就导致checkstyle就非常致命。需要学会将功能细分，分别维护。
度量分析
可以看出addPath，Dij复杂度高，主要在于Dij需要获取多个路径矩阵。
分析代码实现的bug和修复情况
第一次作业
第一次作业要求较为简单：
在基本按照规格构建的基础上，添加一个hashmap disnode,将操作分散到各个方法之中，降低了该方法的时间复杂度，在此次公测和互测没有发现相应的bug，幸运过关。
第二次作业
第二次作业中在第一次作业的基础上主要增添了最短路径和判断相应的点的连通的问题
此次作业在公测与互测中均未发现bug,但是仍有需要改进的地方。例如在进行dfs操作时，可以将搜索过程中获得各点的最短路径存储下来，即可降低后续查询操作的复杂度。
第三次作业
重点来了，单元作业难度最高峰，对比第二次作业，真不是只升了一个阶层（数据结构没学好的我只能哭晕在厕所了），经多次观摩大佬的帖子，发现可以在求解最短路径，最少换乘次数，最少票价，最低不满意度，均可通过DIj实现，只不过传入的边矩阵中的权值不同，求解连通块的问题即转换为地铁图至少能够转换为多少个dij获得的不相交path的问题，哇塞，听起来，好清晰啊，but,理想很丰满，现实却很骨感。
菜鸡的我，非常美好地认为在dij的过程中存储好每个到达到该点的pathid,在判断换乘时即判断前一个的pathid集合与前一个点和后一个点构成的边所在的pathid集合是否有交集的问题，即可实现判断是否需要换乘。
but，我还是太年轻了，在
PATHADD 1 2
PATHADD 1 3 2 4
LEAST_TRANSFER_COUNT 1 4
在判断换乘的时候便会出错。在我的算法中 pathid.get(indexofNode(1)))=[1,2], edge.get(indexofNode(1),indexofNode(2))=[1],故获得二者的交集为[1],使得pathid.get(indexofNode(1)))=[1,2]，目前还没出现问题，但是在判断4时发现edge.get(indexofNode(2),indexofNode(4))=[2],pathid.get(indexofNode(2)))=[1],导致二者之间的交集为null,判断需要换乘，这与实际并不相符。
于是强测的各种花式WA，欲语泪先流啊，和同学讨论在发现，需要在存储多个不同的edge矩阵，进行拆点法，对于同一条路径上的各点依次存储每个点到其余点的距离，相应更新4个矩阵。在WA和TLE的边缘疯狂试探，或者二者兼有之，让人怀疑，这次作业是和前两次作业的亲兄弟吗？？？比悲伤更悲伤的故事，便是oo要你用数据结构，而你不熟……
四、对规格撰写和理解上的心得体会
就我的理解，规格撰写中最主要抓住前置条件与后置条件，若想后置条件的完全满足产品的需求，则需要在思考题意的时候便需要自己不断思考边界条件，不断揣摩后置条件会不会疏漏。
先进行规格化设计，在编写代码确实很有用处，不明晰自己每个函数要做什么，在小工程的层次上有可能可以实现，但在大工程的构建则是完全不可行的。
除此之外，在规格设计的时候，样例也要一边思考，最终完成代码时再想代码则会导致思考不够全面，测试的范围也不够全面，在中测很弱的情况下，强测WA声一篇。