OO第三单元总结：JML

第三单元——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 给定范围内的表达式的连乘结果
  
  \max min 给定范围内的表达式的最大/小值
  
  \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仍仅仅停留在了解阶段，还需要更多的学习。毕竟，第三单元的作业架构严格来说几乎没有自己参与……由此也可见得架构对于程序正确性、效率和可扩展性的重要性。

转载于:https://www.cnblogs.com/DilemmaR/p/10908548.html