第三单元整体目标为实现简单社交关系的模拟和查询,让我们了解了基本的JML语法和语义,以及具备根据JML给出的规格编写Java代码的能力。
在此仅放出最后一次作业的类图,且去掉了实现的异常类。
本单元作业实现给出每个类的结构以及方法规格,只要按照规格实现方法即可,但是为了便于部分方法的实现,仍可以实现其他类,例如算法工具类等等。在本单元最后我在原有类基础上实现了Edge
类用来保存添加关系后的两个人及关系的权值,便于最小生成树的生成,还多加了Node
类,便于最短路径的查询。
在第九次作业中qci
指令要求查询图中两个点是否是连通的。为此使用了路径压缩的并查集来实现,避免所有人都有联系时连成一条线的特殊情况。
private HashMap<Integer, Integer> parent = new HashMap<>();//并查集的根节点 private HashMap<Integer, Integer> rank = new HashMap<>();//树高 public int find(int id) { int newId = id; while (newId != parent.get(newId)) { newId = parent.get(newId); } return newId; } public void unionElements(int id1, int id2) { int id1Root = find(id1); int id2Root = find(id2); if (id1Root == id2Root) { return; } if (rank.get(id1Root) < rank.get(id2Root)) { parent.put(id1Root, id2Root); } else if (rank.get(id1Root) > rank.get(id2Root)) { parent.put(id2Root, id1Root); } else { parent.put(id1Root, id2Root); rank.put(id2Root, rank.get(id2Root) + 1); } }
第十次作业中难点在于qlc
指令,用于查询包含要查询顶点的最小生成树的边的权值之和,为此使用了并查集优化的kruskal
算法,用Edge
类保存人之间的联系,便于排序查找。
HashMap<Integer, Integer> innerParent = new HashMap<>();//并查集的根节点 保存与id相连通的节点 HashMap<Integer, Integer> innerRank = new HashMap<>(); for (int key : people.keySet()) { if (find(key) == find(id)) { innerParent.put(key, key); innerRank.put(key, 1); } } Collections.sort(edges); for (Edge edge : edges) { if (innerParent.containsKey(edge.getBegin())) { int m = find(innerParent, edge.getBegin()); int n = find(innerParent, edge.getEnd()); if (m != n) { unionElements(innerParent, innerRank, m, n); sum += edge.getWeight(); num++; } if (num == innerParent.size() - 1) { break; } } }
第十一次作业中难点为qmi
指令,用于查询两个点之间的最短路径权值之和,在此使用堆优化的Dijkstra算法,用Node
类保存所查询的点到终点的距离,利用PriorityQueue
来保存路径,降低复杂度。
HashMap<Integer, Node> nodes = new HashMap<>();//到达id的点的路径 即已遍历的点 //ArrayList<Node> untrackedNodes = new ArrayList<>();//未跟踪的边 包括长的和新更新的 PriorityQueue<Node> untrackedNodes = new PriorityQueue<>(); untrackedNodes.add(new Node(person1, 0)); while (!untrackedNodes.isEmpty()) { /*paths.size() < queryPeopleSum() && */ //Node untrackedNode = untrackedNodes.get(0); //untrackedNodes.remove(0); Node untrackedNode = untrackedNodes.poll(); MyPerson temporaryShortestPath = (MyPerson) untrackedNode.getNode();//未追踪的最小边的终点 if (!nodes.containsKey(temporaryShortestPath.getId())) { nodes.put(temporaryShortestPath.getId(), untrackedNode); if (temporaryShortestPath.getId() == person2.getId()) { break; } else { for (Integer next : temporaryShortestPath.getAcquaintance().keySet()) { Node pathToNext = nodes.get(next); if (pathToNext == null) { int distance = untrackedNode.getDistance(); int value = temporaryShortestPath.queryValue(getPerson(next)); untrackedNodes.add(new Node(getPerson(next), distance + value)); } } //Collections.sort(untrackedNodes); } } }
qbs
指令。在实现了并查集的情况下,没有意识到联通分支的数量等于满足自己即是自己的父结点的结点个数,按照了规格里给出的方法实现,导致时间复杂度为O(n2),在多次查询qbs
指令时会出现cpu超时的情况。qgvs
指令,在互测中因为这个被hack了多次。按照JML规格里给出的实现方法,时间复杂度为O(n2),为了避免多次查询时的超时,维护了一个valueSum
的变量,将查询的时间分散在将人加入群组时增加valueSum
的值,在删除时减少valueSum
的值,同时在加关系时在同时有关系两人的群组中增加valueSum
的值,这样在查询qgvs
指令时直接给出valueSum
的值即可。由之前的分析可以看出,此单元的测试需要从两方面进行,一个是正确性测试,另一个则是性能测试。
对于正确性测试,首先尝试了指导书中推荐的JUnit
来测试,在刚开始尝试时觉得效果还不错,但在函数数量较多的情况下,对每一个函数手动构造数据过于复杂,于是采取生成随机数据与他人对拍来验证正确性问题。按照此方法检测程序正确性效果不错,不需要很多次即可发现问题。
对于性能测试,首先需要增加输出cpu运行时间的部分,其次在随机生成测试数据时对一些特定指令增加关注,比如增加此类指令的数量等等方法,但正因为如此,将注意力都放在了在实现时较为困难的指令,很容易忽略一些较为简单的指令,例如之前出现的qgvs
指令,就是因为没有对其进行较强的测试导致的。
Advertiser
,Producer
,Customer
实现Person
子接口Product
Network
:
addAdvertiser
、addProducer
、addCustomr
等方法queryProductSales
方法——查询对应ProducerId
的产品的销售额;queryProductPath
方法——查询ProducerId
的产品的销售路径sendBuyingMessage
方法——Customer
向Advertiser
发送购买需求;sendAdvertiseMessage
方法——Advertiser
向Customer
发送广告JML
规格addAdvertiser
/*@ public normal_behavior @ requires !(\exists int i; 0 <= i && i < advertisers.length; advertisers[i].equals(advertiser)); @ assignable advertisers; @ ensures advertisers.length == \old(advertisers.length) + 1; @ ensures (\forall int i; 0 <= i && i < \old(advertisers.length); @ (\exists int j; 0 <= j && j < advertisers.length; advertisers[j] == @ (\old(advertisers[i])))); @ ensures (\exists int i; 0 <= i && i < advertisers.length; advertisers[i] == advertiser); @ also @ public exceptional_behavior @ signals (EqualAdvertiserIdException e) (\exists int i; 0 <= i && i < advertisers.length; @ advertisers[i].equals(advertiser)); @*/ public void addAdvertiser(/*@ non_null @*/Advertiser advertiser) throws EqualAdvertiserIdException;
queryProductSales
/*@ public normal_behavior @ requires containsProduct(id); @ ensures \result == getProduct(id).getSale(); @ also @ public exceptional_behavior @ signals (ProductIdNotFoundException e) !containsProduct(id); @*/ public /*@ pure @*/ int queryProductSales(int id) throws ProductIdNotFoundException;
sendAdvertiseMessage
/*@ public nomal_behavior @ requires containsMessage(id) && (getMessage(id) instance of AdvertiseMessage) && @ getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) && @ getMessage(id).getPerson1() != getMessage(id).getPerson2(); @ assignable messages; @ assignable getMessage(id).getPerson2().messages; @ 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 (\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; @ public exceptional_behavior @ signals (MessageIdNotFoundException e) !containsMessage(id); @ signals (MessageIdNotFoundException e) containsMessage(id) && !(getMessage(id) instance of AdvertiseMessage); @ signals (RelationNotFoundException e) containsMessage(id) && (getMessage(id) instance of AdvertiseMessage) && !(getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2())); @*/ public void sendAdvertiseMessage(int id) throws MessageIdNotFoundException, RelationNotFoundException, PersonIdNotFoundException;
在这单元学习了 JML
语言,接触了契约式编程,按照JML规格写作业不用花费太多精力,只要满足规格代码正确性基本得到了考察,只要考虑性能问题,即如何优化。JML描述十分严谨,但因此出现的问题就是描述可能比较抽象而且会很长,在作业中几个稍复杂一点的方法JML规格写的令人震惊,第一眼就不想去阅读。但在三次作业的迭代中使得阅读JML规格的能力逐步提升,对部分的规格描述也有了一定印象。需要说明的是因为性能的限制,所以不能完全按照规格里的实现方法进行代码的书写,而是需要进行灵活的优化,也是对规格的理解和阅读要求的进一步提升。