一、单元内容

本单元内容为规格化设计，即通过参考已经完成的JML描述实现一个社交网络相关功能。

本单元整体来说难度不大，但是却是我最惨的一次作业，所以本博客可能会主要谈一谈测试中的一些策略吧。

二、自测策略

1、白盒测试

即从JML出发针对各种情况构造测试数据，可以选用课程组推荐的JUnit单元测试框架来对每个函数进行测试。我也借此机会学习了一下JUnit的用法。

在构造测试数据的时候，可以充分利用JML规格来构造一些针对性的数据，比如看哪个方法JML较为复杂，可以针对这样的方法构造一些边界情况的数据，比如作业中的queryBlockSum，getValueSum，queryLeastConnection，sendIndirectMessage等操作，尤其是对于那些不能直接照着JML写，而是需要自己进行优化的方法进行着重测试，构造极端数据。

2、黑盒测试

也就是随机对拍，我个人还是觉得在本课程中随机对拍仍然是最好的调试方式，尤其是在本单元中。本人在本单元第三次作业的时候因为一些其他事情占用了一些时间，而且第二次作业未编写对拍，第三次作业编写对拍相对来说难度不低，因此未进行随机测试，只是进行了一些功能测试和单元测试，各项功能都正常，最后因为在编写异常时直接复制相同类型的类，结果忘了改前面的字符串，然后测试的时候没考虑到这部分，强测喜提30分。

三、架构设计

本单元的目标是要实现一个社交网络，主要包括Network、Message、Group、Person等类，本单元大部分代码都可以直接按照JML的逻辑完成，因此这些代码不涉及架构方面的问题。

在这里主要是列举一些特殊函数，这些函数要么JML并没有给出具体的实现逻辑，要么按照JML的逻辑可能会导致超时（CTLE）的情况。

1、queryBlockSum

JML提供了一个 \(O(N^2)\) 的做法，但是这无法满足复杂度的要求，观察代码可以看出它计算了所有 \(1\sim i-1\) 中和 \(i\) 不相连的 \(i\) 的个数，本质上也就是连通块个数，因此可以使用并查集来维护。

处于优化代码结构的目的，我将并查集单独分为一类，在其中实现了add(x)、merge(x1,x2)、union(x1,x2)、getCountBlock等操作，降低了代码的耦合性。

2、queryLeastConnection

本函数的JML只描述了一个边的集合，即我们的答案具有什么样的特征，而对于如何求解则没有给出具体做法，观察这个边的集合会发现他是用最少的边权和把所有点连起来的方案，也就是最小生成树，考虑到复杂度的问题，我们可以使用堆优化的Prim算法来求解。

Prim我同样单独封装为一个类，实现了add(a,b,val)、query(st)操作，在外层只需要直接调用即可。

3、queryGroupValueSum

这个从JML出发可以直接得到做法，但是这样的做法却会超时，因此正确的做法是在addRelation、addPerson、delPerson时维护一个Group的答案，这样就将询问原本 \(O(N^2)\) 的复杂度转化为了修改时单次 \(O(N)\) 的复杂度。

4、sendIndirectMessage

与queryLeastConnection操作类似，它给出了一个点的集合，观察可以发现相邻两个点相连，也就是描述了路径的性质，而最终也就是求的最短路径，可以用堆优化Dijkstra解决。具体实现与Prim的实现类似。

四、性能问题与修复情况

性能问题上面已经描述了几个可能出现性能问题的操作最终是如何解决的。

本人自己的错误除了上述写错字符串错误外，在第二单元的Dijkstra实现也出现了错误，一是很简单的Dijkstra写错，二是没有考虑到一个连通块中只有一个点的情况。

这些错误归根到底还是没有进行充分的测试，本次出现的错误都很明显，基本都是由于粗心导致写错，也很容易改正，以后还是应该编写足够的随机测试，只能说吃一堑长一智了。

本人在房内hack出qgvs超时等情况，前面已经提过，再次不再赘述。

五、功能扩展

功能要求

假设出现了几种不同的Person

• Advertiser：持续向外发送产品广告
• Producer：产品生产商，通过Advertiser来销售产品
• Customer：消费者，会关注广告并选择和自己偏好匹配的产品来购买 -- 所谓购买，就是直接通过Advertiser给相应Producer发一个购买消息
• Person：吃瓜群众，不发广告，不买东西，不卖东西

