第三单元——jml、junit与图
〇、问题描述
本单元主题为JML的学习，问题载体为一个无向图路径管理系统。在三次作业种，情景不变，需求递增。因此需要在层次上做好安排。
一、JML语言
理论基础(Level 0)
-
注释结构
// @annotation行注释/* @annotation*/块注释 -
JML表达式
-
原子表达式
esult方法执行后的返回值old(expr)表达式expr在方法执行前的值ot_assigned(expr)表达式expr是否被赋值ot_modified(x,y,...)表达式expr是否变化onnullelements( container )表达式：表示container对象中存储的对象不会有 nullype(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给定范围内的表达式的最大/小值um_of指定变量中满足相应条件的取值个数 -
集合表达式
-
操作符
<:子类型关系操作符<==><=!=>等价关系操作符==><==推理操作符othingeverything变量引用操作符
-
-
方法规格
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
esult == 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*/ @Override public 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仍仅仅停留在了解阶段，还需要更多的学习。毕竟，第三单元的作业架构严格来说几乎没有自己参与……由此也可见得架构对于程序正确性、效率和可扩展性的重要性。