OO第三单元总结
作者：互联网
OO第三单元总结
利用JML规格准备测试数据
-
前置条件
-
构造不满足前置条件的数据测试异常处理
-
构造满足前置条件的数据测试正确性
-
-
后置条件和约束条件
-
用于判断输出结果的正确性
-
利用JML规格的前置条件构造数据便于对所有可能的情况进行分类讨论，保障了测试数据的覆盖率。但仅用后置条件和约束条件对结果进行判断无法保证结果完全正确，仍需要对拍。此外，对于代码性能的检测也需要额外构造数据。
图模型构建和维护策略
-
构建Edge类，用于表示一条边，包含以下3个属性
private final int value; //边的权重
private final int id1; //顶点1
private final int id2; //顶点2 -
构建Block类，用于表示一个连通块，包含以下2个属性
private final ArrayList<Integer> people = new ArrayList<>(); //连通块内所有人的id
private final ArrayList<Edge> edges = new ArrayList<>(); //连通块内所有边
-
在Network中添加属性fatherMap，用于表示每个人的父节点（自身以及所有邻接点中id最小的点）
HashMap<Integer, Integer> fatherMap = new HashMap<>(); //personId -> fatherId
-
可以通过findRoot找到根节点，每一个Block中所有点具有相同的根节点，因此可以构建HashMap通过根节点找到对应的Block
private int findRoot(int id) {
int cur = id;
while (cur != fatherMap.get(cur)) {
cur = fatherMap.get(cur);
}
return cur;
}
private final HashMap<Integer, Block> blocks = new HashMap<>(); //root -> block
-
每当addPerson时，新建一个Block，将（id, id）添加到fatherMap中
-
addRelation时，比较并更新fatherMap，向Block中添加新的Egde，并判断是否需要合并Block
queryLeastConnection
先找到节点所在的Block，然后采用kruskal算法计算最小生成树
public int queryLeastConnection() {
if (changed) {
Collections.sort(edges); //对所有边按权重从小到大排序
HashMap<Integer, Integer> fatherMap = new HashMap<>();
leastConnection = 0;
int edgeNum = 0; //已经加入的边的数量，最大为people.size - 1
for (Edge edge : edges) { //遍历所有边
int root1 = findRoot(fatherMap, edge.getId1()); //找到两个顶点的根节点
int root2 = findRoot(fatherMap, edge.getId2());
if (root1 != root2) { //保证不构成回路
if (root1 > root2) {
fatherMap.put(root1, root2);
} else {
fatherMap.put(root2, root1);
}
leastConnection += edge.getValue();
edgeNum++;
if (edgeNum == people.size() - 1) { //已经构成最小生成树
break;
}
}
}
changed = false;
}
return leastConnection;
}
sendIndirectMessage
通过findRoot找到对应的Block，并调用getStep采用Dijkstra算法计算最短路径
public int getStep(PersonClass person1, PersonClass person2) {
HashMap<Person, Integer> net = new HashMap<>(person1.getAcquaintance());
//person1所有能到达的节点，以及对应的路径长度
HashMap<Person, Integer> queue = new HashMap<>(person1.getAcquaintance());
//未找到最短路径的节点的队列，以及当前到达person1的路径长度
for (int layer = 0;layer < people.size();layer++) {
Integer min = null;
PersonClass target = null;
for (Person i : queue.keySet()) { //从queue中寻找离person1最近的节点
if ((min == null) || (queue.get(i) < min)) {
min = queue.get(i);
target = (PersonClass) i;
}
}
assert target != null;
assert min != null;
if (target.equals(person2)) { //找到person2，可以返回
return net.get(person2);
}
queue.remove(target); //从queue中删除已经找到最短路径的节点
for (Person i : target.getAcquaintance().keySet()) {
if ((net.get(i) == null) || (net.get(i) > min + i.queryValue(target))) {
//需要更新路径长度的节点
net.put(i, min + i.queryValue(target)); //更新路径
queue.put(i, min + i.queryValue(target)); //加入队列
}
}
}
return net.get(person2);
}
性能问题
getAgeVar
计算AgeVar时，可以根据每个人年龄的平方和以及平均数得到，在addPerson和delPerson的时候对ageVarSum和ageMeanSum进行更新，降低了getAgeVar的复杂度。但需要注意/表示整除，除法和加法的顺序不同可能会导致结果不同。
public int getAgeVar() {
if (people.size() == 0) {
return 0;
} else {
int mean = getAgeMean();
return (ageVarSum - 2 * ageMeanSum * mean + mean * mean * people.size())
/ people.size();
}
}
queryGroupValueSum
在addPerson和depPerson时，更新group中的valueSum
for (Person i : people) { //addPerson
valueSum += i.queryValue(person);
}
for (Person i : people) { //delPerson
valueSum -= i.queryValue(person);
}
并在addRelation时遍历所有group，更新valueSum
for (Group group : groups.values()) {
if (group.hasPerson(people.get(id1)) && group.hasPerson(people.get(id2))) {
//group中同时包含person1和person2
((GroupClass) group).addValue(value);
}
}
Network扩展
-
Advertiser，Producer和Customer接口都继承Person；广告和购买消息继承Message，假设他们为AdMessage和BuyMessage
-
构建Product类，表示一种产品，包含属性id，price（定价）和sales（销量）并保证每种产品的id不同。在Network中增加Product[] products表示各种产品。
-
Producer包含Product[] products和int[] number，分别表示生产商生产的产品种类和对应的数量。生产之前需要将Network中对应的产品种类添加到products
-
Advertiser只能给acquaintance list中的Producer做广告商，发送特定的广告。且只能发送给acquaintance list中的Customer，AdMessage中包括产品种类product和相应的Producer
-
Customer中包含属性Product[] prefer表示顾客偏好的产品种类，顾客购买产品会根据收到的AdMessage，选择匹配prefer的产品种类，向对应的Producer发送BuyMessage，BuyMessage中包含产品种类product和购买数量number
Advertiser发送AdMessage
/*@ public normal_behavior
@ requires containsMessage(id) && getMessage(id) instanceof AdMessage) &&
@ getMessage(id).getType() == 0 &&
@ getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
@ getMessage(id).getPerson1() != getMessage(id).getPerson2() &&
@ getMessage(id).getPerson1().isLinked(getMessage(id).producer) &&
@ getMessage(id).producer.contains(getMessage(id).product);
@ assignable messages;
@ assignable getMessage(id).getPerson1().socialValue;
@ assignable getMessage(id).getPerson2().messages,
@ getMessage(id).getPerson2().socialValue;
@ ensures !containsMessage(id) && messages.length == \old(messages.length) - 1 &&
@ (\forall int i; 0 <= i && i < \old(messages.length) &&
@ \old(messages[i].getId()) != id;
@ (\exists int j; 0 <= j && j < messages.length;
@ messages[j].equals(\old(messages[i]))));
@ ensures \old(getMessage(id)).getPerson1().getSocialValue() ==
@ \old(getMessage(id).getPerson1().getSocialValue()) +
@ \old(getMessage(id)).getSocialValue() &&
@ \old(getMessage(id)).getPerson2().getSocialValue() ==
@ \old(getMessage(id).getPerson2().getSocialValue()) +
@ \old(getMessage(id)).getSocialValue();
@ also
@ public exceptional_behavior
@ signals (MessageIdNotFoundException e) !containsMessage(id) ||
@ !(getMessage(id) instanceof AdMessage) ||
@ !(getMessage(id).getType() == 0);
@ signals (RelationNotFoundException e) containsMessage(id) &&
@ (getMessage(id) instanceof AdMessage) &&
@ getMessage(id).getType() == 0 &&
@ (!getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) ||
@ !getMessage(id).getPerson1().isLinked(getMessage(id).producer))
@ signals (ProductIdNotFoundException e) containsMessage(id) &&
@ (getMessage(id) instanceof AdMessage) &&
@ getMessage(id).getType() == 0 &&
@ getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
@ getMessage(id).getPerson1() != getMessage(id).getPerson2() &&
@ getMessage(id).getPerson1().isLinked(getMessage(id).producer) &&
@ !getMessage(id).producer.contains(getMessage(id).product);
@*/
public void sendAdMessage(int id) throws
RelationNotFoundException, MessageIdNotFoundException,
ProductIdNotFoundException;
Customer发送BuyMessage
/*@ public normal_behavior
@ requires containsMessage(id) && getMessage(id).getType() == 0 &&
@ getMessage(id) instance of BuyMessage &&
@ getMessage(id).getPerson1 instance of Customer &&
@ (\exist int i;0 <= i && i < getMessage(id).getPerson1.prefer.length;
@ getMessage(id).getPerson1.prefer[i] == getMessage(id).product) &&
@ getMessage(id).getPerson2 instance of Producer &&
@ (\exist int i;0 <= i && i < getMessage(id).getPerson2.products.length;
@ getMessage(id).getPerson2.products[i] == getMessage(id).product) &&
@ (!(\exist Person i; i instance of Advertiser &&
@ (\exist int j;0 <= j && j < getMessage(id).getPerson1.acquaintance.length;
@ getMessage(id).getPerson1.acquaintance[j] == i) &&
@ (\exist int k;0 <= k && k < getMessage(id).getPerson2.acquaintance.length;
@ getMessage(id).getPerson2.acquaintance[k] == i)) ||
@ getMessage(id).getPerson2.getProductNum(getMessage(id).product) <
@ getMessage(id).num ||
@ getMessage(id).getPerson1.money < getMessage(id).product.price);
@ ensures \result == -1;
@ also
@ public normal_behavior
@ requires containsMessage(id) && getMessage(id).getType() == 0 &&
@ getMessage(id) instance of BuyMessage &&
@ getMessage(id).getPerson1 instance of Customer &&
@ (\exist int i;0 <= i && i < getMessage(id).getPerson1.prefer.length;
@ getMessage(id).getPerson1.prefer[i] == getMessage(id).product) &&
@ getMessage(id).getPerson2 instance of Producer &&
@ (\exist int i;0 <= i && i < getMessage(id).getPerson2.products.length;
@ getMessage(id).getPerson2.products[i] == getMessage(id).product) &&
@ (\exist Person i; i instance of Advertiser &&
@ (\exist int j;0 <= j && j < getMessage(id).getPerson1.acquaintance.length;
@ getMessage(id).getPerson1.acquaintance[j] == i) &&
@ (\exist int k;0 <= k && k < getMessage(id).getPerson2.acquaintance.length;
@ getMessage(id).getPerson2.acquaintance[k] == i)) &&
@ getMessage(id).getPerson2.getProductNum(getMessage(id).product) >=
@ getMessage(id).num &&
@ getMessage(id).getPerson1.money >= getMessage(id).product.price;
@ assignable messages, getMessage(id).product;
@ assignable getMessage(id).getPerson1().socialValue,
@ getMessage(id).getPerson1().money;
@ assignable getMessage(id).getPerson2().messages, getMessage(id).getPerson2().money,
@ getMessage(id).getPerson2().socialValue;
@ ensures !containsMessage(id) && messages.length == \old(messages.length) - 1 &&
@ (\forall int i; 0 <= i && i < \old(messages.length) &&
@ \old(messages[i].getId()) != id;
@ (\exists int j; 0 <= j && j < messages.length;
@ messages[j].equals(\old(messages[i]))));
@ ensures \old(getMessage(id)).getPerson1().getSocialValue() ==
@ \old(getMessage(id).getPerson1().getSocialValue()) +
@ \old(getMessage(id)).getSocialValue() &&
@ \old(getMessage(id)).getPerson2().getSocialValue() ==
@ \old(getMessage(id).getPerson2().getSocialValue()) +
@ \old(getMessage(id)).getSocialValue();
@ ensures (\forall int i; 0 <= i && i <
@ \old(getMessage(id).getPerson2().getMessages().size());
@ \old(getMessage(id)).getPerson2().getMessages().get(i+1) ==
@ \old(getMessage(id).getPerson2().getMessages().get(i)));
@ ensures
@ \old(getMessage(id)).getPerson2().getMessages().get(0).equals(\old(getMessage(id)));
@ ensures \old(getMessage(id)).getPerson2().getMessages().size() ==
@ \old(getMessage(id).getPerson2().getMessages().size()) + 1;
@ ensures (\old(getMessage(id)).getPerson1().getMoney() ==
@ \old(getMessage(id).getPerson1().getMoney()) -
@ \old(getMessage(id)).product.price * \old(getMessage(id).num);
@ ensures (\old(getMessage(id)).getPerson2().getMoney() ==
@ \old(getMessage(id).getPerson2().getMoney()) +
@ \old(getMessage(id)).product.price * \old(getMessage(id).num);
@ ensures \old(getMessage(id)).product.sales += \old(getMessage(id).num;
@ also
@ public exceptional_behavior
@ signals (MessageIdNotFoundException e) !containsMessage(id) ||
@ getMessage(id).getType() != 0 ||
@ !getMessage(id) instance of BuyMessage ||
@ !getMessage(id).getPerson1 instance of Customer ||
@ !(\exist int i;0 <= i && i < getMessage(id).getPerson1.prefer.length;
@ getMessage(id).getPerson1.prefer[i] == getMessage(id).product) ||
@ !getMessage(id).getPerson2 instance of Producer
@ signals (ProductIdNotFoundException e) containsMessage(id) &&
@ getMessage(id).getType() == 0 &&
@ getMessage(id) instance of BuyMessage &&
@ getMessage(id).getPerson1 instance of Customer &&
@ (\exist int i;0 <= i && i < getMessage(id).getPerson1.prefer.length;
@ getMessage(id).getPerson1.prefer[i] == getMessage(id).product) &&
@ getMessage(id).getPerson2 instance of Producer &&
@ !(\exist int i;0 <= i && i < getMessage(id).getPerson2.products.length;
@ getMessage(id).getPerson2.products[i] == getMessage(id).product)
@*/
public int sendIndirectMessage(int id) throws
MessageIdNotFoundException, ProductIdNotFoundException;
查询销售额
/*@ public normal_behavior
@ requires (\exists int i; 0 <= i && i < productIdList.length; productIdList[i] == id);
@ ensures (\exists int i; 0 <= i && i < productIdList.length; productIdList[i] == id &&
@ \result == productIdList[i].price * productIdList[i].sales);
@ also
@ public exceptional_behavior
@ requires !(\exists int i; 0 <= i && i < productIdList.length;
@ productIdList[i] == id);
@ signals_only ProductIdNotFoundException;
@*/
public /*@ pure @*/ int querySales(int id) throws ProductIdNotFoundException;
标签：OO,总结,old,getPerson2,int,getMessage,&&,id,单元 来源： https://www.cnblogs.com/rrmmffll/p/16341310.html