BUAA_OO_2020_第三单元总结
BUAA_OO_2020_第三单元总结
JML理论基础
简介
JML(Java Modeling Language)是一种用于对JAVA程序进行规格化设计的语言,其通过定义接口所包含方法的行为,来约束实现接口的类的行为。本章作业就是实现课程组提供的用规格定义好的接口,来学习如何根据规格写方法。
JML表达式
原子表达式
关键字 | 含义 | 示例 |
---|---|---|
\result | 定义返回值 | \result == getPerson(id1).getAge() |
\old(expr) | expr在执行方法前的取值 | groups.length == \old(groups.length) + 1; |
\not_assigned(x) | 括号中的变量是否倍赋值 | \forall int i; 0 <= i < groups.length; \not_assigned(groups[i]) |
其中有一点容易混淆。\old(group.length)代表的是group在执行方法前的长度。而\old(group).length == group.length,指的是方法执行后的长度。这是由于在方法执行过程中,并没有改变group指向的对象,只是改变了其指向对象的值。
量化表达式
表达式 | 含义 | 示例 |
---|---|---|
\forall | 对于范围内的每个元素遍历 | (\forall int i; 0 <= i < groups.length; \not_assigned(groups[i])); |
\exists | 范围内存在一个元素满足后续条件 | (\exists int i; 0 <= i && i < groups.length; groups[i].getId() == id) |
\sum | 范围内满足条件的表达式的和 | (\sum int i; 0 <= i < people.length && people[i].getAge() >= l && people[i].getAge() <= r; 1) |
方法规格
在此,以作业提供的接口方法规格为例,依次分析方法规格的组成部分。
1 /*
2 @ public normal_behavior
3 @ requires contains(id); //前置条件
4 @ assignable \nothing; //副作用限定
5 @ ensures (\exists int i; 0 <= i && i < people.length && people[i].getId() == @id;money[i] == \result); //后置条件
6 @ also
7 @ public exceptional_behavior //异常行为
8 @ signals (PersonIdNotFoundException e) !contains(id);
9 @*/
前置条件
通过requires子句表示,要求确保其表达式为真才可进行正常行为操作。
后置条件
通过ensures子句表示,要求确保方法执行后其表达式为真
副作用限定
通过assignable或modifiable表示,限定方法能够修改的对象
异常行为
通过signals (ExceptionType e)为了提高程序鲁棒性,在不满足requires表达式时,需要进行其他异常行为操作(比如抛异常)。
一般通过public normal_behavior和public exceptional_behavior来区分正常行为和异常行为,但是对于正常行为设计多种条件分支(if-else语句)时,也可以把每个正常/异常分支使用public xxx_behavior区分开,以提高可读性。(在本次作业提供的规格中多是这样,所以阅读规格时按照其分开,就可理清各种个各种if-else情况,方便输写)
类型规格
类型 | 含义 | 示例 |
---|---|---|
invariant | 不变式,在可见状态下必须满足的条件 | invariant seq_nodes != null |
constraint | 状态变化约束,前序和当前状态之间关系的约束 | constraint counter == \old(counter)+1; |
工具链
OpenJML
检查JML语法。不支持高版本java,环境很难配。
JMLUnitNG
根据规格自动生成测试。环境很难配。
Junit
单元测试。根据规格自行构造测试,可以检查覆盖率,尽量保证覆盖率高(但不是全部覆盖就没bug)。
由于OpenJML和JMLUnitNG功能有限,所以本单元中主要还是采用单元测试的方法。
OpenJML验证
整个src的检测结果:
结果非常申必。
调整后:
发现以上的bug。
有时候会冒出上百个warning。为了美观就不放了。
JMLUnitNG测试
以上为使用JMLUnitNG进行UserGroup类的测试。
可以看到,其主要对于边界情况进行简单测试。
我的架构设计
第一次作业
容器选择
第一次作业要求比较简单,实现了官方提供的三个接口。为了使得访问更加方便,多使用HashMap作为容器。例如:在User类(实现Person接口)中,使用HashMap<id, value>来存储熟人和value值。
并查集
另外,针对isCircle
方法,为了降低复杂度,选择并查集。在Network中,实现HashMap<id,father_id>存储每个用户和其祖先的id。在addPerson
方法中,新增id对应的键值对,将father_id设为自己。在addRelation
方法中,合并两个人的father_id。另实现find
方法,路径压缩+返回祖先。在isCircle
方法中,对两个id分别find出祖先,以判断二人是否连通。
在find
方法进行路径压缩时,需要注意先将find其父节点的返回值保存,再替换和返回,及采用如下写法:
1 private int find(int id) {
2 if (father.get(id) == id) {
3 return id;
4 }
5 int ans = find(father.get(id));
6 father.replace(id, ans);
7 return ans;
8 }
若使用如下的简写方法,会在成链情况&人多的时候出现栈溢出:
1 private int find(int id) {
2 if (father.get(id) == id) {
3 return id;
4 }
5 father.replace(id, find(father.get(id)));
6 return father.get(id);
7 }
第二次作业
本次作业新增Group接口,在设计过程中需要注意其中方法的性能。如果直接找着JML写,会出现O(n^2)复杂度,而出现CTLE错误。因此,采用在向Group中加人的时候预处理relationSum,valueSum,conflictSum,ageSum,ageVar(由于向Group中加人有指令条数限制)。预处理方法如下:
1 public void addPerson(Person person) {
2 // renew people
3 people.put(person.getId(), person);
4 // renew conflictSum
5 conflictSum = conflictSum.xor(person.getCharacter());
6 // renew ageSum
7 ageSum = ageSum + person.getAge();
8 int meanAge = getAgeMean();
9 ageVar = 0;
10 // renew relationSum
11 // renew valueSum
12 // renew ageVar
13 for (Integer next : people.keySet()) {
14 ageVar = ageVar +
15 (people.get(next).getAge() - meanAge) * (people.get(next).getAge() - meanAge);
16 if (people.get(next).isLinked(person)) {
17 relationSum = relationSum + 2;
18 valueSum = valueSum + (people.get(next).queryValue(person)) * 2;
19 }
20 }
21 ageVar = ageVar / people.size();
22 relationSum = relationSum - 1;
23 }
采用这种方法不要忘记,在addrelation的时候可能会造成relationSum、valueSum的变化,因此还需要新建方法如下:
1 public void updateRelation(int value) {
2 relationSum = relationSum + 2;
3 valueSum = valueSum + 2 * value;
4 }
第三次作业
本次作业难点在于最短路算法和点双连通分量算法。
最短路
最短路采用堆优化迪杰斯特拉算法,如果不堆优化可能会被卡。具体实现方法为,新建Pair类,包含属性id和dis(表示到起点的距离),并继承comparable接口,重写compareTo方法。
1 @Override
2 public int compareTo(Pair o) {
3 if (dis > o.getDis()) {
4 return 1;
5 } else if (dis < o.getDis()) {
6 return -1;
7 }
8 return 0;
}
点双连通分量
由于对tarjan不熟悉,怕写bug,再加上时间足够,因此采用暴力方法。
首先如果people.size == 2,一定不满足条件,直接return false。
如果!isCircle(id1,id2),一定不满足条件,直接return false。
若isLinked(id1, id2),则将两人分别从acquaitance中移除,及删掉两人之间的边,再dfs。若两人依然连通,则return true。否则return false。
若!isLinked(id1, id2)针对所有出了起点、重点的人,将他们从图中删除(具体实现方法为,设置lock=id),然后dfs判断id1和id2的连通性。若一直连通,则return true。否则return false。
还有一种常数优化,就是再遍历所有点的时候,如果该点和id1不isCircle,可以直接continue,不进行dfs,因为去掉其一定不会影响两点之间本来的连通性。
关于测试和bug
第一次
第一次作业比较简单,在自己写代码的时候发现的bug就是find()
方法栈溢出问题,已在架构设计中详述。
互测和公测都没有出现bug,屋里十分安静。
第二次
第二次作业在自己测试中,一开始没有考虑到addRelation对Group类的relationSum、valueSum的影响,通过Junit单元测试发现。
从本次作业开始采用对拍,不验证输出的正确性,而是横向比较多人的输出,若出现不同则有人有bug。
在公测和互测中没有被发现bug。
互测中,共hack到两个bug:
一位同学在使用O(1)求ageVar的时候,采用如下写法:
(ageSquaredSum - 2 * mean * ageSum) / people.size() + mean * mean;
这种写法的错误在于,第一个因子的分子部分可以是负数,而java整除对于负数向上取整。用如下数据就可以hack:
ag 1
ap 1 1 1 4
ap 2 1 1 5
ap 3 1 1 6
atg 1 1
atg 2 1
atg 3 1
qgav 1一位同学由于时间复杂度高导致CTLE
第三次作业
第三次作业的易错点比较多,依然采用对拍,不验证输出的正确性,而是横向比较多人的输出,若出现不同则有人有bug。在本地测试时发现了一下易错问题:
针对qsl,只有两人的情况可能需要特判。
使用优先队列时,必须调用add方法才会更新排序,直接修改queue中元素时不会触发重新排序的。
Group类中的ageVar会溢出int范围(但是由于java不是到什么神奇的机制,并不会出现错误),但是需要注意,如果多项式中某一项转long而某一项没转,可能会出问题。
delPerson的时候可能需要考虑除0问题。
在公测和互测中没有被发现bug。
在互测中,发现了一下5个bug。
delPerson的时候没有考虑除0。
采用静态数组,出现越界问题。
在delPerson的时候没有更新relationSum,valueSum
暴力求qsl写的有点过于暴力,导致CTLE
qmp不完备,由对拍发现bug,由于可读性不太好,没有深究是什么问题。
测试
Junit单元测试,用于输写一些数据量较小的边界情况,尽量覆盖所有情况,测试基本功能。在此举例:
1 @Test
2 public void testQueryStrongLinked() throws Exception {
3 //TODO: Test goes here...
4 net.addPerson(new User(0, "a", new BigInteger("63"), 22));
5 net.addPerson(new User(1, "a", new BigInteger("1"), 21));
6 assertEquals(false,net.queryStrongLinked(0,1));
7 net.addPerson(new User(2, "a", new BigInteger("1"), 21));
8 // only two + not linked
9 assertEquals(false,net.queryStrongLinked(0,1));
10 net.addRelation(0,1,5);
11 // only two + linked
12 assertEquals(false,net.queryStrongLinked(0,1));
13 net.addRelation(0,2,5);
14 assertEquals(false,net.queryStrongLinked(0,1));
15 // triangle
16 net.addRelation(1,2,5);
17 assertEquals(true,net.queryStrongLinked(0,1));
18 net.addPerson(new User(3, "a", new BigInteger("63"), 22));
19 net.addPerson(new User(4, "a", new BigInteger("1"), 21));
20 net.addRelation(2,3,5);
21 net.addRelation(3,4,5);
22 net.addRelation(4,2,5);
23 // eight
24 assertEquals(false,net.queryStrongLinked(0,3));
25 assertEquals(true,net.queryStrongLinked(3,4));
26 }对拍。在提交之前,邀请一些好友参加对拍,自动生成数据,横向比对输出结果和运行时间。第二次作业帮助多人共de出2-3个bug,第三次帮助多人共de出>5个bug,效率还是蛮高的。但是,由于对拍数据量较小,对于一些小数据边界情况(比如qsl的仅两人)可能不太友好,所以充足的本地单元测试是必要的。
感想
由于本单元没有动手写JML规格,所以对于其输写过程还是比较陌生。
在根据JML输写代码时,看懂JML和按照其写出满足要求的方法不难,但是很多时候需要意会其中的深意,并且考虑性能上的优化。例如,queryblocksum方法是在求连通分量的数量,如果分析出这点,通过动态维护blocksum或者根据并查集求都是很简便的,但如果完全仿照JML的写法,双重循环,会使得性能上有很大的损失。
本单元印象最深的就是在理论课上老师提到,如果规格不够全面,没有考虑一些异常情况,一定要在实现时体现出来抛出的异常是由于规格,而不是自身实现的问题,不能把锅扣到自己头上,我觉得很有道理。
最新文章
- python pymysql和orm
- linq学习
- Android 二维码扫描框 加四个角及中间横线自动下滑
- 利用iOS API编写简单微博客户端全过程
- 小白日记39:kali渗透测试之Web渗透-SQL手工注入(一)-检测方法
- 《RedHatLinux逻辑卷的管理》——一条龙服务
- Ajax跨域请求——PHP服务端处理
- 修改.htaccess实现子目录绑定示例分享
- Struts2 过滤器与拦截器
- 详解Session分布式共享(.NET CORE版)
- Linux第七节随笔-下磁盘管理
- rocketmq番外篇(一):开发命令行
- linux执行jmeter脚本解决响应数据为空
- 微信小程序开发之搞懂flex布局5——cross axis
- [matlab] 16.多约束非线性规划 ga工具箱解决 [带不等式约束]
- Linux基本的操作
- Activity启动模式 Tasks和Back Stack
- U3D面试题
- 2.C#知识点:I/O
- HTML <;input>; <;button>; <;submit>;
热门文章
- svg &; regex
- html->;pdf直接下载
- BGV上线17小时最高888.88美金,投资最高回报率近+1778倍, 带动NGK内存暴涨
- K8s炼气期(一)| minikube安装本地Kubenetes环境
- 一条sql语句的执行过程
- Python数据读取函数
- 基于element-ui封装一个Table模板组件
- fastjson 漏洞利用 命令执行
- mongoDB服务器连接不上Error: couldn&#39;t connect to server 127.0.0.1:27017, connection attempt failed: SocketException:
- dubbo实战之四:管理控制台dubbo-admin