目录
- 第三单元——
jml、junit与图
第三单元——jml、junit与图
〇、问题描述
本单元主题为JML的学习，问题载体为一个无向图路径管理系统。在三次作业种，情景不变，需求递增。因此需要在层次上做好安排。
一、JML语言
理论基础(Level 0)
注释结构
// @annotation行注释/* @annotation*/块注释JML表达式
原子表达式
\result方法执行后的返回值\old(expr)表达式expr在方法执行前的值\not_assigned(expr)表达式expr是否被赋值\not_modified(x,y,...)表达式expr是否变化\nonnullelements( container )表达式：表示container对象中存储的对象不会有 null\type(type)表达式：返回类型type对应的类型(Class)量化表达式
\forall全称修饰(\forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j])\exists存在修饰(\exists int i; 0 <= i && i < 10; a[i] < 0)\sum给定范围内的表达式的和(\sum int i; 0 <= i && i < 5; i)\product给定范围内的表达式的连乘结果\maxmin给定范围内的表达式的最大/小值\num_of指定变量中满足相应条件的取值个数集合表达式
操作符
<:子类型关系操作符<==><=!=>等价关系操作符==><==推理操作符\nothing\everything变量引用操作符
方法规格
requires前置条件ensures后置条件assignable可赋值modifiable可修改public normal_behavior正常功能signals抛出异常类型规格
invariant不变式constraint状态变化约束
应用工具链
lowa State JML ： 提供了一个断言检查编译器jmlc，将JML注释转换为运行时的断言；
jmldoc： 文档生成器，用于生成Javadoc文档，增加了来自JML注释的额外信息。
jmlunit： 单元测试生成器可以从JML注释中生成JUnit测试代码。
二、JMLUnitNG/JMLUnit
public class Demo {/*@ public normal_behaviour@ ensures \result == a + b;@*/public static int add(int a, int b) {return a + b;}public static void main(String[] args) {add(12,3);}
}[TestNG] Running:
Command line suite
Passed: racEnabled()
Passed: constructor Demo()
Passed: static add(-2147483648, -2147483648)
Passed: static add(0, -2147483648)
Passed: static add(2147483647, -2147483648)
Passed: static add(-2147483648, 0)
Passed: static add(0, 0)
Passed: static add(2147483647, 0)
Passed: static add(-2147483648, 2147483647)
Passed: static add(0, 2147483647)
Passed: static add(2147483647, 2147483647)
Passed: static main(null)
Passed: static main({})
===============================================
Command line suite
Total tests run: 13, Failures: 0, Skips: 0
===============================================
三、程序设计
类的设计——继承与递进
简析三次作业涉及到的指令及实现方式：
第一次：
HashMap管理路径// 两个对应的 HashMap 存储，加快查找 private HashMap<Integer/*id*/,MyPath/*path*/> pathList; private HashMap<MyPath/*path*/,Integer/*id*/> pidList; // 在添加和删除时管理总点数，分摊复杂度 private HashMap<Integer/*node*/,NumberOfNode/*number of node*/> distinct;// hashcode的设定 /*path*/ @Overridepublic int hashCode() {return nodes.hashCode();} /*integer*/Integer.hashCode();添加删除类
O(n)在两个表中添加/删除路径；管理节点数目。包括：
- 添加路径
- 删除路径
- 根据id删除
查询类
O(1)包括：
- 查询id
- 查询路径
- 获取总路径数
- 根据id获取路径大小
- 根据结点序列判断容器是否包含路径
- 根据路径id判断容器是否包含路径
- 容器内不同结点个数
- 路径中是否包含某个结点
根据id获取不同节点个数
O(n)path内排序+遍历第一次为O(n)，其后为O(1)
根据字典序比较两个路径的大小关系
O(n)
第二次：
HashMap存储邻接表管理无向图// 邻接表：边权均为1的无向图 private HashMap<Integer/*起点*/,HashMap<Integer/*终点*/,Integer/*边数*/>> reachable= new HashMap<>();边的存在性
O(1)bfs搜索O(v+e)包括：
两个结点是否连通
最短路径存在
两个结点之间的最短路径
第三次：
UndirectedGraph含有图的嵌套关系；图的连接状态相同但边权不同。新增一类专门管理。
abstract class UndirectedGraph {// 无向图private HashMap<Integer/*point*/,HashMap<Integer/*point*/,Integer/*weight*/>> undirectedGraph;// 缓存区private HashMap<Integer/*point*/,HashMap<Integer/*point*/,Integer/*weight*/>> cache;private bfs(){}private spfa(){}... }以下复杂度讨论均不考虑缓存查找。（重复查询时
O(1)）连通块数量
涂色
spfa本质上都是带权最短路径的问题。。。以前的沙雕方法都重写了。
- 最低票价
- 最少换乘次数
- 最少不满意度
- 最短路径
- 两点连通性
三次架构
- 第一次：哈希表+规格方法
- 第二次：添加可达表，原有方法不变
- 第三次：添加图，重写查找算法相关方法
算法
第二次：bfs
第三次：每条path内部先构建好小图，即建立好所有的边，这样在每一条边上加上换乘权值，搜最短路 (
spfa) 就行。共需三个权值不同的图。因为查询指令较多，应每次搜索都将当前起点的所有终点最短路都放入缓存。每当图结构更改应该清空缓存。
四、BUG分析
（本地bug）写第三次作业时，bfs写成找到目标终点即停止：
while (size != 0) {if(fr==to) return;//...for (Integer x : keySet()) {//...}
} 导致第二次搜索时进行不下去。应改成一次性搜索完所有终点。
五、心得体会
对于jml，语法是相对简单，理解也相对容易。难点在于自己写出一份规范的规格。因为写规格的成本比写代码高出太多，我对jml仍仅仅停留在了解阶段，还需要更多的学习。毕竟，第三单元的作业架构严格来说几乎没有自己参与……由此也可见得架构对于程序正确性、效率和可扩展性的重要性。
)
)
——使用注解标注监听器(Listener))
)
 培训总结)
