做网站要学会那些,成都品牌logo设计公司,石家庄专业制作网站,wordpress 付费主题目录 第三单元——jml、junit与图第三单元——jml、junit与图 〇、问题描述 本单元主题为JML的学习#xff0c;问题载体为一个无向图路径管理系统。在三次作业种#xff0c;情景不变#xff0c;需求递增。因此需要在层次上做好安排。 一、JML语言 理论基础(Level 0) 注释… 目录 第三单元——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 HashMapInteger/*id*/,MyPath/*path*/ pathList;
private HashMapMyPath/*path*/,Integer/*id*/ pidList;
// 在添加和删除时管理总点数分摊复杂度
private HashMapInteger/*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 HashMapInteger/*起点*/,HashMapInteger/*终点*/,Integer/*边数*/ reachable new HashMap(); 边的存在性 O(1)bfs 搜索 O(ve) 包括 两个结点是否连通 最短路径存在两个结点之间的最短路径第三次UndirectedGraph 含有图的嵌套关系图的连接状态相同但边权不同。新增一类专门管理。 abstract class UndirectedGraph {// 无向图private HashMapInteger/*point*/,HashMapInteger/*point*/,Integer/*weight*/ undirectedGraph;// 缓存区private HashMapInteger/*point*/,HashMapInteger/*point*/,Integer/*weight*/ cache;private bfs(){}private spfa(){}...
} 以下复杂度讨论均不考虑缓存查找。重复查询时O(1) 连通块数量 涂色spfa 本质上都是带权最短路径的问题。。。以前的沙雕方法都重写了。 最低票价最少换乘次数最少不满意度最短路径两点连通性三次架构 第一次哈希表规格方法第二次添加可达表原有方法不变第三次添加图重写查找算法相关方法算法 第二次bfs第三次每条path内部先构建好小图即建立好所有的边这样在每一条边上加上换乘权值搜最短路 ( spfa ) 就行。共需三个权值不同的图。 因为查询指令较多应每次搜索都将当前起点的所有终点最短路都放入缓存。每当图结构更改应该清空缓存。四、BUG分析 本地bug写第三次作业时bfs写成找到目标终点即停止 while (size ! 0) {if(frto) return;//...for (Integer x : keySet()) {//...}
} 导致第二次搜索时进行不下去。应改成一次性搜索完所有终点。 五、心得体会 对于jml语法是相对简单理解也相对容易。难点在于自己写出一份规范的规格。因为写规格的成本比写代码高出太多我对jml仍仅仅停留在了解阶段还需要更多的学习。毕竟第三单元的作业架构严格来说几乎没有自己参与……由此也可见得架构对于程序正确性、效率和可扩展性的重要性。转载于:https://www.cnblogs.com/DilemmaR/p/10908548.html
