1 梳理JML语言的理论基础、应用工具链情况
由于篇幅原因，这里只梳理几个在本单元常用的
注释结构
-
行注释:
//@annotation -
块注释：
/* @ annotation @*/例如：纯粹查询方法
/*@ pure @ */，即方法的执行不会有任何副作用
JML表达式
原子表达式
-
\result：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值
-
\old(expr): 用来表示一个表达式 expr 在相应方法执行前的取值。作为一般规则，任何情况下，都应该使用\old把关心的表达式取值整体括起来。
量化表达式
-
\forall：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
作业中的例子：
1 (\forall int i; 0 <= i && (i < npath.length - 1); containsEdge(npath[i], npath[i + 1])));
保证isConnected 的前提之一是，这两个点之间有连续的边将他们相连（否则不通）
-
\exist：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束
作业中的例子：
1 requires (\exists Path path; path.isValid() && containsPath(path); path.containsNode(fromNodeId)) && 2 (\exists Path path; path.isValid() && containsPath(path); path.containsNode(toNodeId));
保证isConnected 的前提之一，要存在某个Path，这个Path上包含这个点（否则就Not Found Exception）
操作符
-
子类型关系操作符: E1<:E2
-
等价关系操作符:
b_expr1<==>b_expr2或者b_expr1<=!=>b_expr2 -
推理操作符:
b_expr1==>b_expr2或者b_expr2<==b_expr1。对于表达式b_expr1==>b_expr2而言，当b_expr1==false，或者b_expr1==true且b_expr2==true时，整个表达式的值为 true 。 -
变量引用操作符
-
\nothing指示一个空集:
例如：
assignable \nothing表示当前作用域下每个变量都不可以在方法执行过程中被赋值 -
\everything指示一个全集
-
方法规格
正常行为规格normal_behavior
前置条件
-
通过requires子句来表示
-
例如增加一条路径的前提条件：增加的这条路径必须合法有效
1 requires path != null && path.isValid();
-
后置条件
-
通过ensures子句来表示
-
getPathId必须确保返回的ID确实属于当前存在的路径
-
1 ensures (\exists int i; 0 <= i && i < pList.length; pList[i].equals(path) && pidList[i] == \result);
-
副作用
-
使用关键词 assignable 或者 modifiable，这个函数要改什么变量，就在后面加那个变量的名字
-
例如addPath
1 /*@ normal_behavior 2 @ requires path != null && path.isValid(); 3 @ assignable pList, pidList; 需要修改这两个List 4 省略一部分 5 @ also 6 省略一部分 7 @ assignable \nothing; 如果Path不合法，那么返回0，没有需要修改的东西 8 @ ensures \result == 0; 9 @*/ 10 public int addPath(Path path);
-
异常行为规格expcetional_behavior
-
also: 有两种场景使用
-
除了正常功能规格外，还有一个异常功能规格，需要使用also来分隔。
-
父类中对相应方法定义了规格，子类重写了该方法，需要补充规格，这时应该在补充的规格之前使用also;
-
-
signals子句
-
结构为signals (***Exception e) b_expr，意思是当b_expr为true时，方法会抛出括号中给出 的相应异常e。
例子：
1 /*@ public normal_behavior 2 省略 3 @ also 下面是异常行为 4 @ public exceptional_behavior 5 @ assignable \nothing; 6 @ signals (PathNotFoundException e) path == null; 7 @ signals (PathNotFoundException e) path.isValid() == false; 8 @ signals (PathNotFoundException e) !containsPath(path); 9 @*/ 10 public int removePath(Path path) throws PathNotFoundException;
-
当 path == null条件成立，抛出异常
-
当 path.isValid条件成立，抛出异常
-
当容器内不含 path，抛出异常
-
-
在线OpenJML链接
2 部署SMT Solver，至少选择3个主要方法来尝试进行验证，报告结果
跳过
3 部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例， 并结合规格对生成的测试用例和数据进行简要分析
生成数据
我研究了好久貌似OpenJML对MacOS不是很友好……好像也没有搞清楚TestNG怎么生成测试样例
写了一个python程序来生成测试指令
1 import random 2 SEQUENCE = 0; 3 ID = 1; 4 DOUBLE_ID = 2; 5 NONE = 3; 6 ID_NODE = 4; 7 queries = [("PATH_ADD", SEQUENCE), 8 ("PATH_REMOVE", SEQUENCE), 9 ("PATH_REMOVE_BY_ID", ID), 10 ("PATH_GET_ID", SEQUENCE), 11 ("PATH_GET_BY_ID", ID), 12 ("PATH_COUNT", NONE), 13 ("PATH_SIZE", ID), 14 ("PATH_DISTINCT_NODE_COUNT", ID), 15 ("CONTAINS_PATH", SEQUENCE), 16 ("CONTAINS_PATH_ID", ID), 17 ("DISTINCT_NODE_COUNT", NONE), 18 ("COMPARE_PATHS", DOUBLE_ID), 19 ("PATH_CONTAINS_NODE", ID_NODE) 20 ] 21 22 NUMBER = 100 23 PATH_LENGTH = 500 24 query_count = len(queries) 25 path_count = 0 26 27 28 def gen_node(): 29 """generate random node""" 30 return random.randint(-2**31, 2**31 -1) 31 32 def gen_none(): 33 """""" 34 return [] 35 36 def gen_sequence(): 37 """generate id sequence""" 38 len = random.randint(2, PATH_LENGTH) 39 sequence = [] 40 41 for i in range(len): 42 sequence.append(gen_node()) 43 44 path_count + 1; 45 return sequence 46 47 def gen_id(): 48 """generate id""" 49 return [random.randint(1, path_count * 2 + 1)] 50 51 def gen_doubel_id(): 52 """generate two ids""" 53 return [random.randint(1, path_count + 1), random.randint(1, path_count + 1)] 54 55 def gen_id_node(): 56 return [random.randint(1, path_count + 1), gen_node()] 57 58 # print(gen_sequence()) 59 60 generators = {SEQUENCE : gen_sequence, 61 ID: gen_id, 62 DOUBLE_ID: gen_doubel_id, 63 NONE: gen_none, 64 ID_NODE: gen_id_node } 65 66 for i in range(13): 67 (op, arg) = queries[0] 68 print(op + ‘ ‘ + ‘ ‘.join(map(lambda x: str(x), generators[arg]()))) 69 for i in range(NUMBER): 70 (op, arg) = queries[random.randint(0, query_count - 1)] 71 print(op + ‘ ‘ + ‘ ‘.join(map(lambda x: str(x), generators[arg]())))
IDEA TestMe插件和 TestNG和OpenJML的安装历程
-
安装TestMe插件，可以直接在Plugin 的Market里面下载，TestNG失败
-
下载TestNG
(TestNG下载及安装教程链接)
（TestNG6.8.7JAR包的下载链接）
Build TestNG from source code
TestNG is also hosted on GitHub, where you can download the source and build the distribution yourself:
然后把Jar包导入新创建的Maven项目当中，课程组的Jar包导入项目当中
在右侧边栏的Maven，点击加号，把课程组给的pom.xml导入
后来弄出了形如这样的一堆令人头疼的代码，遂放弃
1 @Test 2 public void testGetConnectedBlockCount() { 3 when(bfs.getBlockSize()).thenReturn(0); 4 when(bfs.updateGraph(any())).thenReturn(new HashMap<Integer, HashMap<Integer, Integer>>() {{ 5 put(Integer.valueOf(0), new HashMap<Integer, Integer>() {{ 6 put(Integer.valueOf(0), Integer.valueOf(0)); 7 }}); 8 }}); 9 10 int result = myRailwaySystem.getConnectedBlockCount(); 11 Assert.assertEquals(result, 0); 12 }
（错误示范）
正确使用OpenJML
在许多大佬的帖子中已经把如何生成测试代码讲得很清楚了
示例主程序在Demo.java里面
java -jar jmlunitng.jar src/Demo.java javac -cp jmlunitng.jar src/*.java
然后会出现很多名字奇怪的.java文件，其中有一个叫Demo_JML_Test.java，也就是测试时要运行的主程序
我把生成的.java测试文件都加入到IDEA工程的src文件夹下面，需要导入的包有openjml.jar，jmlunitng.jar
但是我在运行Demo_JML_Test的时候有一些奇怪的报错 “org.jmlspecs.utils.JmlAssertionError 中是 protected访问控制”
于是把报错代码Catch 的 Exception删了
在艰苦卓绝的研究下，和修改了一堆版本不兼容的问题后，测试代码终于运行成功了！
（racEnabled尚未解决）
Junit 测试代码
创建单元测试可以直接在IDEA里面自动生成一个测试代码的框架
Junit中集中基本注解，是必须掌握的：
-
@BeforeClass – 表示在类中的任意public static void方法执行之前执行
-
@AfterClass – 表示在类中的任意public static void方法执行之后执行
-
@Before – 表示在任意使用@Test注解标注的public void方法执行之前执行
-
@After – 表示在任意使用@Test注解标注的public void方法执行之后执行
-
@Test – 使用该注解标注的public void方法会表示为一个测试方法
junit中的assert方法全部放在Assert类中，总结一下junit类中assert方法的分类。
Junit中部分Assert方法总结：（来自这个博客）
-
assertTrue/False([String message,]boolean condition); 判断一个条件是true还是false。感觉这个最好用了，不用记下来那么多的方法名。
-
fail([String message,]); 失败，可以有消息，也可以没有消息。
-
assertEquals([String message,]Object expected,Object actual); 判断是否相等，可以指定输出错误信息。 第一个参数是期望值，第二个参数是实际的值。 这个方法对各个变量有多种实现。在JDK1.5中基本一样。 但是需要主意的是float和double最后面多一个delta的值。
-
assertNotEquals([String message,]Object expected,Object actual); 判断是否不相等。 第一个参数是期望值，第二个参数是实际的值。
-
assertArrayEquals([java.lang.String message,] java.lang.Object[] expecteds, java.lang.Object[] actuals) ;
-
assertNotNull/Null([String message,]Object obj); 判读一个对象是否非空(非空)。
-
assertSame/NotSame([String message,]Object expected,Object actual); 判断两个对象是否指向同一个对象。看内存地址。
-
failNotSame/failNotEquals(String message, Object expected, Object actual) 当不指向同一个内存地址或者不相等的时候，输出错误信息。 注意信息是必须的，而且这个输出是格式化过的。
下面仅写出部分函数的测试代码
1 public class MyGraphTest { 2 MyGraph graph = new MyGraph(); 3 int[] nodelist1 = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 13}; 4 int[] nodelist2 = {-1, 6, -2, -3, -4, -5, -6, -7, -8}; 5 int[] nodelist3 = {0,1205, 999, 888, 777, 666}; 6 @Before 7 public void before() throws Exception { // 每个方法检测之前，都另这个图里面有这三条路径 8 System.out.println("Ready to test " ); 9 //MyGraph graph = new MyGraph(); 10 graph.addPath(new MyPath(nodelist1)); 11 graph.addPath(new MyPath(nodelist2)); 12 graph.addPath(new MyPath(nodelist3)); 13 } 14 15 @After 16 public void after() throws Exception { // 每个函数检测完毕都会输出“test successfully!” 17 System.out.println("test successfully!"); 18 } 19 20 @Test 21 public void testContainsPath() throws Exception { 22 //TODO: Test goes here... 23 System.out.println("Testing ContainsPath!"); 24 Assert.assertTrue(graph.containsPath(new MyPath(nodelist1))); 25 Assert.assertTrue(graph.containsPath(new MyPath(nodelist2))); 26 Assert.assertTrue(graph.containsPath(new MyPath(nodelist3))); 27 int[] nodelist4 = {9,9,9,9}; 28 Assert.assertFalse(graph.containsPath(new MyPath(nodelist4))); 29 } 30 31 @Test 32 public void testContainsPathId() throws Exception { 33 System.out.println("Testing contains Path id!"); 34 Assert.assertTrue(graph.containsPathId(1)); 35 Assert.assertTrue(graph.containsPathId(2)); 36 Assert.assertTrue(graph.containsPathId(3)); 37 Assert.assertFalse(graph.containsPathId(100)); 38 } 39 40 41 @Test 42 public void testRemovePath() throws Exception { 43 //TODO: Test goes here... 44 graph.removePath(new MyPath(nodelist1)); 45 Assert.assertFalse(graph.containsPathId(1)); 46 } 47 48 @Test 49 public void testRemovePathById() throws Exception { 50 //TODO: Test goes here... 51 graph.removePathById(2); 52 Assert.assertFalse(graph.containsPath(new MyPath(nodelist2))); 53 } 54 55 @Test 56 public void testContainsNode() throws Exception { 57 //TODO: Test goes here... 58 Assert.assertTrue(graph.containsNode(999)); 59 Assert.assertFalse(graph.containsNode(14)); 60 61 62 @Test 63 public void testIsConnected() throws Exception { 64 //TODO: Test goes here... 65 System.out.println("Testing is [email protected]"); 66 Assert.assertTrue(graph.isConnected(2,-8)); // 判断这个连接是对的 67 Assert.assertTrue(graph.isConnected(13,-8)); 68 Assert.assertFalse(graph.isConnected(0, 1)); 69 // 把这个文件拖到src文件夹里面即可运行 70 71 } 72 73 }
愉快的Tests passed! ??
4 按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构
第一次作业
第一次作业比较简洁，接口已经提供好了（超级良心），实现函数的需求即可。
需要重视的几个需求：
根据ID获得路径&根据路径获得ID：
-
构造两个HashMap，key 和 value 反向存储一次，一个是<id, path>，一个是<path, id>，这个构造可以解决大多数基本需求
-
注意自己写的类，需要重写equals()方法和 hashCode()方法，不重写的话，每次判断路径都是不一样的
Object类默认的equals比较规则就是比较两个对象的内存地址。而hashCode是本地方法，java的内存是安全的，因此无法根据散列码得到对象的内存地址，但实际上，hashcode是根据对象的内存地址经哈希算法得来的。
-
1 private HashMap<Integer, Path> container; // 用来装路径的<ID, path> 2 private HashMap<Path, Integer> reverseContainer; 3 // 下面是重写的方法 4 @Override 5 public boolean equals(Object obj) { 6 if (path == null || !(obj instanceof Path)) { 7 return false; 8 } 9 // obj instanceof Path 10 Path path = (Path) obj; 11 if (this.size != path.size()) { 12 return false; 13 } 14 int min = Math.min(this.size, path.size()); 15 //Iterator iter = this.iterator(); 16 for (int i = 0; i < min; i++) { // 一个个比较节点， 17 if (this.getNode(i) != path.getNode(i)) { 18 return false; 19 } 20 } // 如果所有节点都完全相同，那么这两个路径就是等价的 21 return true; 22 } 23 24 @Override 25 public int hashCode() { 26 int result; 27 // 至少两个节点，所以可以利用第二个，减少哈希冲突 28 result = this.size() * this.getNode(0) * this.getNode(1); 29 return result; 30 }
容器内不同节点个数
-
由于哈希表速度快，查找方便，键-值一一对应，故也选用哈希表
-
1 private HashMap<Integer, Integer> distinctCount; // <nodenum, 该点出现次数>
比较两个路径大小关系
-
节点逐个比较即可，有个小坑，返回值要严格大于/小于/等于0，所以我就没有用x-y的形式
1 @Override 2 public int compareTo(Path o) { 3 int min = Math.min(o.size(), this.size); 4 for (int i = 0; i < min; i++) { 5 if (this.getNode(i) == o.getNode(i)) { 6 continue; 7 } 8 else if (this.getNode(i) < o.getNode(i)) { 9 return -1; 10 } 11 else if (this.getNode(i) > o.getNode(i)) { 12 return 1; 13 } 14 } 15 // 一路上都一样大 16 if (this.size > o.size()) { 17 return 1; 18 } else if (this.size == o.size()) { //if () 19 return 0; 20 } else { 21 return -1; 22 } 23 }
第二次作业
第二次作业在第一次的基础上，将PathContainer升级成为了Graph类，不再是简单的“路径存储管理器”，而变成了一个无权无向图。
通过分析新增需求，我对架构做出了如下调整：
容器中是否存在某个结点：
-
直接把上次维护的distinctCount这个HashMap拿来用，containsKey即可
是否存在某一条边 & 结点是否连通 & 结点间最短路径
出于速度的考虑，我维护了两个HashMap套HashMap的结构
-
一个是“种子”，仅仅记录<nodeid1, <nodeid2, 这两个点构成的边出现的次数>>，在增删时维护很方便
-
一个是通过“种子”生成的“图”，<nodeid1, <nodeid2, 这两个点的最短距离>>，查询时直接返回
-
注意nodeid2是与id1连接的所有点，一个nodeid1可对应很多邻接点nodeid2，也就是一个结点一张表
1 // 维护Edge的第一个HashMap，一个结点对应直接连接的邻接点，增删时维护 2 // 维护邻接点（一个边）的信息， 3 private HashMap<Integer, HashMap<Integer, Integer>> edgeCount; // 种子 4 5 // 维护Edge的第二个HashMap, 存储两个间接连接的Node之间最短路径长度, 查询时维护 6 private HashMap<Integer, HashMap<Integer, Integer>> connectedMap; // 图
那么，如何由“种子”生成“图”呢？我考虑了不同方法找最短路径，最终选择了BFS广搜
新建一个Bfs类，里面只有两个函数：
1 public HashMap<Integer, Integer> PerformBfs(int startNode, 2 HashMap<Integer, HashMap<Integer, Integer>> edgeCountGraph) 3 // 这个传进去的参数 edgeCountGraph 就是上面维护的“种子”
-
PerformBfs用于单次广搜，找出从startNode起点出发，所可以到达的所有点的最短路径
-
由于BFS算法的特性，一旦到达某个点，那么所经过的路径一定是最短的，直接存到一个HashMap即可。
PerformBfs返回的HashMap就是我第二个大“图”所用的内层HashMap
存的键-值是 <startNode可达点ID，startNode到该点路径>
1 public HashMap<Integer, HashMap<Integer, Integer>> 2 updateGraph(HashMap<Integer, HashMap<Integer, Integer>> edgeCountGraph)
-
updateGraph通过调用N次（N是容器内不同点个数）PerformBfs，遍历edgeCountGraph，把每个点到它所有可达点都算一遍，并存下最短路径值（其实也是双向存储），这样就做好了我们的大“图”
-
外面的Graph类只需要把增删时维护好的“种子”放进来，直接调用updateGraph即可得到一张完整的“图”及其最短路径，拿出去查询就可以了，不需要关心是怎么实现的
-
当然，我们并不需要每次查询指令来的时候都重新计算，设置一个布尔变量upToDate，每当addPath或者removePath，对“种子”进行操作的时候，upToDate = false。当查询指令到来时，如果upToDate == false，那么调用一下updateGraph，将uoToDate变量设为true；否则，直接查阅
所以，“是否存在某一条边”可通过“种子”edgeCount来解决。
而是否连通，只要能算出来最短路径的（connectedMap内外层Key同时含有两个结点的ID），一定连通
第三次作业
这次在图的基础上，升级成为了RailwaySystem类（吐血）
加入了四个新的魔鬼需求：
-
连通块个数
-
最少票价
-
最少换乘
-
最少不满意度
下面我们来一一分析：
连通块个数
突然发现，连通块在BFS的时候就已经维护好了！
connectMap外层Key对应的HashMap就包含了它所有的可达点，所以它和它的可达点们构成了一个连通块！
沿用上次的Bfs类，在类中新建一个ArrayList，里面存Set集合（结点无序，不重复，所以用Set）
1 private ArrayList<HashSet<Integer>> connectedBlock; // 需要随着最短路径updateGraph 2 // 一个Set就是一个连通块 3 public int getBlockSize() { 4 return connectedBlock.size(); 5 }
遍历我们创建的大“图”，connectedMap外层结点，如果它已经存在于ArrayList中某个Set，直接跳过；
如果该结点尚未出现在任何Set里面，那么把它和它内层的所有可达点都放到一个Set，加入ArrayList
最终，返回这个ArrayList的大小，即为连通块个数
最少票价 & 最少换乘 & 最少不满意度
这三个问题在需求上是等价的，变成了无向带权图，我们可以列一个表格
这下不能愉快的BFS了，通过分析各路大佬提出来的思路，有拆点建站台和不拆点的方法，我写了两天拆点和Dijkstra，还用HashMap实现，心态爆炸，于是转向了优雅的Floyd和静态数组
思路
-
将每一个Path内所有的结点都连接，变成直连点，构成path.size大小的完全无向带权图
-
各个Path之间的共同点合并为1个点（也就是说integer型的ID就是结点唯一的标识）
-
每一条路径找出每个点到该路径内所有点的最短路径，也就是完全图的边权
-
这样，多走一条边就是多换乘1次，例如走了两条边就相当于从一个Path换乘到另一个Path，换乘一次，走N条边就是换乘了N-1次
-
为了方便计算，把所有边权都写成如上表所示，每一条边的权重都是“非换乘边权重”，多走一条边，票价+2，换乘+1，不满意+32；
封装一个Floyd类，里面仅仅含有一个函数
public int[][] perfromFloyd(int[][] a, int totalNodes)
-
perfromFloyd传进去的参数是邻接矩阵a，不同点个数totalNodes
-
返回的是最短路径矩阵（三层循环，莽就完事儿了）
-
三个需求都可以用这个perfromFloyd算，区别就是构建邻接矩阵时边权不同
RailwaySystem 类新增三个邻接矩阵
private int[][] priceResult; // 票价 private int[][] transResult; // 换乘 private int[][] unpleasantResult; // 不满意度 public void FloydNewRequest() // 在增删路径时统一处理这三个需求，更新上面的数组
-
使用Floyd先对每一条路径找出每个点到该路径所有点的最短路径
-
再用Floyd对每一个点的可达点找最短路径
-
每次增删都要遍历已有的pathContainer（HashMap<Path, Integer>）重新构建邻接矩阵
5 按照作业分析代码实现的bug和修复情况
在本单元的三次作业当中，强测均为100分，互测中没有被找出bug（组员都比较平和）
6 阐述对规格撰写和理解上的心得体会
-
因为初次接触规格，所以还需要花一定的时间来熟悉它。规格描述确实让我们少了很多理解上的歧义，也许在更大的工程当中使用起来可以提高效率。
-
第三题真的好难部署啊，呜呜呜
-
令我比较惊喜的是，在第三次作业中，不拆点的Floyd算法貌似表现得不错，没有炸TLE
-
好像规格在实际作业中很少看……第三次作业被搞成了算法作业