首页 > 其他分享> > 第三单元实验总结 | TrickEye

第三单元实验总结 | TrickEye

2022-06-06 16:00:48 作者：互联网

第三单元实验总结 | TrickEye

基本情况部分

这篇帖子为什么会在这？
- 这是北航计算机学院面向对象构造与设计2022春季课程第三单元的总结博客
本次作业的要求是什么？
- 根据课程组提供的JML形式语言，实现一个简单的社交网络建模程序，按要求完成对该社交网络的信息查询功能。

自测篇：如何构造测试数据？

对于JML而言，受其规定的一个方法在各种情况下的行为都受到了JML精确严格的约束，因此如果一个数据能够覆盖JML指出的所有情况，那么这个数据就是合理的。对于我们的程序而言，一个合理的数据应当能够对应代码的每一行。

注意到Idea提供了代码覆盖率检查的工具，它可以根据java程序的一次执行，检测哪些代码被执行了，那些代码没有执行。通过在自动构造数据的基础上手动添加一些数据，能够达到比较高的覆盖率，在此情况下，与其他同学的代码对拍，可以快速检查自己有没有问题。

上面讲到的这种测试方式对于行为复杂，涉及多个异常抛出的方法比较合适。而有些方法，行为种类不多，（只有一个normal_behavior），但是要求繁琐，例如要求连通块数、最小生成树、单源最短路等等。对于这种函数的测试，要求我们构造各种类型的图，避免算法在某些情况下性能退化或者过低不能满足要求的情况。

例如，并查集求最小连通块问题，如果不在合并时维护连通块数量，而是每次询问时用一个O(n)的算法来计算，那就会超时。

再例如，求所有边权值和（QueryGroupValueSum）也不能在询问时查询，而应当在产生关系时维护。

模型构建和维护策略

本次作业的模型可以被抽象成一个无向图。在增删改查这四大操作中，我们只需要支持增和查。增的基本操作包括增加节点，增加关系，增加群组，群组增加成员等；查的操作就有不少。

为了解决比较复杂的查询操作问题，我们采用多种数据结构和算法，例如，维护并查集来解决qbs问题，使用kruskal算法来求最小生成树，使用dijkstra算法求单源最短路。

性能问题

通过使用以上的模型，可以得到正确答案，但是性能不一定强。在一些操作容易出现超时的问题。这是因为虽然JML提供了方法行为的约束，但是不约束，不指定方法的实现方式，如果只是简单的翻译JML的描述，那么的得到的方法性能不会太好。

我遇到的几次这样的性能问题，几乎都是因为询问时查询导致的。例如，qbs的HashSet实现跑了一遍O(n)，ArrayList实现跑了一个O(n^2)，qgvs跑了一个BFS等等，而优化的思路就是在添加关系的时候适当维护一些量，使得在询问的时候可以直接O(1)查询。

Network 拓展

首先，Advertiser，Producer，Customer均继承自Person类

Advertisement继承自message类

