前言

第三单元的主题是规格化设计,主要是理解如何根据规格进行代码实现,如何撰写规格以及规格撰写和代码实现的区别等。三次作业简单来说就是对课程组给出的规格进行翻译,不过需要注意部分方法的实现性能。

关于JML学习,(感觉现在也没人学这个了),课程组给出的JML-level0已经说的比较简洁详细了,总结了所有这次作业可能用到的语法等,还有部分拓展,我也写了一篇笔记。(也没简洁多少,主要是记录)

第一次作业

第一次作业为简单的社交关系的模拟和查询,通过NetworkPerson维护社交网络的图并询问某些图的特性,同时需要对某些非法的指令进行异常抛出和记录相关信息。

代码架构

总的架构课程组已经给出了,可能有一点创意的地方就在于异常的设计,我使用了 工厂模式 进行封装。

1
2
3
// ExceptionManager.java
private static final HashMap<Exceptions, HashMap<Integer,Integer>> allCounts = new HashMap<>();
private static final HashMap<Exceptions,Integer> total = new HashMap<>();

ExceptionManager里面维护两个容器分别是某种异常下各种id的触发次数以及某种异常的总触发次数,当需要抛出异常的时候就进行信息的更新,大致的形式如下:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
// ExceptionManager.java
public static Exception getException(Exceptions exceptionType,int id) {
addTotalException(exceptionType);
addPersonException(exceptionType,id);
switch (exceptionType) {
case PersonIdNotFound:
return new MyPersonIdNotFoundException(id);
case EqualPersonId:
return new MyEqualPersonIdException(id);
default:
assert false;
}
return null;
}

public static Exception getException(Exceptions exceptionType,int id1,int id2) {
//...
}

需要两个id的异常同理,只需要特判一下id大小和是否相同进行相应维护即可。

因为我把成员都设成了静态,异常构造时直接进行相关查询即可。

Network抛出异常时为了程序美观和代码复用我也进行了封装,如:

1
2
3
4
5
6
7
8
// Network.java
private void throwPersonIdNotFound(int id) throws PersonIdNotFoundException {
if (!contains(id)) {
Exception exception = ExceptionsManager.getException(Exceptions.PersonIdNotFound,id);
assert exception != null : "PersonIdNotFound == null!";
throw (PersonIdNotFoundException) exception;
}
}

其实也不太需要工厂模式,因为这样写也需要在NetWork中对每一种异常写一个方法,不过要是课程组让这些异常都继承自一个带print方法的异常,那么只需要一或者两个方法即可,就很简洁很多,现在这样感觉有太多无意义的重复,比如各种异常之间并没有联系(比如单参数和双参数可以分为一类等的关系)。

部分方法实现

isCircle & queryBlockSum

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// Network.java
/*@ public normal_behavior
@ requires contains(id1) && contains(id2);
@ ensures \result == (\exists Person[] array; array.length >= 2;
@ array[0].equals(getPerson(id1)) &&
@ array[array.length - 1].equals(getPerson(id2)) &&
@ (\forall int i; 0 <= i && i < array.length - 1;
@ array[i].isLinked(array[i + 1]) == true));
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id1);
@ signals (PersonIdNotFoundException e) contains(id1) && !contains(id2);
@*/
public /*@ pure @*/ boolean isCircle(int id1, int id2) throws PersonIdNotFoundException;

/*@ ensures \result ==
@ (\sum int i; 0 <= i && i < people.length &&
@ (\forall int j; 0 <= j && j < i; !isCircle(people[i].getId(), people[j].getId()));
@ 1);
@*/
public /*@ pure @*/ int queryBlockSum();

isCircle判断两个点是否连通。

queryBlockSum其实就是图中联通块的数量blocks,因为对答案有贡献的点满足它之前(某种顺序)的所有点都和它不连通,对于一个联通块在这种顺序下最靠前的点x必然可以产生1的贡献,而其他的点由于x的存在不能产生贡献,所以答案就是联通块数量。

比较经典的连通性和联通块维护就是通过并查集,通过路径压缩或者按秩合并可以达到一个比较优秀的复杂度(O(log)O(log)左右,结合使用会更低),并查集的直接作用时判断两个点是否在一个联通块也就是isCircle需要的,而联通块动态维护即可:

  1. 加入人的时候,blocks+1
  2. 当加入关系的两人不连通时,blocks-1