如此Network可以支持市场营销，并能查询某种商品的销售额和销售路径等 请讨论如何对Network扩展，给出相关接口方法，并选择3个核心业务功能的接口方法撰写JML规格（借鉴所总结的JML规格模式）

扩展实现

Advertiser、Producer、Customer 实现 Person 接口，新增 AdvertisementMessage 类、BuyMessage 类，他们实现 Message 接口。AdvertisementMessage 类应保存 Producer、Product、Price 等信息。BuyMessage类应保存 Product 等信息。

求产品销售量

/*@ public instance model non_null Product[] products;
  @ public instance model non_null Product[] productSales;
  @*/

/*@ public normal_behavior
  @ requires containsProduct(product);
  @ ensures (\exists int i; 0 <= i && i < products.length;
  @         products[i].getId() == product.getId() && \result == productSales[i]);
  @ also
  @ public exceptional_behavior
  @ signals (ProductNotFoundException e) !containsProduct(product);
  @*/
public int queryProductSales(Product product) throws ProductNotFoundException;

发布广告

/*@ public instance model non_null AdvertisementMessage[] advertisementMessages;
  @*/

/*@ public normal_behavior
  @ requires !(\exists int i; 0 <= i && i < advertisementMessages.length; advertisementMessages[i].equals(advertisement)) &&
  @          containsProductId(advertisement.getProductId()) &&
  @          (advertisement.getType() == 0) ==> (advertisement.getPerson1() != advertisement.getPerson2());
  @ assignable advertisementMessages;
  @ ensures advertisementMessages.length == \old(advertisementMessages.length) + 1;
  @ ensures (\forall int i; 0 <= i && i < \old(advertisementMessages.length);
  @          (\exists int j; 0 <= j && j < advertisementMessages.length; advertisementMessages[j].equals(\old(advertisementMessages[i]))));
  @ ensures (\exists int i; 0 <= i && i < advertisementMessages.length; advertisementMessages[i].equals(advertisement));
  @ also
  @ exceptional_behavior
  @ signals (EqualAdvertisementIdException e) (\exists int i; 0 <= i && i < advertisementMessages.length; advertisementMessages[i].equals(advertisement));
  @ signals (ProductIdNotFoundException e) !(\exists int i; 0 <= i && i < advertisementMessages.length; advertisementMessages[i].equals(advertisement)) &&
  @                                        !containsProductId(advertisement.getProductId());
  @ signals (EqualPersonIdException e) !(\exists int i; 0 <= i && i < advertisementMessages.length; advertisementMessages[i].equals(advertisement)) &&
  @                                    containsProductId(advertisement.getProductId()) &&
  @                                    advertisement.getType() == 0 && advertisement.getPerson1() == advertisement.getPerson2();
  @*/
public void advertise(AdvertisementMessage advertisement)
        throws EqualAdvertisementIdException, ProductIdNotFoundException, EqualPersonIdException;

这里只是生成发布广告的Message，之后需要进一步sendIndirectMessage。

生产产品、购买产品的操作与此类似

添加偏好

/*@ public normal_behavior
  @ requires !(\exists int i; 0 <= i && i < referenceProductId.length; referenceProductId[i].equals(product.getId()));
  @ assignable referenceProductId;
  @ ensures referenceProductId.length == \old(referenceProductId.length) + 1;
  @ ensures (\forall int i; 0 <= i && i < \old(referenceProductId.length);
  @          (\exists int j; 0 <= j && j < referenceProductId.referenceProductId; people[j] == (\old(referenceProductId[i]))));
  @ ensures (\exists int i; 0 <= i && i < referenceProductId.length; referenceProductId[i] == product.getId());
  @ also
  @ public exceptional_behavior
  @ signals (EqualProductIdException e) (\exists int i; 0 <= i && i < referenceProductId.length; referenceProductId[i].equals(product.getId()));
  @*/
public void AddReference(Product product) throws EqualProductIdException;

六、总结反思

首先是编程思想方面，本单元通过学习JML相关知识以及课外的了解和分享，我了解了契约式编程等相关思想，对于其可靠、易于测试的优势有了一定理解，鉴于目前写的代码都比较短，了解这些思想对于之后编写大规模的项目肯定还是很有用处的。

然后是测试方面，我学会了如何用JUnit进行单元测试。本单元相对前两个单元难度不高，但是却出了很大的错误，之后还是应该更加注重数据的测试，尽可能自己设计覆盖率高的强测。