面向对象OO第三单元总结

程序员文章站 2022-10-05 10:43:43

第三单元OO总结博客 1 梳理JML语言的理论基础、应用工具链情况由于篇幅原因，这里只梳理几个在本单元常用的注释结构行注释://@annotation 块注释：/* @ annotation @*/ 例如：纯粹查询方法/*@ pure @ */，即方法的执行不会有任何副作用 JML表达式原子 ......

第三单元oo总结博客

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: 有两种场景使用
1. 除了正常功能规格外，还有一个异常功能规格，需要使用also来分隔。
2. 父类中对相应方法定义了规格，子类重写了该方法，需要补充规格，这时应该在补充的规格之前使用also;

signals子句

结构为signals (***exception e) b_expr，意思是当b_expr为true时，方法会抛出括号中给出的相应异常e。

例子：

/*@ public normal_behavior
    省略
     @ also 下面是异常行为
     @ public exceptional_behavior 
     @ assignable \nothing;
     @ signals (pathnotfoundexception e) path == null;
     @ signals (pathnotfoundexception e) path.isvalid() == false;
     @ signals (pathnotfoundexception e) !containspath(path);
     @*/
   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     }

面向对象OO第三单元总结

（错误示范）

正确使用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删了

在艰苦卓绝的研究下，和修改了一堆版本不兼容的问题后，测试代码终于运行成功了！

面向对象OO第三单元总结

（racenabled尚未解决）

junit 测试代码

创建单元测试可以直接在idea里面自动生成一个测试代码的框架

面向对象OO第三单元总结

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) 当不指向同一个内存地址或者不相等的时候，输出错误信息。注意信息是必须的，而且这个输出是格式化过的。

下面仅写出部分函数的测试代码

public class mygraphtest {
   mygraph graph = new mygraph();
   int[] nodelist1 = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 13};
   int[] nodelist2 = {-1, 6, -2, -3, -4, -5, -6, -7, -8};
   int[] nodelist3 = {0,1205, 999, 888, 777, 666};
   @before
   public void before() throws exception { // 每个方法检测之前，都另这个图里面有这三条路径
       system.out.println("ready to test " );
       //mygraph graph = new mygraph();
       graph.addpath(new mypath(nodelist1));
       graph.addpath(new mypath(nodelist2));
       graph.addpath(new mypath(nodelist3));
   }

   @after
   public void after() throws exception { // 每个函数检测完毕都会输出“test successfully!”
       system.out.println("test successfully!");
   }

@test
public void testcontainspath() throws exception { 
//todo: test goes here...
   system.out.println("testing containspath!");
   assert.asserttrue(graph.containspath(new mypath(nodelist1)));
   assert.asserttrue(graph.containspath(new mypath(nodelist2)));
   assert.asserttrue(graph.containspath(new mypath(nodelist3)));
   int[] nodelist4 = {9,9,9,9};
   assert.assertfalse(graph.containspath(new mypath(nodelist4)));
} 

@test
public void testcontainspathid() throws exception { 
   system.out.println("testing contains path id!");
   assert.asserttrue(graph.containspathid(1));
   assert.asserttrue(graph.containspathid(2));
   assert.asserttrue(graph.containspathid(3));
   assert.assertfalse(graph.containspathid(100));
} 


@test
public void testremovepath() throws exception { 
//todo: test goes here...
   graph.removepath(new mypath(nodelist1));
   assert.assertfalse(graph.containspathid(1));
} 

@test
public void testremovepathbyid() throws exception { 
//todo: test goes here...
   graph.removepathbyid(2);
   assert.assertfalse(graph.containspath(new mypath(nodelist2)));
} 

@test
public void testcontainsnode() throws exception { 
//todo: test goes here...
   assert.asserttrue(graph.containsnode(999));
   assert.assertfalse(graph.containsnode(14));


@test
public void testisconnected() throws exception { 
//todo: test goes here...
   system.out.println("testing is connected@");
   assert.asserttrue(graph.isconnected(2,-8)); // 判断这个连接是对的
   assert.asserttrue(graph.isconnected(13,-8));
   assert.assertfalse(graph.isconnected(0, 1));
   // 把这个文件拖到src文件夹里面即可运行

}

}

面向对象OO第三单元总结

愉快的tests passed!

上一篇： SEO 分析关键词密度和页面信噪比

下一篇： Python十分钟制作属于你自己的个性logo

面向对象OO第三单元总结

第三单元oo总结博客

1 梳理jml语言的理论基础、应用工具链情况

注释结构

jml表达式

原子表达式

量化表达式

操作符

方法规格

正常行为规格normal_behavior

前置条件

后置条件

副作用

异常行为规格expcetional_behavior

在线openjml链接

2 部署smt solver，至少选择3个主要方法来尝试进行验证，报告结果

3 部署jmlunitng/jmlunit，针对graph接口的实现自动生成测试用例，并结合规格对生成的测试用例和数据进行简要分析

生成数据

idea testme插件和 testng和openjml的安装历程

build testng from source code

正确使用openjml

junit 测试代码

junit中集中基本注解，是必须掌握的：

junit中部分assert方法总结：

Python面向对象总结

js面向对象编程总结

王之泰201771010131《面向对象程序设计（java）》第四周学习总结

PHP面向对象精要总结

OOCSS(面向对象的CSS)总结

PowerShell面向对象编程基础知识总结

Pyhton入门笔记第三天面向对象类

面向对象程序设计课程复习——Java基础知识总结

Python面向对象总结及类与正则表达式详解

面向对象第一次总结作业

面向对象OO第三单元总结

第三单元oo总结博客

1 梳理jml语言的理论基础、应用工具链情况

注释结构

jml表达式

原子表达式

量化表达式

操作符

方法规格

正常行为规格normal_behavior

前置条件

后置条件

副作用

异常行为规格expcetional_behavior

在线openjml链接

2 部署smt solver，至少选择3个主要方法来尝试进行验证，报告结果

3 部署jmlunitng/jmlunit，针对graph接口的实现自动生成测试用例， 并结合规格对生成的测试用例和数据进行简要分析

生成数据

idea testme插件和 testng和openjml的安装历程

build testng from source code

正确使用openjml

junit 测试代码

junit中集中基本注解，是必须掌握的：

junit中部分assert方法总结：

Python面向对象总结

js面向对象编程总结

王之泰201771010131《面向对象程序设计（java）》第四周学习总结

PHP面向对象精要总结

OOCSS(面向对象的CSS)总结

PowerShell面向对象编程基础知识总结

Pyhton入门 笔记 第三天 面向对象 类

面向对象程序设计课程复习——Java基础知识总结

Python面向对象总结及类与正则表达式详解

面向对象第一次总结作业

3 部署jmlunitng/jmlunit，针对graph接口的实现自动生成测试用例，并结合规格对生成的测试用例和数据进行简要分析

Pyhton入门笔记第三天面向对象类