当然上述两种查询通过dfs或者bfs进行搜索也是可以的,只要打上vis标记避免重复遍历即可,只是复杂度相较之下略高(O(n)O(n))。

queryTripleSum

1
2
3
4
5
6
7
8
9
10
11
// Network.java
/*@ ensures \result ==
@ (\sum int i; 0 <= i && i < people.length;
@ (\sum int j; i < j && j < people.length;
@ (\sum int k; j < k && k < people.length
@ && getPerson(people[i].getId()).isLinked(getPerson(people[j].getId()))
@ && getPerson(people[j].getId()).isLinked(getPerson(people[k].getId()))
@ && getPerson(people[k].getId()).isLinked(getPerson(people[i].getId()));
@ 1)));
@*/
public /*@ pure @*/ int queryTripleSum();

查询三元环的数量,也可以进行动态维护,每次加入关系(边),通过遍历其中一人认识的人,如果另一个人也认识这个人那么总的答案+1,这种时候选取认识的人更少的一方进行遍历会更好,当然直接遍历整个网络的人也是可以的,虽然最差复杂度一致但是实际上前者肯定会快不少。

第二次作业

第二次作业加入了MessageGroup,模拟群组和消息的功能。

异常

因为Group的加入,让某些异常的判断条件不再唯一,所以之前说的抛出异常的方法进行了以下修改:

1
2
3
4
5
6
7
8
// Network.java
private void throwPersonIdNotFound(boolean check,int id) throws PersonIdNotFoundException {
if (check) {
Exception exception = ExceptionsManager.getException(Exceptions.PersonIdNotFound,id);
assert exception != null : "PersonIdNotFound == null!\n";
throw (PersonIdNotFoundException) exception;
}
}

虽然更加规范化了,但是让我更难受了,因为各类方法更加趋同了却不能合并。

部分方法实现

modifyRelation

规格很长,简单来说就是修改两个点的边权,如果修改后边权为非正数那么删除这条边。

修改后为正数很简单,主要考虑删除边的情况会造成什么影响:

  1. 三元环数量需要进行更新
  2. 连通性可能发生改变

对于第一个影响很简单只需要照着加边进行修改即可,因此可以合并成一个方法,设置对答案的影响参数(±1\pm 1)即可。

对于第二个影响,删边对连通性可能有影响也可能没影响,但是没有一种优秀(比重构更快)的方法进行判断,并且由于并查集没有删除操作,因此如果还要继续使用并查集的话就需要对并查集进行重构,可以像之前说的使用搜索进行部分重构——只修改与这两个点连通的点。

先从一个点进行搜索,将搜到的点的父亲都设为这个点,结束后如果另一个点没有vis标记说明产生了新的联通块,令blocks+1然后同样的方式从这个点进行搜索更新它所在的联通块的点的父亲信息,总体复杂度O(n)O(n)

getAgeMean & getAgeVar

1
2
3
4
5
6
7
8
9
10
11
// Group.java
/*@ ensures \result == (people.length == 0? 0:
@ ((\sum int i; 0 <= i && i < people.length; people[i].getAge()) / people.length));
@*/
public /*@ pure @*/ int getAgeMean();

/*@ ensures \result == (people.length == 0? 0 : ((\sum int i; 0 <= i && i < people.length;
@ (people[i].getAge() - getAgeMean()) * (people[i].getAge() - getAgeMean())) /
@ people.length));
@*/
public /*@ pure @*/ int getAgeVar();

分别是求组内成员年龄平均值和方差。

对于前者可以动态维护组内成员年龄和,对于后者可以进行以下公式推导:

ageVar=(ageiageMean)2n=agei22ageiageMean+nageMean2n=agei22ageSumageMean+nageMean2n\begin{aligned} ageVar&=\frac{\sum{(age_i-ageMean)^2}}{n}\\ &=\frac{\sum{age_i^2}-2*\sum{age_i*ageMean}+n*ageMean^2}{n}\\ &=\frac{\sum{age_i^2}-2*ageSum*ageMean+n*ageMean^2}{n} \end{aligned}

因此只需要再维护一个组内成员年龄平方和即可。

需要注意的是,使用到的除法是向下整除,所以不能轻易地将ageMeanageMean变成ageSumn\frac{ageSum}{n}然后进行消除,因为这种情况下nageSumnageSumn*\frac{ageSum}{n}\neq ageSum

queryBestAcquaintance & queryCoupleSum