Advertiser向某个Customer发送广告：（这里我们假设是通过message来打广告）

 /*@ public normal_behavior
   @ requires containsMessage(id) && getMessage(id).getType() == 0 && 
   @         getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) && 
   @         (getMessage(id).getPerson1() instanceof Advertiser) && 
   @         (getMessage(id).getPerson2() instanceof Customer)
   @ assignable messages;
   @ assignable getMessage(id).getPerson1().socialValue;
   @ assignable getMessage(id).getPerson2().messages, getMessage(id).getPerson2().socialValue;
   @ 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 !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) == \old(getMessage(id));
   @ ensures \old(getMessage(id)).getPerson2().getMessages().size() == 
   @         \old(getMessage(id).getPerson2().getMessages().size()) + 1;
   @ 其他涉及advertise的量的改变，例如
   @ ensures \old(getMessage(id)).getPerson2.getPurchaseWill() == \old(getMessage(id).getPerson2.getPurchaseWill()) + 
   @         ((Advertisement) \old(getMessage(id))).getPurchaseWillIncrease;
   @ also
   @ public exceptional_behavior
   @ signals (MessageIdNotFoundException e) !containsMessage(id) || getMessage(id).getType() == 1;
   @ signals (RelationNotFoundException e) containsMessage(id) && getMessage(id).getType() == 0 &&
   @          !(getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2())); 
   @ signals (PersonIdNotFoundException e) containsMessage(id) && getMessage(id).getType() == 0 && 
   @         getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) && 
   @         !(getMessage(id).getPerson1() instanceof Advertiser)
   @ signals (PersonIdNotFoundException e) containsMessage(id) && getMessage(id).getType() == 0 && 
   @         getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) && 
   @         (getMessage(id).getPerson1() instanceof Advertiser) && 
   @         !(getMessage(id).getPerson2() instanceof Customer)
   @ */
 public void advertiseToCustomer(int id) throws RelationNotFoundException, MessageIdNotFoundException, PersonIdNotFoundException;

 /*@ public normal_behavior
   @ requires containsMessage(id) && getMessage(id).getType() == 0 && 
   @         getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) && 
   @         (getMessage(id).getPerson1() instanceof Advertiser) && 
   @         (getMessage(id).getPerson2() instanceof Producer)
   @ assignable messages;
   @ assignable getMessage(id).getPerson1().socialValue;
   @ assignable getMessage(id).getPerson2().messages, getMessage(id).getPerson2().socialValue;
   @ 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 !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) == \old(getMessage(id));
   @ ensures \old(getMessage(id)).getPerson2().getMessages().size() == 
   @         \old(getMessage(id).getPerson2().getMessages().size()) + 1;
   @ 其他涉及advertise的量的改变，例如
   @ ensures \old(getMessage(id)).getPerson2.getProduceWill() == \old(getMessage(id).getPerson2.getProduceWill()) + 
   @         ((Advertisement) \old(getMessage(id))).getProduceWillIncrease;
   @ also
   @ public exceptional_behavior
   @ signals (MessageIdNotFoundException e) !containsMessage(id) || getMessage(id).getType() == 1;
   @ signals (RelationNotFoundException e) containsMessage(id) && getMessage(id).getType() == 0 &&
   @          !(getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2())); 
   @ signals (PersonIdNotFoundException e) containsMessage(id) && getMessage(id).getType() == 0 && 
   @         getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) && 
   @         !(getMessage(id).getPerson1() instanceof Advertiser)
   @ signals (PersonIdNotFoundException e) containsMessage(id) && getMessage(id).getType() == 0 && 
   @         getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) && 
   @         (getMessage(id).getPerson1() instanceof Advertiser) && 
   @         !(getMessage(id).getPerson2() instanceof Producer)
   @ */
 public void advertiseToProducer(int id) throws RelationNotFoundException, MessageIdNotFoundException, PersonIdNotFoundException;

     /*@ public normal_behavior
       @ requires containsMessage(id) && getMessage(id).getType() == 0 &&
       @         getMessage(id) instanceof RedEnvelopMessage &&
       @         (getMessage(id).getPerson1() instanceof Advertiser) && 
       @         (getMessage(id).getPerson2() instanceof Producer) &&
       @         !isCircle(getMessage(id).getPerson1().getId(), getMessage(id).getPerson2().getId());
       @ ensures \result == -1;
       @ also
       @ public normal_behavior
       @ requires containsMessage(id) && getMessage(id).getType() == 0 &&
       @          isCircle(getMessage(id).getPerson1().getId(), getMessage(id).getPerson2().getId());
       @ 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;
       @ 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 (\exists Person[] pathM;
       @         pathM.length >= 2 &&
       @         pathM[0].equals(\old(getMessage(id)).getPerson1()) &&
       @         pathM[pathM.length - 1].equals(\old(getMessage(id)).getPerson2()) &&
       @         (\forall int i; 1 <= i && i < pathM.length; pathM[i - 1].isLinked(pathM[i]));
       @         (\forall Person[] path;
       @         path.length >= 2 &&
       @         path[0].equals(\old(getMessage(id)).getPerson1()) &&
       @         path[path.length - 1].equals(\old(getMessage(id)).getPerson2()) &&
       @         (\forall int i; 1 <= i && i < path.length; path[i - 1].isLinked(path[i]));
       @         (\sum int i; 1 <= i && i < path.length; path[i - 1].queryValue(path[i])) >=
       @         (\sum int i; 1 <= i && i < pathM.length; pathM[i - 1].queryValue(pathM[i]))) &&
       @         \result==(\sum int i; 1 <= i && i < pathM.length; pathM[i - 1].queryValue(pathM[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 (\old(getMessage(id)) instanceof RedEnvelopeMessage) ==>
       @         (\old(getMessage(id)).getPerson1().getMoney() ==
       @         \old(getMessage(id).getPerson1().getMoney()) - ((RedEnvelopeMessage)\old(getMessage(id))).getMoney() &&
       @         \old(getMessage(id)).getPerson2().getMoney() ==
       @         \old(getMessage(id).getPerson2().getMoney()) + ((RedEnvelopeMessage)\old(getMessage(id))).getMoney());
       @ ensures (!(\old(getMessage(id)) instanceof RedEnvelopeMessage)) ==> (\not_assigned(people[*].money));
       @ 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;
       @ also
       @ public exceptional_behavior
       @ signals (MessageIdNotFoundException e) !containsMessage(id) ||
       @         getMessage(id).getType() == 1 || 
       @         !(getMessage(id) instanceof RedEnvelopMessage);
       @ signals (RelationNotFoundException e) containsMessage(id) &&
       @         getMessage(id).getType() == 0 &&
       @         (getMessage(id) instanceof RedEnvelopMessage) && 
       @         !(getMessage(id).getPerson1() instanceof Customer || getMessage(id).getPerson2() instanceof Producer)
       @*/
 public void buy(int id) throws PersonIdNotFoundException, MessageIdNotFoundException;

这里，buy就是一个sendIndirectMessage的翻版。

标签：总结,getPerson2,getPerson1,old,TrickEye,getMessage,&&,id,单元
来源： https://www.cnblogs.com/trickeye/p/16348501.html