清河网站建设多少钱,会计网站建设,网站开发敲代码,免费注册个人个人网站目录 JML语言学习笔记理论基础应用工具链情况JMLUnit/JMLUnitNGUNIT3 作业分析作业 3-1 实现两个容器类Path和PathContainer作业 3-2 实现容器类Path和数据结构类Graph作业 3-3 实现容器类Path#xff0c;地铁系统类RailwaySystem规格撰写的心得与体会最后#xff0c;衷心感谢… 目录 JML语言学习笔记理论基础应用工具链情况JMLUnit/JMLUnitNGUNIT3 作业分析作业 3-1 实现两个容器类Path和PathContainer作业 3-2 实现容器类Path和数据结构类Graph作业 3-3 实现容器类Path地铁系统类RailwaySystem规格撰写的心得与体会最后衷心感谢为这门课程辛苦付出的老师和助教。??? JML语言学习笔记 理论基础 1. 注释结构 2. JML表达式 原子表达式量化表达式集合表达式操作符etc.3. 方法规格 前置条件(pre-condition)后置条件(post-condition)副作用范围限定(side-effects)4. 类型规格 不变式(invariant)状态变化约束(constraint)应用工具链情况 1. OpenJML SMT Solver 首先由OpenJML将JML规格转换乘SMT-LIB格式的代码然后调用SMT solver进行检查。用于静态检查。2. JMLUnitNG 根据规格自动生成测试文件。用于自动测试。3. JMLdoc 可以快速生成JML文档的相关文件4. Junit Junit主要用于单元化测试与一定的自动化测试配合JML食用效果极佳。JMLUnit/JMLUnitNG 1. 前期准备 简单代码示例与jar包配置 2. 命令行操作 java -jar jmlunitng.jar src/Demo.java
javac -cp jmlunitng.jar src/*.java 3. 测试结果 4. 结果分析 我们可以看出自动生成的测试样例对各种极端情况进行了测试具有较好的覆盖性。但是在试验过程中JML测试的局限性也被暴露出来了。UNIT3 作业分析 作业 3-1 实现两个容器类Path和PathContainer 1. 架构设计 1度量分析 2结构分析 3算法分析 MyPath // path的存储结构用来顺序存储结点
private ArrayListInteger arrayNodes;
// 用来存储一条path中的node的个数无重复。key结点名称value该结点出现的次数
private HashMapInteger, Integer hashNodes; ADD
1读入一个结点数组
2将结点顺序存入arrayNodes
3遍历结点数组对于任一结点node若node不在hashNodes中即存入(node, 1)若已存在即存入(node, value 1)。MyPathContainer private int id 0; // pathID
private HashMapPath, Integer hashPaths; // Path -- PathID
private HashMapInteger, Path hashIds; // PathID -- Path
private HashMapInteger, Integer nodes; // Node -- frequentNumberADD:
原理与path相同REMOVE
1hashIds.remove(pathID)hashPaths.remove(path)
2对于path中的每一个node设node的出现次数为frequentNumber若frequentNumber1则将node从nodes中移除若frequentNumber1则 nodes.replace(node, frequentNumber-1)。2. BUG分析 1bug情况 由于测试数据量的限制程序在评测与互测环节没有出现错误。2修复情况 该程序存在一些不优美的地方如MyPath中利用HashMap来存储不同结点是复杂的可以说是自己造了个轮子改正方法为使用HashSet进行存储通过容器的特性来减少手动判断。作业 3-2 实现容器类Path和数据结构类Graph 1. 架构设计 1度量分析 2结构分析 3算法分析 AlGraph // alGraph: node1 -- (node2 - node2_frequentNumber)
private HashMapInteger, HashMapInteger, Integer alGraph;
// edges: node1 -- (node2 - shortestPathLength_From_Node1_To_Node2)
private HashMapInteger, HashMapInteger, Integer edges; // 由原始图alGraph生成距离图edges的算法 ———— Floyd算法
for (k 0; k MAX; k) for (i 0; i MAX; i) for (j 0; j MAX; j) if (Graph[i][j] Graph[i][k] Graph[k][j]) Graph[i][j] Graph[i][k] Graph[k][j];
public boolean containsEdge(int node1, int node2) {return alGraph.get(node1).containsKey(node2);
}
public boolean isConnected(int node1, int node2) {if (node1 node2) return true;else return edges.get(node1).containsKey(node2);
}
public int getShortestPathLength(int node1, int node2) {if (node1 node2) return 0;else return edges.get(node1).get(node2);
}4迭代中对架构的重构 AlGraph继承了上一次作业中的PathContainer并进行了适当的扩充具体扩充见如上算法分析。2. BUG分析 1bug情况 测试数据量增大时程序出现 CPU_TIME_LIMIT_EXCEED 的错误。原因据我分析在Floyd算法中加入的大量的判断当数据量增大时造成CPU的负担过大运算超时。2修复情况 重构后UML图 算法分析 private final int biggest 999999999; // 极大数自由定义小于2^31即可
private int id 0; // PathID同上一次作业
private HashMapPath, Integer pathToId; // Path -- PathID同上一次作业
private HashMapInteger, Path idToPath; // PathID -- Path同上一次作业
private HashMapInteger, Integer nodeToSum; // Node -- Node_Sum同上一次作业
private HashMapInteger, Integer nodeToIndex; // Node -- Node_index_in_matrix
private HashSetInteger[] adjVexSets; // 临界表Node--Set{node1, node2, ...}
private int[][] disMatrix; // Graph生成的存储各点之间距离的距离矩阵
private StackInteger indexStack; // 用来维护node-index的映射的栈映射关系建立机制搭建点与数组下标的关系
if put_New_Node_Into_Graph then bond_NewNode_to_IndexStack.pop()
else if remove_Node_From_Graph then indexStack.push(oldNode.index)3前后对比 // 原程序floyd部分代码
for (int k : tempEdges.keySet()) for (int i : tempEdges.keySet()) for (int j : tempEdges.keySet()) if (tempEdges.get(i).containsKey(k) tempEdges.get(k).containsKey(j)) { int via tempEdges.get(i).get(k) tempEdges.get(k).get(j);if (tempEdges.get(i).containsKey(j)) {if (tempEdges.get(i).get(j) via) {tempEdges.get(i).replace(j, via);}} else {tempEdges.get(i).put(j, via);}}// 重构后floyd部分代码
for (int k 0; k 255; k) for (int i 0; i 255; i) for (int j 0; j 255; j) if (disMatrix[i][j] (newDis disMatrix[i][k] disMatrix[k][j])) disMatrix[i][j] newDis;作业 3-3 实现容器类Path地铁系统类RailwaySystem 1. 架构设计 1度量分析 2结构分析 3算法分析 MyRailwaySystem private int cbCount 0; // 连通块个数
private int[][] disMatrix; // 距离矩阵
private int[][] transferMatrix; // 最小换乘矩阵
private int[][] priceMatrix; // 价格矩阵
private int[][] happyMatrix; // 最低不满意度矩阵// 下面是算法的伪代码以价格矩阵的更新为例其它类似
private void updatePriceMatrix() {priceMatrix initMatrix(2);for (Each path : paths) {maxSize path.size();priceArray ((MyPath)path).getPriceArray();nodeMap ((MyPath)path).getNodeMap();for (Each node1, node2 : nodeMap)if (priceArray[tempId1][tempId2] 2 priceMatrix[index1][index2]) priceMatrix[index1][index2] priceMatrix[index2][index1] priceArray[tempId2][tempId1] 2;}floyd(priceMatrix, 125);
}4迭代中对架构的重构 MyPath 在MyPath添加了两个距离矩阵用来存储一个Path地铁线路内部的加权距离信息。首先将Path构建成两个加权无向图权值分别为价格和满意度然后通过Floyd算法生成各自的距离矩阵存储下来。private int[][] priceArray; // 加权价钱距离矩阵
private int[][] happyArray; // 加权满意度距离矩阵
// 以下是算法的伪代码
private void updateMatrix() {setNodeMap(); // 重新建立映射关系priceArray initMatrix(nodeCount, 2); // 距离矩阵初始化happyArray initMatrix(nodeCount, 32); // 距离矩阵初始化for (Each node1, node2 nodes) { // 建图赋权priceArray[node1.index][node2.index] priceArray[node2.index][node1.index] 1;happyArray[node1.index][node2.index] happyArray[node2.index][node1.index] CalculatePleasure();}floyd(priceArray); floyd(happyArray); // 计算各点之间距离
}2. BUG分析 1bug情况 这种算法在测试数据最多结点数以及最多图变动指令数有所约束时展现出非常出色的性能。在强测与互测中均未出现错误。但是我的代码结构有着较为严重的问题几乎完全面向过程的写法严重违反了OOP的原则多个相似结构重复计算等。2修复情况 尚未进行代码重构仅对课程组给出的标程进行了研究并进行了简单的算法优化尝试。规格撰写的心得与体会 规格化设计和契约式编程让人如沐清风受益匪浅。 其实这次的代码工程量很大但是由于课程组给出的JML的引导以及课程组已经将我们需要填写的代码抽象成了接口这使得我们在写代码时会产生一种错觉——“这是面向对象课程吗”、“这是数据结构补习课吧”…… 这正是规格化设计和契约式编程 的巨大作用。JML语言——好用不好写。 JML语言书写的困难度过高从课程组编写JML出现的各种状况可以看出给我的感觉是“可远观而不可亵玩”。而且由于DDL过多加上学习资料不足网上、课程资料都几乎为零我缺乏自己动手写JML的动力。没有指引路程变成了痛苦的过程。也许是因为JML这一课还在探索阶段课程对JML编写、检测、使用的工具的讲解和介绍颇少基本全靠讨论区和大佬们的指点自己摸索着完成任务。固然可以说这是对我们自主学习能力的养成但是有必要吗我相信JML单元会一步步从碎片化走向体系化更加容易上手。在路上 ……最后衷心感谢为这门课程辛苦付出的老师和助教。???转载于:https://www.cnblogs.com/FUJI-Mount/p/10905195.html