前者查询与某个点的最大边权的边(根据定义唯一)连接的点,后者查询互相满足前者条件的点对数。

前者可以考虑对每个点动态维护各自的bestAcquaintance,在加边、更改边权以及删边的时候进行更新,加边只需要判断是否能成为bestAcquaintance即可,而后两者在改动为当前的bestAcquaintance时就需要从集合中进行O(n)O(n)遍历更新。

对于后者则不考虑动态维护了,因为改动是跟随着每一次点的bestAcquaintance的,但是两者不是同一层次的,要是改动对边权的改动都在Network倒也好说,但偏偏Group内也会修改边权,强行维护也不是不行,但整体就不是很美观了,比较零散后期拓展性可能不是很客观,所以直接选择O(n)O(n)查询就好了(前面已经保证了bestAcquaintance查询是O(1)O(1)的)。

queryGroupValueSum

查询组内各成员之间的边权和,不太好动态维护,因为边权修改部分在NetworkPersonGroup相当于高Person一级,如果动态维护的话就得再让每个人记录所在的组,然后进行某种判断,感觉性能也不会很优秀,所以最后打算直接O(n2)O(n^2)求了。

sendMessage

并不复杂,只是需要注意课程组对于下标的要求,所以对于这个数据的维护需要用有序容器,比如ArrayList或者LinkedList,由于需要在首位插入,所以后者复杂度更加优秀。

第三次作业

第三次作业增加了继承自MessageEmojiMessageRedEnvelope以及NoticeMessage,实现不同消息的类型以及相关操作。

部分方法实现

deleteColdEmoji

删除包含的emoji热度低于limitEmojiMessage以及相应的emoji,已经维护了每个emoji的热度。

删除有以下两种方式:

  1. 删除信息可以遍历信息然后判断是否是EmojiMessage并且包含的emoji热度是否低于limit,然后进行删除信息,最后遍历emoji集合删除相关emoji
  2. 再开一个集合emojiMessages对每个emoji记录包含该emojiEmojiMessage,删除操作遍历emoji集合然后对需要删除的emoji根据emojiMessages进行删除,然后删除emoji

前者操作简便,后者复杂度更优秀。

我选择的是后者,对于emojiMessages需要进行动态维护,在以下几个地方:

  1. 储存emoji

    1
    emojiMessages.put(id,new HashSet<>());
  2. 发送信息时,需要将信息移除集合

    1
    emojiMessages.get(((EmojiMessage) message).getEmojiId()).remove(message.getId());
  3. 添加信息时,将信息加入集合

    1
    emojiMessages.get(((EmojiMessage) message).getEmojiId()).add(message.getId());

然后关于遍历删除我在上个单元的作业已经讲过了,需要使用迭代器。

queryLeastMoments

查询包含某个点x的最小环(边权和,至少3个点)。

最小环一定可以由最小生成树再加上一条非树边组成,以x为根节点的话,非树边(<u,v>)需要满足的条件就是

  1. (u==x && dep[v]3)  (v==x && dep[u]3)(u == x \ \&\&\ dep[v] \ge 3)\ ||\ (v==x\ \&\&\ dep[u]\ge3)
  2. ux && vx && LCA(u,x)==xu\ne x\ \&\&\ v\ne x\ \&\&\ LCA(u,x)==x

LCA(u,v) 就是两者的最近公共祖先。

实现部分可以考虑使用Dijkstra算法+枚举边,其实prim算法和Dijkstra差不太多,最短路的前驱结点就是该结点的父亲结点,所以通过Dijkstra算法可以得到一颗最小生成树,最短路径就是该结点到源点(根节点)的边权和。关于深度和LCA部分真正按照定义实现的话稍显复杂,简单的做法就是记录每个点的最短路是从哪个点延伸出来的,也就是它深度为2的祖先是谁,然后判断就好了。

具体实现时,由于朴素的DijkstraO(n2)O(n^2)的复杂度,可以加入堆优化实现达到O(mlogn)O(mlogn)级别,在稠密图中复杂度前者会更优,但就本题而言稠密图时mm的范围并不大,相较之下还是后者好。

结点的封装

1
2
3
4
5
6
7
8
9
10
// Node.java
private final int id; // 编号
private final int from; // 之前说的深度为2的祖先
private final int values; // 最短路

public Node add(int origin, int id, int values) {
// 从当前节点加上一条边,origin-源点,id-边的另一个点的id,values-边权
return new Node(id, this.id == origin ? id : this.from, this.values + values);
}
public int compareTo(Node node) {return Integer.compare(values,node.values);} // 用于堆的比较

