目录
BUAA_OO_JML单元总结一、JML语言理论基础JML概述JML语法简述JML应用工具链二、SMT Solver应用三、JML UnitNG自动生成样例四、本单元作业分析架构设计与重构分析BUG分析与修复五、单元学习体会
BUAA_OO_JML单元总结
一、JML语言理论基础
JML概述
Java建模语言（JML）是一种行为接口规范语言，可用于指定Java模块的行为。我们知道，面向对象分析和设计的原则之一就是应当尽可能地把过程设想往后推，把精力集中于整体架构的设计，协调管理各个单元部件的运转，而不拘泥于某些琐碎细节实现当中。
因此，在设计层面，我们对于每一个类以及方法，要淡化过程，只需关注它的结果，所以我们需要精准地描述出它的行为以及影响。（就和计组中，我们使用列表的方法将IFU、ALU、GRF等部件的输入输出功能全部列举出来一样。）但是 Java 语言没有提供显式地将这种信息合并到代码中的方法，JML便应运而生。
JML语法简述
JML作为一种接口规格语言，包含的大量知识是一篇博客所不能承载的。
首先，如果有什么记不清的内容，当然首选查阅课程组JML手册(链接在这里)啦。
其次，官方文档(链接在这里)中包含了JML的全部内容，想要拓展JML语法知识可以选择食用。
按惯例列举一波常用操作：
1、JML表达式
原子表达式
\result\old()\not_assigned()\not_modified()\nonnullelements()\type()\typeof()
量化表达式
\forall\exists\sum\product\max\min\num_of
操作符
子类型关系操作符 <:
等价关系操作符 <==>
推理操作符 ==>
变量应用 \nothing \everything
2、方法规格
前置条件 reqquires后置条件 ensures副作用范围限定 assignable modifiablesignals子句
3、类规格
状态变化约束 constraint不变式 invariant
如果发现自己不记得，当然要回去再看看啦~
JML应用工具链
在本单元学习JML的过程中主要引用到的工具有SMT Solver、OpenJML、JML UnitNG。吐槽一下这些工具的帮助文档写的比较魔鬼以及中文资料真的非常匮乏，所以真心感谢讨论区大佬们的帮助！
二、SMT Solver应用
这里使用的是OpenJML命令行来进行代码审查，配置过程参考讨论区伦佬帖子。
同时为了方便命令行表述，可以编写bat来进行简化（或者bash）。这里使用bat，保存为openjml.bat并添加到环境变量中。
java -jar D:/OpenJML/openjml-0.8.42-0401/openjml.jar %*
测试一 使用check选项检查JML语法
只需使用
openjml -check xxxxx.java
检查相应的文件即可，如果所有JML语法正确，那么将不会有任何显示，如果有错误，那么将会出现提示。
而这个功能局限性也非常大，首先不能检查/forall、/exists等语句，会报错；其次，也不能检测到继承。
这里以Graph.java作为例子，检查结果如下（只贴部分）：
Graph.java:6: 错误: 找不到符号public interface Graph extends PathContainer {^符号: 类 PathContainerGraph.java:28: 错误: 找不到符号public /*@pure@*/ boolean isConnected(int fromNodeId, int toNodeId) throws NodeIdNotFoundException;^符号: 类 NodeIdNotFoundException位置: 接口 GraphGraph.java:47: 错误: 找不到符号public /*@pure@*/ int getShortestPathLength(int fromNodeId, int toNodeId) throws NodeIdNotFoundException, NodeNotConnectedException;^符号: 类 NodeIdNotFoundException位置: 接口 GraphGraph.java:47: 错误: 找不到符号public /*@pure@*/ int getShortestPathLength(int fromNodeId, int toNodeId) throws NodeIdNotFoundException, NodeNotConnectedException;^符号: 类 NodeNotConnectedException位置: 接口 GraphGraph.java:7: 错误: 找不到符号//@ ensures \result == (\exists Path path; path.isValid() && containsPath(path); path.containsNode(nodeId));^符号: 类 Path位置: 接口 GraphGraph.java:10: 错误: 找不到符号/*@ ensures \result == (\exists Path path; path.isValid() && containsPath(path);^符号: 类 Path位置: 接口 GraphGraph.java:17: 错误: 找不到符号@ requires (\exists Path path; path.isValid() && containsPath(path); path.containsNode(fromNodeId)) &&^符号: 类 Path位置: 接口 GraphGraph.java:18: 错误: 找不到符号@(\exists Path path; path.isValid() && containsPath(path); path.containsNode(toNodeId));^符号: 类 Path位置: 接口 GraphGraph.java:25: 错误: 找不到符号@ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(fromNodeId));^符号: 类 NodeIdNotFoundException位置: 接口 GraphGraph.java:25: 错误: 找不到符号@ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(fromNodeId));^符号: 类 Path位置: 接口 GraphGraph.java:26: 错误: 找不到符号@ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(toNodeId));^符号: 类 NodeIdNotFoundException位置: 接口 GraphGraph.java:26: 错误: 找不到符号@ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(toNodeId));^符号: 类 Path位置: 接口 GraphGraph.java:31: 错误: 找不到符号@ requires (\exists Path path; path.isValid() && containsPath(path); path.containsNode(fromNodeId)) &&
所以这个功能，玩玩开心就好
测试二 使用esc选项进行代码静态检查
静态检查不依赖于JML。使用
openjml -esc xxxxx.java
即可检查。
测试三 使用rac选项进行动态检查
使用指令
java -jar openjml.jar -rac xxxx.javajava -classpath ".;jmlruntime.jar" xxxx
即可检查错误，这里自己写一个测试程序，在JML中故意写错
public class Add {//@ requires a > 0;//@ requires b > 0;//@ ensures \result == a-b;public static int add(int a, int b) {return a + b;}public static void main(String args[]) {System.out.println(add(2, 3));}}
可以看到以及发现了我的错误——把加写错成了减。
三、JML UnitNG自动生成样例
OpenJML中带有jmluniting.jar文件，即可让我们使用JML UnitNG功能来进行自动生成样例测试。
使用
java -jar jmlunitng.jar xxxxx.javajavac -cp jmlunitng.jar *.javajava -jar openjml.jar -rac xxxx.javajava -cp jmlunitng.jar pare_JML_Test
即可得到相应的结果
这里自己新建一个简单的加法函数
public class Add {/*@ requires a > 0;@ requires b > 0;@ ensures \result == a+b;@*/public static int add(int a, int b) {return a + b;}public static void main(String args[]) {System.out.println(add(1, 2));}}
先用
java -jar jmlunitng.jar Add.java
得到以上文件，
接着用
javac -cp .\jmlunitng.jar *.java
编译出相应的class
使用
java -jar openjml.jar -rac Add.java
就能得到相应的JML_TEST程序文件
最后运行即可看到自动生成的样例以及给出的结果
原因显而易见，两个极限int数相加会造成int溢出。
四、本单元作业分析
架构设计与重构分析
第一次作业
第一次作业我们实现的只是简单的路径和容器，功能需求可以说非常简单。但是在复杂度方面我们还是需要权衡，三次作业都是如此。在第一次作业中我也有想到后面的发展走向，所以使用了多个Hashmap来优化查找操作，建立了
$$
边号<->次数、点号<->次数、路径<->路径编号
$$
之类的映射关系。将主要的复杂度集中在图结构变更指令中，每次变更图结构的同时刷新Hashmap。这样的架构在之后的两次作业都能得到沿用，不需要进行重构，只在必要时进行小范围修补即可。
类协作关系
方法复杂度统计
第二次作业
第二次作业相比于第一次作业增加了若干功能函数，新增了“边”的概念，同时引入连通性问题和最短路问题，在第一次代码的基础上，我只需要新增求解最短路问题的方法类即可。同时由于我们的点号是随机的，为了便于使用最短路算法，我增加了一个映射Hashmap，将所有点的点号按自然数从低到高排列映射。
在算法方面，我使用了Dijkstra算法，并使用了优先队列优化，相对于Floyed较高的复杂度，我在第三次作业中仍然可以直接沿用前面的算法，无需重构，没有爆TLE的风险。
类协作关系
方法复杂度统计
第三次作业
第三次作业在第二次作业上继续进行了功能性的扩充，增加了连通块以及最小换乘、最少不满意度、最低票价等等功能。但是除了连通块，其他几个功能本质上仍然是图的最短路的问题。
在处理连通块问题，这里使用了从网上学习到的非常巧妙的并查集思路。非常推荐这篇博客，同时也为自己的弱鸡算法能力感到羞愧。
最小换乘、最少不满意度、最低票价其实都是最短路的变种问题，几种问题都只需要在建立图的策略上下功夫，如果最短路算法复杂度不爆，完全可以不进行修改。这里使用的也是大家常用的拆点做法，给换乘车站在每条Path上都设一个“站台”。详细的过程可以参考zyy在讨论区里面的方法，我们没必要完全按照这个思路拆点，只需要理解拆点这个过程就可以自己设计代码。
类协作关系
方法复杂度统计
在这次作业中由于在图结构变更函数"add"、"remove"中包含了比较多的刷新Hashmap、建立图等操作，所以方法复杂度较高。
BUG分析与修复
第一次作业
第一次作业出现的bug非常非常非常傻，问题出在compareTo函数中，在比较字典序的过程中我选择直接拼接字符串来使用字符串的compare方法进行比较。导致强测被炸了五六个点，后面老老实实一个一个节点比较就没问题了 。（枯了555
第二次作业
第二次作业通过了所有中测以及强测测试点，互测中没有出现bug。
第三次作业
第三次作业通过了所有中测以及强测测试点。
但是在互测中被狼?人用50组ADD+120个节点+每个节点都有几十次换乘爆了数组越界错误。原因是在拆点时候我只开了4000个节点。
(大意了，心里想着50*80=4000就足够了)
被hack扣一分无伤大雅，但是以后还是要警醒，要么开大一点点数组，要么用可变长度。
五、单元学习体会
本单元任务相对于前两个单元较为轻松，除了引入了JML规格，在java实际的编码过程中其实都在做一个以前知识点的回顾。课下的三次作业，其实在脱离JML的情况下也可以正确的完成。我在阅读接口的JML遇到疑惑时，问我身边的很多同学，他们很多都表示压根没看JML直接开始编码。所以我觉得OO的JML系列作业可以设置更多坑点来促进我们在编码过程中结合JML思考问题。这样更能够让我们体会到JML契约式编程的好处。
所以我感觉相对于这几次作业，课上实验撰写JML规格也让人印象深刻。新入坑JML，感觉JML很多时候写起来难度比正式编码还要大。而且从搜索引擎查找到的资料来看，JML的中文资料是非常匮乏的，我们还需要勤于收集资料才能进一步加深对JML的学习。
另外这单元的三次作业仍然是递增迭代的过程，这也是每个单元作业的共同特征。相较于以前单元的次次作业重构，现在写作业已经可以偷不少懒了，感谢OO这学期给我们带来的进步。
还剩最后一个单元，我们一起征服。
