BUAA_OO_2022_U3_JML规格
作者：互联网
第三单元总结
一、测试数据的准备
通过第三单元的训练项目的学习，我尝试了用JUnit单元测试框架，但是在几次作业的自测中，主要还是使用随机生成数据的方法测试。
随机生成数据主要有三个部分：
1.对每条指令的触发异常部分
在生成数据的最开始就对每条指令的异常处理进行覆盖性测试，主要是测试异常处理的基本功能。部分代码如下：
def coverAllException():
global groupCnt
global personCnt
id1 = random.choice(person_ids)
personId_In.append(id1)
personCnt = personCnt + 1
id2 = random.choice(person_ids)
while id2 == id1:
id2 = random.choice(person_ids)
newname = random.sample(alphabet, 10)
newname = ''.join(newname)
cmds.append(f'ap {id1} {newname} {random.randint(1, 200)}\n')
cmds.append(f'ap {id1} {newname} {random.randint(1, 200)}\n') # ap exception
cmds.append(f'ar {id2} {id1} 1\n') # ar exception1
cmds.append(f'ar {id1} {id2} 1\n') # ar exception2
cmds.append(f'ar {id1} {id1} 1\n') # ar exception4
因为只是对异常处理的正确性检验，这一部分生成数据主要用于检验完成架构之初的规格实现的正确性，在后续强测找bug过程中可以注释掉这部分。
2.随机数据的构造
主要分为两大部分：正确指令的构造，异常指令的构造。下面给出构造 ar 指令的方法：
def ar():
global cmds
p = random.random()
idIn1 = random.choice(personId_In)
idIn2 = random.choice(personId_In)
idNotIn1 = random.choice(person_ids)
while idNotIn1 in personId_In:
idNotIn1 = random.choice(person_ids)
idNotIn2 = random.choice(person_ids)
while idNotIn2 in personId_In:
idNotIn2 = random.choice(person_ids)
if p < 0.45:
cmds += f'ar {idIn1} {idIn2} {random.randint(1, 1000)}\n'
elif p < 0.55:
cmds += f'ar {idIn1} {idIn1} {random.randint(1, 1000)}\n'
elif p < 0.65:
cmds += f'ar {idNotIn1} {idIn1} 1\n'
elif p < 0.75:
cmds += f'ar {idIn1} {idNotIn2} 1\n'
elif p < 0.85:
cmds += f'ar {idNotIn1} {idNotIn2} 1\n'
else:
cmds += f'ar {idNotIn2} {idNotIn2} 1\n'
在后来的测试中发现，使用if-else结构生成数据（else生成触发异常的指令）异常指令占比仍然较高，达不到强测的效果，考虑到第一部分已经对异常处理做了覆盖性测试，可以将id的生成简化为id = random.randint(0, PERSON + 5)
这一部分是类似于JUnit测试的工作，针对每个方法规格的前置条件生成数据，在对拍过程中检验方法的后置条件等实现的正确性。
3.针对时间复杂度限制的数据构造
主要是针对qgvs、qgav等指令进行单独大量的数据构造。比如我在第10次作业中发现有人的qgav方法复杂度超过了O(n^2)，于是我构造了一个包含1111个Person的Group，剩下的指令全部为qgav。
这也是本单元hack的基本思路：阅读代码 + 定点爆破。
二、梳理本单元的架构设计，分析自己的图模型构建和维护策略
1.本单元架构设计
主要就是根据JML实现了自己的Person、Group、Message等类，除此之外，还建立了一个Egde类，用于记录person之间的关系，体现图中的边结构。
2.图模型构建和维护策略
2.1维护策略
除去可以依照JML规格直接实现的部分以外，还进行了一下的一些维护：
- 在Person类中用优先队列维护了person之间的关系（Edge类）
- 在Group类中维护了
valueSum、ageSum和ageSqure三个属性，使指令的时间复杂度为O(1) - 在Network类中维护了
blockSum属性，在addPerson和addRelation时会被修改，用来记录当前的连通分支数，使qbs指令的时间复杂度为O(1) - 对于每一个有id属性的对象的存储，都采用HashMap，方便O(1)查找
2.2图模型的构建
qci采用了并查集和路径压缩的方法，qbs采用动态维护blockSum属性的方法，qlc的最小生成树使用了堆优化的Prim算法,sim使用了dijkstra算法
2.2.1 路径可达
采用并查集和路径压缩的方法降低时间复杂度，维护了一个father的HashMap容器
private HashMap<Integer, Integer> father = new HashMap<>(); // <child, father>
public int find(int p) {
if (father.get(p) != p) {
father.put(p, find(father.get(p)));
}
return father.get(p);
}
public boolean isCircle(int id1, int id2) throws PersonIdNotFoundException {
if (!contains(id1)) {
throw new MyPersonIdNotFoundException(id1);
} else if (contains(id1) && !contains(id2)) {
throw new MyPersonIdNotFoundException(id2);
}
return find(id1) == find(id2);
}
2.2.2 最小生成树
采用堆优化的Prim算法
public boolean edgeQualified(int id, Edge edge) throws PersonIdNotFoundException {
Person person1 = edge.getPerson1();
Person person2 = edge.getPerson2();
return isCircle(id, person1.getId()) && isCircle(id, person2.getId());
}
public int queryLeastConnection(int id) throws PersonIdNotFoundException {
if (contains(id)) {
ArrayList<Person> subgroup = new ArrayList<>();
for (Person p : people.values()) {
if (isCircle(id, p.getId())) {
subgroup.add(p);
}
}
if (subgroup.size() == 1) {
return 0;
}
HashMap<Integer, Person> personInMinGroup = new HashMap<>();
PriorityQueue<Edge> edges = new PriorityQueue<>(Comparator.comparing(Edge::getValue));
MyPerson person = (MyPerson) subgroup.get(0);
edges.addAll(person.getEdges());
personInMinGroup.put(person.getId(), person);
int value = 0;
Edge edge;
while (personInMinGroup.size() < subgroup.size()) {
while ((edge = edges.poll()) != null) {
if (edgeQualified(id, edge) &&
!personInMinGroup.containsKey(edge.getPerson2().getId())) {
//System.out.println(edge);
value += edge.getValue();
person = (MyPerson) edge.getPerson2();
personInMinGroup.put(person.getId(), person);
edges.addAll(person.getEdges());
break;
}
}
}
return value;
} else {
throw new MyPersonIdNotFoundException(id);
}
}
2.2.3 最短路径
采用最短路径算法dijkstra，实现代码如下
HashMap<Integer, Person> vertexList = new HashMap<>();
HashMap<Person, Integer> sufNodes2Value = new HashMap<>();
PriorityQueue<Edge> edg = new PriorityQueue<>(Comparator.comparing(Edge::getValue));
vertexList.put(person1.getId(), person1);
for (Edge edge : person1.getEdges()) {
sufNodes2Value.put(edge.getPerson2(), edge.getValue());
Edge newEdge = new Edge(person1, edge.getPerson2(), edge.getValue());
edg.add(newEdge);
}
MyPerson person = (MyPerson) edg.poll().getPerson2();
while (!person.equals(person2)) { // when to quit ?
if (!vertexList.containsKey(person.getId())) {
vertexList.put(person.getId(), person);
int edgeValue = sufNodes2Value.get(person);
for (Edge newEdge : person.getEdges()) {
int value;
if (!vertexList.containsKey(newEdge.getPerson2().getId())) {
if (!sufNodes2Value.containsKey(newEdge.getPerson2()) ||
newEdge.getValue() + edgeValue <
sufNodes2Value.get(newEdge.getPerson2())) {
value = newEdge.getValue() + edgeValue;
sufNodes2Value.put(newEdge.getPerson2(), value);
edg.add(new Edge(person1, newEdge.getPerson2(), value));
}
}
}
}
person = (MyPerson) edg.poll().getPerson2();
}
三、分析代码实现出现的性能问题和修复情况
在对拍过程中，自己的代码跑的时间更长，简单分析之后，可能是因为一些方法我的实现是O(n)，并不会造成测试TLE，不过后来还是进行了优化和维护。
在优化过程中，也发现了一个会造成bug的点，在实现queryGroupAgeVar的时候，如果处理的顺序不当，由于int的取整，逻辑上与JML规格有出入。
错误的实现：
int ageMean = getAgeMean();
if (people.size() != 0) {
return (ageSquare - ageMean * ageMean * people.size()) / people.size();
}
正确的实现应该是(ageSquare - 2 * ageMean * ageSum + people.size() * ageMean * ageMean) / people.size();
四、对Network进行扩展，并给出相应的JML规格
假设出现了几种不同的Person
Advertiser：持续向外发送产品广告
Producer：产品生产商，通过Advertiser来销售产品
Customer：消费者，会关注广告并选择和自己偏好匹配的产品来购买
- 所谓购买，就是直接通过Advertiser给相应Producer发一个购买消息
Person：吃瓜群众，不发广告，不买东西，不卖东西
如此Network可以支持市场营销，并能查询某种商品的销售额和销售路径
增加的类：Producer、Advertiser、Customer、Advertise，其中Producer、Advertiser、Customer实现Person接口，Advertise糅合了产品和广告两类性质（这样应该不太好，但是能简化一下实现）
Advertise类中应该至少包含生产商Producer和广告商Advertiser，广告投放的群组Group，广告费用，产品售价，以及其他广告相关的信息。
Network类增加public instance model non_null Advertise[] productList、public instance model non_null Advertise[] advertiseList 属性。
- 产品生产商生产产品
Producer通过Advertiser来销售产品，于是Producer创造一个Advertise代表其销售的一类产品。
/*
@ public normal_behavior
@ requires !(\exists int i; 0 <= i && i < productList.length; productList[i].equals(product)) &&
@ (product.getGroup().hasPerson(product.getProducer())) &&
@ (product.getGroup().hasPerson(product.getAdvertiser()));
@ assignable productList;
@ assignable product.getProducer().money, product.getAdvertiser().money;
@ ensures productList.length == \old(productList.length) + 1;
@ ensures (\forall int i; 0 <= i && i < \old(productList.length);
@ (\exists int j; 0 <= j && j < productList.length; productList[j].equals(\old(productList[i]))));
@ ensures (\exists int i; 0 <= i && i < productList.length; productList[i].equals(product));
@ ensures product.getProducer().getMoney() == \old(product.getProducer().getMoney()) - product.getCommercialFee();
@ ensures product.getAdvertiser().getMoney() == \old(product.getAdvertiser().getMoney()) + product.getCommercialFee();
@ also
@ public exceptional_behavior
@ signals (EqualAdvertiseIdException e) (\exists int i; 0 <= i && i < productList.length;
@ productList[i].equals(product));
@ signals (ProducerIdNotFoundException e) !(\exists int i; 0 <= i && i < productList.length; productList[i].equals(product)) &&
@ !(product.getGroup().hasPerson(product.getProducer()));
@ signals (AdvertiserIdNotFoundException e) !(\exists int i; 0 <= i && i < productList.length; productList[i].equals(product)) &&
@ (product.getGroup().hasPerson(product.getProducer())) &&
@ !(product.getGroup().hasPerson(product.getAdvertiser()));
*/
addProduct(Advertise product) throws EqualAdvertiseIdException, ProducerIdNotFoundException, AdvertiserIdNotFoundException;
- Advertiser发送产品广告
/*
@ public normal_behavior
@ requires (\exists int i; 0 <= i && i < productList.length; productList[i].getId() == id) &&
@ !(\exists int i; 0 <= i && i < advertiseList.length; advertiseList[i].getId() == id)
@ assignable advertiseList, productList;
@ ensures !(\exists int i; 0 <= i && i < productList.length; productList[i].getId() == id) &&
@ productList.length == \old(productList.length) - 1 &&
@ (\forall int i; 0 <= i && i < \old(productList.length) && \old(productList[i].getId()) != id;
@ (\exists int j; 0 <= j && j < productList.length; productList[j].equals(\old(productList[i]))));
@ ensures (\exists int i; 0 <= i && i < advertiseList.length; advertiseList[i].getId() == id) &&
@ advertiseList.length == \old(advertiseList.length) + 1 &&
@ (\forall int i; 0 <= i && i < \old(advertiseList.length) && \old(advertiseList[i].getId()) != id;
@ (\exists int j; 0 <= j && j < advertiseList.length; advertiseList[j].equals(\old(advertiseList[i]))));
@ also
@ public exceptional_behavior
@ signals (ProductIdNotFoundException e) !(\exists int i; 0 <= i && i < productList.length; productList[i].getId() == id);
@ signals (EqualAdvertiseIdException e) (\exists int i; 0 <= i && i < productList.length; productList[i].getId() == id) &&
@ (\exists int i; 0 <= i && i < advertiseList.length; advertiseList[i].getId() == id);
*/
sendAdvertise(int id) throws ProductIdNotFoundException, EqualAdvertiseIdException;
- 消费者购买产品
/*
@ public normal_behavior
@ requires (\exists int i; 0 <= i && i < advertiseList.length; advertiseList[i].getId() == advertiseId) &&
@ getAdvertise(advertiseId).getGroup.hasPerson(getPerson(personId));
@ assignable getAdvertise(advertiseId).getProducer().money, getPerson(personId).money;
@ ensures getAdvertise(advertiseId).getProducer().getMoney() == \old(getAdvertise(advertiseId).getProducer().getMoney()) + getAdvertise(advertiseId).getProductPrice();
@ ensures getPerson(personId).getMoney() == \old(getPerson(personId).getMoney()) - getAdvertise(advertiseId).getProductPrice();
@ also
@ public exceptional_behavior
@ signals (AdvertiseIdNotFoundException e) !(\exists int i; 0 <= i && i < advertiseList.length; advertiseList[i].getId() == advertiseId);
@ signals (PersonIdNotFoundException e) (\exists int i; 0 <= i && i < advertiseList.length; advertiseList[i].getId() == advertiseId) &&
@ !getAdvertise(advertiseId).getGroup.hasPerson(getPerson(personId));
*/
buyProduct(int personId, int advertiseId) throws AdvertiseIdNotFoundException, PersonIdNotFoundException;
有待开发的功能：生产商决定投放广告数量，生产产品的数量，商品销售额及销售路径的查询功能……
五、本单元学习体会
本单元学习了JML的契约式编程，因为不需要自己设计架构，难度比前两单元要友好一些。最主要的收获是能够读懂并实现JML规格，而对于自己写JML规格的能力，这一方面仍然很薄弱，仅在实验和讨论部分进行了少量的训练学习。
通过对JML的学习，我体会到JML对前置条件和后置条件的严格定义使得实现和维护代码变得容易，不再会担心产生新的神秘bug令人秃头，除了实现的正确性以外，只需要考虑性能问题。
标签：OO,int,random,BUAA,id1,person,edge,2022,ar 来源： https://www.cnblogs.com/cchanghhh/p/16347686.html