遍历边的部分

1
2
3
4
5
6
7
8
9
10
11
12
13
14
// Network.java
for (Integer id1 : people.keySet()) {
if (!minPath.containsKey(id1)) { continue; }
Node x = minPath.get(id1);
for (Map.Entry<Integer,Integer> entry : map.get(id1).entrySet()) {
int id2 = entry.getKey();
if (!minPath.containsKey(id2)) { continue; }
Node y = minPath.get(id2);
if (x.getFrom() == y.getFrom()) { continue; }
if (x.getId() == id && y.getFrom() == y.getId()) { continue; }
if (y.getId() == id && x.getFrom() == x.getId()) { continue; }
minAns = Integer.min(minAns,x.getValues() + y.getValues() + entry.getValue());
}
}
优化部分

其实可以发现在更新最短路的过程中,对于每一条边肯定会到达一个状态就是x和y都已经得到了最短路(否则就会更新y的最短路,然后再次枚举这条边),而此时就可以进行答案的更新,而当不都是最短路的时候也可以更新只是答案不正确而已,所以我们就可以在求最短路的过程中进行更新答案,这样的好处在于可以根据当前已有答案减少不必要的遍历,即当已有答案已经大于当前点x的最短路时,就可以从最短路循环中break了。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
// Network.java
public static int getLeastCircle(int id,HashMap<Integer,HashMap<Integer,Integer>> map) {
HashMap<Integer,Node> minPath = new HashMap<>();
HashMap<Integer,Boolean> vis = new HashMap<>();
PriorityQueue<Node> queue = new PriorityQueue<>();
int minAns = Parameters.maxValue;
Node node = new Node(id,id,0);
queue.add(node);
minPath.put(node.getId(),node);
while (!queue.isEmpty()) {
Node x = queue.poll();
if (minPath.get(x.getId()).getValues() > minAns) { break; }
if (vis.containsKey(x.getId())) { continue; }
vis.put(x.getId(),true);
HashMap<Integer,Integer> dis = map.get(x.getId());
for (Map.Entry<Integer,Integer> entry : dis.entrySet()) {
int idY = entry.getKey();
int value = entry.getValue();
Node y = x.add(id,idY,value);
if (!minPath.containsKey(idY) || y.compareTo(minPath.get(idY)) < 0) {
queue.add(y);
minPath.put(idY,y);
}
y = minPath.get(idY);
if (x.getFrom() == y.getFrom()) { continue; }
if (x.getId() == id && y.getFrom() == y.getId()) { continue; }
if (idY == id && x.getFrom() == x.getId()) { continue; }
minAns = Integer.min(minAns,x.getValues() + y.getValues() + value);
}
}
return minAns;
}

测试过程

黑白箱测试

黑箱测试:测试者不需要了解程序的内部实现细节和结构,只是通过观察输入和输出是否符合预期来验证程序是否正确运行。黑箱测试的目的是验证程序的功能和行为是否正确,是站在用户的角度来说的。

白箱测试:测试者需要了解程序的内部实现细节和结构,可以检查程序的逻辑路径、条件覆盖、循环覆盖等,并使用这些信息设计测试用例和执行测试。白箱测试的目标是验证程序的内部逻辑是否正确,确保代码按照预期方式工作,通常由开发者执行。

单元测试

用于验证系统的最小的可测试单元,如方法、类等的正确性,通过确保每个代码单元都能够按照预期工作从而确保整个系统的正确性。单元测试的主要目的是隔离和测试代码单元,以验证其功能是否正确、边界条件是否处理正确、异常情况是否被处理等。

功能测试

旨在验证程序的功能是否符合预期,主要关注程序在各种输入条件下的输出和行为,以确保程序按照用户需求和规格说明正确地执行。

集成测试

用于测试不同组件、模块或子系统之间的集成和交互,其目的是验证各个组件在集成后能否正常协同工作,以确保系统在整体上具有正确的功能、性能和稳定性。

压力测试

用于评估系统在负载压力下的性能和稳定性,通过模拟高负载条件和极限情况来测试系统的响应能力、吞吐量、资源利用率和错误处理能力。在作业中表现为对时间和内存的限制。

回归测试

用于验证修改或更新后的程序在进行修改之前的功能和性能的基础上是否仍然正确运行,它的目的是确保修改没有引入新的错误或者对现有功能产生负面影响。

