JML表达式
\result表达式：方法执行后的返回值。
\old( expr )表达式：用来表示一个表达式expr 在相应方法执行前的取值。
\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
\sum表达式：返回给定范围内的表达式的和。
\max，\min表达式：返回给定范围内的表达式的最大值、最小值。
等价关系操作符： b_expr1<==>b_expr2 或者b_expr1<=!=>b_expr2 分别表示表达式相等或不等。
推理操作符： b_expr1 = => b_expr2 或者b_expr2 <==b_expr1 。
方法规格
前置条件：requires P1||P2; 对方法输入参数的限制。
后置条件：ensures P; 对方法执行结果的限制。
副作用范围限定： assignable 可赋值 modifiable 可修改
pure方法：纯粹访问性的方法，即不会对对象的状态进行任何改变，也不需要提供输入参数。
方法的异常行为：normal_behavior, also, exceptional_behavior, signals (***Exception e) b_expr, signals_only。
类型规格
不变式invariant，要求在所有可见状态下都必须满足的特性。
状态变化约束constraint，来对前序可见状态和当前可见状态的关系进行约束。
JML编译器，比如OpenJML，编译含有JML标记的代码。
-check 选项可以对生成的类文件进行JML规范检查，检查是否含有语法错误；
-esc 选项可以对程序代码进行静态检查，检查程序中的潜在问题；
-rac 选项可以对程序代码进行运行时检查；
JMLdoc，与javadoc工具相似，不同的是它在生成的Html格式文档中包含JML规范；
JMLUnitNG，可以根据JML生成一个Java类文件测试的框架，结合OpenJML的-rac运行时检查选项，实现对代码的自动化测试。
测试代码
public class Path{
/*@ requires toAdd1 >= 0&&toAdd2>=0;
@ assignable \nothing;
@ ensures \result == toAdd1+toAdd2;
@*/
public /*@pure@*/ int add(int toAdd1,int toAdd2){
return toAdd1+toAdd2;
}
}
使用jmlunitng生成文件如下
（最后面还是没有调试出来不知道为什么...
其中MyPath直接管理点集数据，行为包括新建节点，对Path内数据的各类查询操作，以及生成迭代器。
MyPath其下的节点管理使用ArrayList的数据结构可以按位置查询，并建立点集HashSet，使查询结点存在性和不同结点个数的效率更高。迭代器让遍历更加迅速。
而MyPathContainer管理各Path，行为包括新建删除节点，和对Path与其下节点的查询操作。
对于题目要求的时间复杂度的限制，所以建立了两个HashMap，一个由Path到Id，另一个由Id到Path
另外对于不同结点的查询，我还建立了一个HashMap来记录已经访问过的点，每一次加的Path有这个结点就将该点的计数+1，remove时同理减1。这样大大提高了查询结点数量时的效率。
MyPathContainer类成员变量如下
HashMap<Path, Integer> pathToId;
private HashMap<Integer, Path> idToPath;
private HashMap<Integer, Integer> nodeSet;
依旧是题目要求的三个类，即Main，MyPath和MyGraph。
其中MyPath没有进行任何的修改，MyGraph继承了MyPathContainer的全部功能。但是由于数据管理更加方便等原因，并没有通过继承上次的代码来实现，而是直接复制了MyPathContainer的全部代码并进行了一定的修改。
MyGraph中的nodeSet修改为了HashMap<Integer, LinkedList<Integer>>，以方便对图的遍历。这个HashMap为结点指向一个链表，而这个链表中储存了这个结点直接相连的所有结点。
对于getShortestPathLength函数中的图的遍历，我在这次中使用的是dfs算法。时间复杂度较低，写起来也很简单。对于isConnected函数也是进行同样的操作，通过调用dfs算法。
这次作业还是很简单，只是犯了一个错误，没有记清楚JML的要求导致强测炸了，这是后话，后面分析bug再谈
在这一次作业中，我将图的相关功能与Path管理进行了分离。即基本的path和Id的转换依旧留在MyRailwaySystem里，但是关于图的最短相关计算和查询都放在了MyGraph里面。
在MyGraph里面设置了很多的成员变量。对于每一个结点都保存其连接的path，对于每一个path都保存了在该path上的换乘结点的信息。我当时的想法就是一个点到另外一个点只需要判断一些重要的结点就可以了，即换乘节点，其他节点是没有必要访问的。对于这个结构计算连通集就变得非常简单了。而在计算最短路径只需要计算起始节点到换乘节点和换乘节点之间就可以了。
但是我在计算的时候错误的使用了跟上一次作业一样的dfs算法。当我发现不对的时候已经离交作业只有五个小时了，所以没有时间进行重构了，于是直接由dfs强行转了bfs，导致强测爆炸0分。最后换乘节点之间的计算为bfs算法，而线内两结点的最短使用的是Floyd算法。因为是最后极限大改结构，所以我的成员变量包括整体结构都十分的混乱，基本是为了完成功能而随意添加语句。
这告诉我们下次一定要早点开始写orz
public class MyGraph {
private HashMap<Integer, ArrayList<Integer>> nodeSet;
private HashMap<Integer, ArrayList<PathSide>> pathSet;
private HashMap<Integer, Path> idToPath;
?
private HashMap<Integer, HashMap<Integer, Integer>> pathNode;
private HashMap<Integer, int[][]> pathShortest;
private HashMap<Integer, int[][]> pathUnpleasant;
private HashSet<Integer> pathIdSet;
private HashMap<PathSide, Integer> nodeUse;
private int minLength;
}
第一个作业没有bug跳过
第二次作业的bug是因为没有记清楚JML指令的要求。其中有一条是getShortestPathLength函数中如果fromNodeId和toNodeId相等，则输出0.没看见这一条所以没有写特判，让我强测挂了一大半。因为是不记得有这一条所以自己测试的时候也没有写过这样的样例，所以错了感觉十分可惜。
第三次作业的强测bug总所周知就是tle，因为深度优先的算法实在是太太太太慢了，即使结合了Floyd也一样很慢，强测直接得了0分。因为是算法的问题，而算法又连带了各种数据存储和程序结构的问题，所以除了重构之外没有其他方法。
JML在整体思路设计的时候能发挥很好的作用。特别是一份写得很清晰的JML，可以很很轻松的翻译成成行的代码。
但是JML也有很多不足，首先就是它不可能将一件稍微复杂一点的事情讲得完全清楚。总会有一些遗漏的点没有涉及。再者，就像是我第二次作业一样，有一个要求没看清，于是就爆炸了（当然也是我自己审题的问题）。
这次的作业前两次都比较简单，但是最后一次作业很难，而且更多的像是再考算法。
原文：https://www.cnblogs.com/lxy17373300/p/10906098.html