标签：OO relationGroup 结点 连通 作业 BUAA 算法 JML 单元
目录一、需求分析
1、第一次作业
通过实现官方的Person、Network、Group接口来实现自己的Person、Network、Group类（根据官方源码中的JML规格），实现相关的异常类。主要是理解isCircle和queryBlockSum两个函数的JML规格的含义，转化为一种自然语言的理解，把person看成点，人与人之间的关系看成边，那么isCircle函数就是查验两个点之间是否连通。queryBlockSum函数是查询有几个连通图。
2、第二次作业
新增了Message接口，根据源码的JML规格实现自己的Message类。实现Person、Network、Group接口中新增的方法和新增的异常类。主要难点在于queryLeastConnection函数的最小生成树算法的实现和qgvs指令的复杂度优化。
3、第三次作业
新增了EmojiMessage、NoticeMessage、RedEnvelopeMessage，在原有的类中新增方法。主要难点在于sendIndirectMessage函数需要实现最短路径算法。
二、方案实现
1、第一次作业
通过HashMap来存储一个连通图中的Person，在addPerson时，新增加一个孤立点作为一个单独的连通图，在addRelation时，把两个分隔的连通图合并到一个HashMap里面，第一次作业功能比较简单，因此通过简单的记录连图中的点的信息即可。
合并连通图函数：
public void addToRelationGroup(Person p1, Person p2) {
int indexP1 = -1;
int indexP2 = -1;
int flag = 0;
for (int i = 0; i < relationGroup.size(); i++) {
if (relationGroup.get(i).containsKey(p1.getId())) {
indexP1 = i;
flag++;
}
if (relationGroup.get(i).containsKey(p2.getId())) {
indexP2 = i;
flag++;
}
if (flag == 2) {
break;
}
}
if (indexP1 == -1 && indexP2 == -1) {
HashMap<Integer, Person> group = new HashMap<>();
relationGroup.add(group);
group.put(p1.getId(), p1);
group.put(p2.getId(), p2);
} else if (indexP1 != -1 && indexP2 == -1) {
relationGroup.get(indexP1).put(p2.getId(), p2);
} else if (indexP1 == -1) {
relationGroup.get(indexP2).put(p1.getId(), p1);
} else {
if (indexP1 != indexP2) {
HashMap<Integer, Person> group1 = relationGroup.get(indexP1);
HashMap<Integer, Person> group2 = relationGroup.get(indexP2);
relationGroup.remove(group1);
relationGroup.remove(group2);
if (group1.size() <= group2.size()) {
group2.putAll(group1);
relationGroup.add(group2);
} else {
group1.putAll(group2);
relationGroup.add(group1);
}
}
}
}
2、第二次作业
由于需要求最小生成树，我们需要维护图的更多的信息，因此新建了Graph和Edge类来存储一个连通图的信息。
Edge类记录两边结点Person以及边的权值，Graph类记录了一个连通图中的所有结点，并且采用kruskal算法来生成最小生成树，算法实现为把边按照权值大小排序，然后从最小的边开始选择，把两边结点加入到最小生成树的结点集合中，当加入的边其两边结点不都在最小生成树的结点集合中时，该边可加入到最小生成树，这样在构造过程中就保证了不会成环。即每次选择最小边，并且保证已经选择的边不会成环。为了减少算法的复杂度，在维护连通图中存储的边时，采取了这样的策略，经过一次最小生成树计算之后，边集中只保留最小生成树的边，合并两个图时，若两个图都是未更新的并且已经计算过最小生成树，那么合并这两个图只需要把两个图的边集合并再加上新增的边即可。
qgvs指令通过分析可得，如果按照JML的描述，无论采取ArrayList（O（mn^2））存储还是HashMap（计算hash值耗费时间）存储都有较高的复杂度。但如果我们遍历每个人的acquaintance集合，那么当每个人的acquaintance集合较小时，复杂度会下降很多，而测试点中，为稠密图的可能性并不大，并且必须当group中的人数小于acquaintance中的人数，这个策略才会耗时更多。
3、第三次作业
第三次作业相比第二次作业，在有关图的部分就多了个最短路径算法，新建了个Path类用来记录某结点到其他结点的路径长度。以便使用优先队列来存储结点路径。
采用堆优化的狄克斯特拉算法，利用Java自带的优先队列实现起来很方便。算法思路就是从起点出发，维护一个到其他结点的路径矩阵，每次选择能到达的最短的那条路径的结点作为新的搜索结点（之前没有搜索过）。
4、架构设计，图模型构建维护总结
本单元的架构基本上不需要自己设计，我们需要做的工作基本上是按照官方源码中的JML规格实现相关函数接口即可。总的来说，我认为本单元作业的架构可以分为三个部分，异常部分、图模型部分、社交网络模拟部分。
异常部分：
社交网络模拟：
需要我们自己设计的是图模型的构建与维护，我新建了Graph类，进行ap就是新建一个连通图（此时连通图中只有一个孤立结点），进行ar就是向图中加边或者合并两个原本相互不连通的连通图。把最小生成树和最短路径的算法封装到Graph类中，能够体现良好的封装性，把图的功能和社交网络部分内容独立开来。
三、测试数据准备
主要是针对每条指令随机生成数据进行覆盖性测试，不过我测试的量不够导致覆盖性并不是很好（另一方面随机性过高，错误更多的出现在多个指令组合时而出错，但我只是随机生成单个的指令，很多时候只测试了一个正确的分支），在第二次作业和第三次作业中强测雪崩。除了随机生成每条指令构造测试数据之外，针对性能上可能会出现问题的地方，构造一些容易超时的数据，如针对qgvs、qlc、sim指令来专门构造一些稠密图，稀疏图来测试下性能。
四、bug分析
第一次作业指令比较简单，没有被发现bug。第二次作业，sendMessage函数在message的type为1时，对群组里的person进行addSocialValue操作时，传参写错了，写成了p.addSocialValue(p.getSocialValue() + message.getSocialValue())，是一个十分粗心的错误，而在测试时刚好又没测到这个情况。第三次作业错的更离谱了，狄克斯特拉算法实现错了，在确定新的搜索结点的时候，我直接把当前搜索的结点能够到达的最短的那条边的另一端结点作为新的搜索结点，算法要求是从当前已经搜索过的结点能够到达的所有结点中，选择最短的那条边的另一端的结点。然而，自测时测试的刚好都是可以一直沿着一条路径走下去确定最短路径的情况，导致测试了50组数据并没有出现问题，强测直接出现空指针崩掉。
本单元作业中，针对性能优化的情况比较重视，出现的bug都不是性能上的问题。第三次作业由于错的比较严重，直接重写了狄克斯特拉算法，并且利用Java的优先队列对狄克斯特拉算法进行了优化。
五、Network扩展
/*@ public normal_behavior
@ requires containsMessage(id)
@ assignable messages;
@ assignable people[*].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 < people.length && this.isLinked(people[i]);
@ (\forall int j;0 <= j && j < \old(people[i].getMessages().size());
@ people[i].getMessages().get(j + 1) == \old(people[i].getMessages().get(j))) &&
@ people[i].getMessages().get(0).equals(\old(getMessage(id))) &&
@ people[i].getMessages().size() == \old(people[i].getMessages().size()) + 1);
@ ensures (\forall int i;0 <= i && i < people.length && !this.isLinked(people[i]);
@ people[i].getMessages() == \old(people[i].getMessages()));
@ also
@ public exceptional_behavior
@ signals (MessageIdNotFoundException e) !containsMessage(id);
*/
void sendAdvertisementMessage(int id) throws MessageIdNotFoundException;
/*@ public normal_behavior
@ requires !containsProduct(id)
@ assignable products;
@ ensures (\forall int i;0 <= i && i <= \old(products.length);
@ (\exists int j;0 <= j && j <= products.length;products[j].equals(\old(products[i]))));
@ ensures (\exists int i;0 <= i && i < products.length;products[i].equals(getProduct(id)));
@ ensures products.length == \old(products.length) + 1;
@ also
@ public exceptional_behavior
@ signals (EqualProductIdException e) containsProduct(id);
*/
void publishProduct(int id);
/*@ public normal_behavior
@ requires containsMessage(id) && this.isLinked(getPerson(advertiserId));
@ assignable messages;
@ assignable getPerson(advertiserId).messages;
@ ensures (\forall int i;0 <= i && i <= \old(messages.size()) && message[i].getId != id;
@ (\exists int j;0 <= j && j <= messages.size();messages[j] == \old(messages[i])));
@ ensures (\forall int i;0 <= i && i <= messages.size();message[i].getId != id);
@ ensures messages.size() = \old(message.size()) - 1;
@ ensures (\forall int i;0 <= i && i <= \old(getPerson(advertiserId).getMessages().size());
@ getPerson(advertiserId).getMessages().get(i + 1) == \old(getPerson(advertiserId).getMessages().get(i)) &&
@ getPerson(advertiserId).getMessages().get(0).equals(getMessage(id)));
@ ensures getPerson(advertiserId).getMessages().size() == \old(getPerson(advertiser).getMessages().size()) + 1;
@ also
@ public exceptional_behavior
@ signals (MessageIdNotFoundException) !containsMessage(id);
@ signals (NotLinkedAdvertiserException) !this.isLinked(getPerson(advertiserId));
*/
void sendPurchaseMessage(int advertiserId,int id) throws MessageIdNotFoundException;
六、心得体会
这一单元学习了JML形式化表述语言，体会了契约式编程思想。感受最深的一点是JML规格只是相当于互相的一个约定，代码的实现其实是很自由的，需要个人先读懂规格、理解需求，然后再去设计的，完完全全按照规格来写的代码肯定是很“臭”的。规格的作用在于准确传达需求，然而，读懂JML规格其实并不是很轻松，需要我们从逻辑严谨但又比较抽象的描述中提炼出具体需求。另一方面，感受深刻的是这单元需要我们做好自测，不仅是针对特定指令的性能考虑，还需要做好覆盖性测试，利用JML规格构造出能够尽量进入到每一个程序分支的测试数据。
标签：OO,relationGroup,结点,连通,作业,BUAA,算法,JML,单元 来源： https://www.cnblogs.com/lxyskyler/p/16342546.html
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。