测试工具 & 数据生成

手动感谢权佬的测试工具和群友的数据,测试原理大概是数据生成器+对拍。

数据生成很麻烦,随机生成的话强度不是很高,需要考虑生成不同类的样例:

  1. 检测异常抛出是否正确
  2. 完成上述验证后需要减少无效的指令,针对稀疏图、稠密图等构造数据,或者像单元测试一样针对某个指令构造数据

还有OKTest的数据就基本上只能手动根据规格进行构造了。

架构分析

图模型

没有专门另外维护图的结构,课程组规格给出的结构就相当于是一个图了,Network记录了所有点,Person记录了和它相连的点以及对应的边权(类似前向星可能),至于Group其实相当于是子图。

维护策略

需要维护的信息大部分都在前面说了,性能大体是没啥问题的,除了GroupValueSum,要是课程组加入大量的点进同一个组,并且多次查询的话,可能会超时,可能的解决方法就是遍历的时候第二维变成组员的集合和人认识的人的集合的较小的一个。

规格和实现分离

像荣文戈老师说的,规格化设计就是一种契约,是客户和程序员之间的约定,对于规格中的要求不同的人可以有不同的实现方法,只要保证满足条件即可,例如容器的选择、以及数据结构和算法的选择,比如课程组在tripleSum的规格中使用了三重循环,实际实现显然不能这样操作,否则直接T飞掉。

OKTest

OKTest通过方法执行前后的数据判断方法是否正确按照规格执行,判断过程需要使用规格提供的方法才能保证严格的正确性,不过OKTest实际上也是黑盒测试,还是比较依赖于数据构造的。

OKTest的判断过程是根据规格来的,然而规格其实也有挺多的表述方式的,所以想要OKTest简单的话对规格的要求也挺高的,如何采用完备并且简单的规格也是一门技术活(虽然荣文戈老师多次强调规格不必考虑实际实现方法)。

Bug分析

第一次作业强测错了一个点是关于queryTripleSumOKTest的,因为我是直接三层循环枚举的,所以最后统计结果需要 /6,但是我却只 /3

第二次作业OKTest有一个地方afterbefore写反了,第三次作业emojiMessages维护以及OKTest出现了问题,最后强测都是100。

(上述错误中测都没测出来,不得不说是真水)

体会与感想

  • 设计相比于代码实现更加困难,如果设计出现问题,修改起来更加耗费人力物力,本次单元对规格化设计只是相当于在门口驻足观望,重点在于如何实现规格,而更加重要的撰写需要自己去深挖了,这绝对是对自我的提升,无论是考虑问题的角度还是经验的积累。

  • 课程组在架构上的设计可能存在部分不足,比如前面说过的异常的问题,大量的异常但是没有什么本质上的区别,完全可以继承自一个异常,没有必要各自继承,这样也导致实现的时候大量的重复代码却由于抛出异常类型的限制无法合并;还有某些异常抛出不合理,比如delFromGroup方法的第三个异常

    1
    2
    3
    @signals (EqualPersonIdException e) (\exists int i; 0 <= i && i < groups.length;
    @ groups[i].getId() == id2) && (\exists int i; 0 <= i && i < people.length;
    @ people[i].getId() == id1) && !getGroup(id2).hasPerson(getPerson(id1));

    实在不能理解为什么不是PersonIdNotFoundException;除此之外,规格好像不是很统一,比如判断Network是否存在某个人的时候,某些地方使用contains,某些地方又使用forall去重复了一遍前者的规格。当然我也很理解,JML确实很难写,助教也需要兼顾自己的学业,所以难免会出现疏漏。

  • 关于动态维护这个问题,我觉得可以动态维护的东西,应该尽量是同一层面上的东西,换句话说不会修改或者修改只在这个地方,比如组内求关于年龄的相关数据,所有成员的年龄都是固定的,所以很容易维护;然而关于ValueSum,它既是改变的,同时改变又发生在NetworkPerson内部,这个过程基本上不会经过Group,维护就很麻烦。

    不过动态维护对于后期迭代可能不是很友好,需要经常注意到对这些动态变量的修改,忘记了的话就会导致结果错误,所以实际上就是简便和性能的抉择。

  • 不得不说的是,JML没有高亮再加上臃肿的描述,使得阅读过程变得十分困难,不过主要的还是学会规格化设计的思想,而不是这个淘汰的语言。n