标签：OO HashMap int BUAA 规格 JML new id 单元
BUAA OO 第三单元总结
一、题目简介
第三单元整体目标为实现简单社交关系的模拟和查询，让我们了解了基本的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指令，就是因为没有对其进行较强的测试导致的。
五、拓展JML
新增接口与方法
Advertiser，Producer，Customer实现Person子接口Product- 为新开设的类，代表产品
- AdvertisementMessage：继承Message，有advertiserId、producerId、productId的属性。
- PurchaseMessage：继承Message，有advertiserId、producerId、productId的属性。
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规格的能力逐步提升，对部分的规格描述也有了一定印象。需要说明的是因为性能的限制，所以不能完全按照规格里的实现方法进行代码的书写，而是需要进行灵活的优化，也是对规格的理解和阅读要求的进一步提升。
标签：OO,HashMap,int,BUAA,规格,JML,new,id,单元 来源： https://www.cnblogs.com/xzynb/p/16338982.html
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。