|
1 梳理JML语言的理论基础、应用工具链情况由于篇幅原因，这里只梳理几个在本单元常用的 注释结构
JML表达式原子表达式
量化表达式
操作符
方法规格正常行为规格normal_behavior前置条件
后置条件
副作用
异常行为规格expcetional_behavior
在线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的安装历程
Build TestNG from source codeTestNG 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中集中基本注解，是必须掌握的：
junit中的assert方法全部放在Assert类中，总结一下junit类中assert方法的分类。 Junit中部分Assert方法总结：（来自这个博客）
下面仅写出部分函数的测试代码 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 Connected@"); 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! |
|
|
