OO 第三单元总结
规格的阅读与实现心得
JML的阅读方法
- 语法上， 可以参考课程组的《JML level0手册》， 涵盖了基本的jml关键词和语法，看不明白的话可以多翻翻，类比着就搞懂了
- 阅读顺序上， 阅读JML可以从一些比较底层的类开始读， 比如
Person,Message这种依赖关系比较少的类， 可以先读起来，这样对一个类的功能就可以很快的了解 - 阅读tips : Idea对于JML高亮支持其实很不好（基本没有啊喂）推荐在vscode上装好插件在上面阅读，
还可以对Idea注释调颜色，这样至少看起来清楚一点不会灰糊糊的一团
JML迭代
每次迭代推荐用Idea 鼠标右键的compare with clipboard, 比较一下差异， 同时注意一下一些坑人限制条件比如1111
测试数据与JML
本单元一开始想试试单元测试的，但咨询了一下学长们，似乎都不太推荐JUNIT, OPENJML等基于JML的测试， 后来经过尝试确实有点麻烦。OpenJml 就是个jml语法检查器（bushi, Junit有点像Verilog的testbench样例还需要自己构造，如果能够有一个可以根据JML直接校验函数的工具就好了
剩下的日子里， 就都在写对拍机了，在构造测试数据时， JML的存在也可以使测试数据的覆盖率提高， 就比如am指令的构造
/*@ public normal_behavior
@ requires !(\exists int i; 0 containsEmojiId(((EmojiMessage) message).getEmojiId()) &&
@ (message.getType() == 0) ==> (message.getPerson1() != message.getPerson2());
@ assignable messages;
@ ensures messages.length == \old(messages.length) + 1;
@ ensures (\forall int i; 0
@ containsEmojiId(((EmojiMessage) message).getEmojiId())) &&
@ message.getType() == 0 && message.getPerson1() == message.getPerson2();
@*/
## 依据JML构造数据来覆盖所有可能分支 ##
def am():
ty = random.randint(0, 1)
sv = random.choice(extreme_sv_pool)
if random.randint(0, excRate) == 1: # emi
try:
id = random.choice(list(message_pool.keys()))
except:
id = random.randint(idmin, idmax)
if ty == 0:
try: # {id:{type:, pid1:, pid2:, sv:, gid:,}}
if random.randint(0, excRate) == 1:
# 在sm时会触发异常：
# epi & pinf情况， 异常可控
if random.randint(0, 2) == 1:
pid1 = pid2 = random.choice(list(person_pool.keys())) # epi
else:
pid1 = pid2 = random.randint(idmin, idmax) # pinf when send
elif random.randint(0, 2 * excRate) == 1:
pid1 = random.randint(idmin, idmax)
pid2 = random.randint(idmin, idmax)
else:
pid1, pid2 = random.sample(list(person_pool.keys()), 2)
# ADD! 真正加入， 用一点数据结构记录
message_pool[id] = {"type": ty, "sv": sv, "pid1": pid1, "pid2": pid2, "gid": None, "div": "am"}
except:
pid1 = random.randint(idmin, idmax)
pid2 = random.randint(idmin, idmax)
return "am {} {} {} {} {}".format(id, sv, ty, pid1, pid2)
else:
# pinf ginf 情况 覆盖了所有异常，进行测试
if random.randint(0, excRate) == 1:
pid1 = random.randint(idmin, idmax)
gid = random.randint(idmin, idmax)
else:
pid1 = random.choice(list(person_pool.keys()))
try:
gid = random.choice(list(group_pool.keys()))
except:
return ag()
# ADD! 真正的加入
message_pool[id] = {"type": ty, "sv": sv, "pid1": pid1, "pid2": None, "gid": gid, "div": "am"}
return "am {} {} {} {} {}".format(id, sv, ty, pid1, gid)
else:
id = random.randint(idmin, idmax)
if ty == 0:
try:
if random.randint(0, excRate) == 1: # epi
if random.randint(0, 2) == 1:
pid1 = pid2 = random.choice(list(person_pool.keys()))
else:
pid1 = pid2 = random.randint(idmin, idmax)
elif random.randint(0, 2 * excRate) == 1:
pid1 = random.randint(idmin, idmax)
pid2 = random.randint(idmin, idmax)
else:
pid1, pid2 = random.sample(list(person_pool.keys()), 2)
except:
pid1 = random.randint(idmin, idmax)
pid2 = random.randint(idmin, idmax)
message_pool[id] = {"type": ty, "sv": sv, "pid1": pid1, "pid2": pid2, "gid": None, "div": "am"}
return "am {} {} {} {} {}".format(id, sv, ty, pid1, pid2)
else:
pid1 = random.choice(list(person_pool.keys()))
try:
gid = random.choice(list(group_pool.keys()))
message_pool[id] = {"type": ty, "sv": sv, "pid1": pid1, "pid2": None, "gid": gid, "div": "am"}
return "am {} {} {} {} {}".format(id, sv, ty, pid1, gid)
except:
return ag()
容器的选择
一些容器和我的选择， 因为一些容器需要O(1)的查询效率， 那么 Hashmap是最好的选择
第三次作业中， Message的存储满足的是一个FIFO的规则， 所以用了 linkedlist
Exception
private int id; //personId触发了异常
private static int totalExcCnt = 0;
private static HashMap excTable = new HashMap<>();
// 触发的personId - 触发的次数
Group
private HashMap people = new HashMap<>();
// id - person
Person
private HashMap linkage = new HashMap<>();
// 邻居Person - distance
private LinkedList messages = new LinkedList<>();
// Person收到的信息
Network
private HashMap people = new HashMap<>();
private HashMap groups = new HashMap<>();
private HashMap messages = new HashMap<>();
private HashMap emojiHeatMap = new HashMap<>();
// 上述皆为 的Hashmap, O(1)查找不错的
private HashSet edges = new HashSet<>();
// Edge是我自己定义的边类， edges记录了所有的边， kruskal的时候会比较方便
private MyDsu dsu = new MyDsu<>();
// Dsu是我自己写的优化完全的并查集类， 支持不同模板很好用
算法和性能分析
本单元有一些需要注意算法时间复杂度的点
- 维护
valueSum，ageSum，ageSquareSum如果要求ageVar那么为了保证精度与jml一致， 自己推一下就好
return (timeSum - 2 * ageSum * getAgeMean() + getAgeMean() * getAgeMean() * people.size()) / people.size();
////////////////////////////////////////////////////////////////////
BigInteger part1 = ageSquareSum;
BigInteger part2 = (new BigInteger("2")).multiply(ageSum)
.multiply(BigInteger.valueOf(getAgeMean()));
BigInteger part3 = BigInteger.valueOf(getAgeMean()).multiply(BigInteger.valueOf(getAgeMean()))
.multiply(BigInteger.valueOf(people.size()));
BigInteger result = (part1.subtract(part2).add(part3)).divide(BigInteger.valueOf(people.size()));
return result.intValue();
需要注意的是： valueSum是将每对关系计算两次，需要在每次加人时 valueSum加 2 * value。除了在加人删人外，在添加关系时需要遍历所有 group维护 valueSum。(别忘了哦！)
2. Kruskal算法， 需要提前维护所有的边集， 然后遍历边集找到所有在联通分量的边。这样可以实现O(ElogE)的复杂度， 如果不存储需要用iscircle再查找可能会慢
3. isCircle方法, 要用路径压缩+合并秩优化的并查集， 鉴于网上似乎还没有java版的，我给一个吧嘿嘿
import java.util.HashMap;
public class MyDsu {
private HashMap fatherMap = new HashMap<>();
private HashMap rankMap = new HashMap<>();
public MyDsu() {
}
public void addElement(T a) {
fatherMap.put(a, a);
rankMap.put(a, 1);
}
public T findRoot(T a) {
T r = a;
while (fatherMap.get(r) != r) {
r = fatherMap.get(r);
}
T i = a;
T tmp;
while (i != r) {
tmp = fatherMap.get(i);
fatherMap.put(i, r);
i = tmp;
}
return r;
}
public void unionSet(T a, T b) {
if (a == null || b == null) {
return;
}
T root1 = findRoot(a);
T root2 = findRoot(b);
if (rankMap.get(root1) == rankMap.get(root2)) {
fatherMap.put(root2, root1); //root 1 is fa
rankMap.put(root1, rankMap.get(root1) + 1);
} else {
if (rankMap.get(root1) < rankMap.get(root2)) {
fatherMap.put(root1, root2);
} else {
fatherMap.put(root2, root1);
}
}
}
}
- DeleteColdEmoji 如果是按着jml的逻辑， 先遍历
heatmap找到对应待删除的emojiMessage, 那么针对每一个emoji,都要遍历一遍整个messages显然复杂度较大。正常想法就是先遍历messages再遍历heatmap, 那么就可以O(n)解决问题 - dijkstra算法 注意可以使用堆优化， 并使用一个内部类
node来记录相关节点信息
public class Dijkstra {
public class Node implements Comparable {
private int dis = 0;
private int id = 0;
public int getDis() {
return dis;
}
public int getId() {
return id;
}
public Node(int id, int dis) {
this.dis = dis;
this.id = id;
}
@Override
public int compareTo(Node o) {
return Integer.compare(this.getDis(), o.getDis());
}
}
//
private HashMap dis = new HashMap<>();
//
private HashMap done = new HashMap<>();
//
private HashMap people;
private PriorityQueue queue = new PriorityQueue<>();
public Dijkstra(HashMap people) {
this.people = people;
for (Map.Entry personEntry : people.entrySet()) {
int id = personEntry.getKey();
dis.put(id, (int) 1e9);
done.put(id, false);
}
}
public int run(int fromId, int toId) {
//算法本体
}
}
Network 扩展考虑
题目要求
假设出现了几种不同的Person
- Advertiser：持续向外发送产品广告
- Producer：产品生产商，通过Advertiser来销售产品
- Customer：消费者，会关注广告并选择和自己偏好匹配的产品来购买 — 所谓购买，就是直接通过Advertiser给相应Producer发一个购买消息
- Person：吃瓜群众，不发广告，不买东西，不卖东西
如此Network可以支持市场营销，并能查询某种商品的销售额和销售路径等 请讨论如何对Network扩展，给出相关接口方法，并选择3个核心业务功能的接口方法撰写JML规格（借鉴所总结的JML规格模式）
首先我设计：
- 在Message下新增加
Advertisement类， 其中包含了attraction代表广告吸引力，其余属性类似于message分群发、私发等 - 新增加Product类用于买卖，宣传, 内置属性
storage,salesAmount - productList[]保存着当前的product
- 每个person(作为吃瓜群众，也会收到广告) 其中可以通过getInterest(Product p) 来获取对p的a兴趣
/*@ public normal_behavior
@ requires containsMessage(id) && getMessage(id).getType() == 0 &&
@ getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
@ getMessage(id).getPerson1() != getMessage(id).getPerson2();
@ assignable messages, emojiHeatList; +
@ assignable getMessage(id).getPerson1().socialValue, getMessage(id).getPerson1().money;
@ assignable getMessage(id).getPerson2().messages, getMessage(id).getPerson2().socialValue, getMessage(id).getPerson2().money,
getMessage(id).getPerson2().interests;
@ ensures (\old(getMessage(id)) instance of Advertisement) ==>
@ (\old(getMessage(id)).getPerson1().getInterest(Advertisement.getProduct()) ==
@ \old(getMessage(id).getPerson1().getInterest(Advertisement.getProduct())) + ((Advertisement)\old(getMessage(id))).getAttraction()
@ ensures (!(\old(getMessage(id)) instanceof Advertisement)) ==> (\not_assigned(people[*].getInterest(Product[*]));
......略
@
@ also
@ public normal_behavior
@ requires containsMessage(id) && getMessage(id).getType() == 1 &&
@ getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1());
@ assignable people[*].socialValue, people[*].money, people[*].interests
messages, emojiHeatList;
......略
@ ensures (\old(getMessage(id)) instance of Advertisement) ==>
@ (\exists int i; i == ((Advertisement)\old(getMessage(id))).getAttraction();
@ (\forall Person p; \old(getMessage(id)).getGroup().hasPerson(p) && p != \old(getMessage(id)).getPerson1();
@ p.getInterest(Advertisement.getProduct()) == \old(p.getInterest(Advertisement.getProduct())) + i));
@ ensures (!(\old(getMessage(id)) instanceof Advertisement)) ==> (\not_assigned(people[*].getInterest(Product[*]));
......略
@ also
@ public exceptional_behavior
@ signals (MessageIdNotFoundException e) !containsMessage(id);
@ signals (RelationNotFoundException e) containsMessage(id) && getMessage(id).getType() == 0 &&
@ !(getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()));
@ signals (PersonIdNotFoundException e) containsMessage(id) && getMessage(id).getType() == 1 &&
@ !(getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1()));
@*/
public void sendMessage(int id) throws
RelationNotFoundException, MessageIdNotFoundException, PersonIdNotFoundException;
// Customer
/*@ public normal_behavior
@ requires contains(producerId);
@ requires !(\exists int i; 0
架构分析
本单元作业架构已经由课程组给出，无需多分析，重要的是阅读jml和采取合适的数据结构和算法来实现。
体会感想
整个单元其实期待还是很高的。但是整个单元学下来， 似乎所有的时间都用在读jml上了， 图论算法也不算难，感谢助教的怜悯，其实希望有个jml直接对接检查代码的说，结果似乎没有，感觉jml的威力瞬间减少了不少。 三次作业难得全满挺不错的，希望下次继续努力！
Original: https://www.cnblogs.com/cywuuuu/p/16303312.html
Author: cywuuuu
Title: OO 第三单元总结
原创文章受到原创版权保护。转载请注明出处：https://www.johngo689.com/714001/
转载文章受原作者版权保护。转载请注明原作者出处！