本单元根据给出的JML规格实现一个社交网络模型，同时为了让我们阅读理解一些复杂的JML规格，涉及了图论的一些算法。这部分的JML还是较难以理解的，并且一些指令的实现也不能完全按照JML所给出的方法去实现不然容易超时，在满足JML规格的要求下还需要进行很多的优化。

从JML的角度构造测试数据

在测试方面，首先可以再阅读一边JML规格，找到一些写代码时没有注意到的细节，比如群组的容纳上限是1111人。同时根据功能对每个指令进行测试，简单地测试功能是否正常以及异常的抛出是否正常。
然后采取随机生成数据的方式，根据JML规格进行一些调整和限制，尽可能覆盖更多的情况，首先对每个指令进行全覆盖的测试，比如不满足前置条件，数据不合法，在有多个异常的方法中，构造满足不同异常的数据等，在限定范围内大量构造数据。
对于一些复杂度较高的方法，比如图论相关的算法以及Group的getValueSum方法，在互测中，同学们大多都从这方面入手hack，所以在满足JML规格的情况下，对复杂度较高的方法要进行一定的优化，在测试时对这些方法也要构造针对性的大量的数据看是否会超时。

架构设计与模型构建和维护策略

除了实现接口所规定的类以外，增加了Counter类用于在异常类中保存触发的异常次数，增加了Edge类用于实现某些图论算法，增加了Tool类用于封装某些算法，避免MyNetwork类中行数过多。
在此社交网络中，每个person为该网络的一个节点，每个person的acquaintance则是与其相连的点，对于的socialValue则是边权，以此构建了一个无向图，除了实现添加，查询节点，边之类的指令外，还需要实现求连通分量的个数，求最小生成树，计算最短路径的问题。

hw9：查询连通分类的个数

刚开始采用JML描述的查询方式，对每个Person的acquaintance查询直至全部查询完进行计数，没有进行优化，很容易TLE。在学习了并查集算法后，更改了实现方式。并查集的本质是维护一个森林，开始时每一个节点都是孤立的，各自形成一个树，之后进行若干次的合并操作，每次合并将两个数合并成为一个更大的树。因为并查集的find操作的时间复杂度和树的高度成正相关，在合并时还可以采取按秩合并和路径压缩的优化方法，尽可能地降低树地高度，减少树的层数在具体实现是采用HashMap，初始时所有人指向自己，添加关系后，确定一个根节点，处于同一个连通图的合并根节点。最后在查询连通分量个数时，只要查询HashMap中有多少个不同的Value值。

hw10：求最小生成树

最小生成树有Prim算法和Kruskal算法，我才用了Kruskal算法，在Krusal算法中判断是否生成回路，也采用并查集的方法，在hw9的基础上较容易实现。在具体实现时，先在hw9所实现的并查集中，找到该连通分量的所有边并进行排序，不断选取最小且不构成回路的边，直至包含了n-1条边为止，便是最小生成树，在并查集的合并查找等操作就可以直接使用hw9中所写的函数来实现。

hw11：计算最短路径

采用Dijkstra算法找到最短路径发送消息，在基本的Dijkstra算法上采用了堆优化，加入一个优先队列，加快了寻找最小值这一步。在JAVA中便有优先队列可以很轻松的实现这一步。

性能问题和优化情况

除了在上述提到的三个图论算法会出现性能问题外，在hw10的互测中，qgvs这一指令同样会造成性能问题，这一指令查询群组的边权和。最开始我按照JML所给出的规格来实现造成了超时，经过优化后，在Group中新增这一属性，每更新点或边时便维护这一属性的值，解决了这一指令在数据较大时的超时问题

Network拓展

新增的三种不同的Person可以视为Person的子类，在继承Person接口的基础上再实现新的方法。同时，广告可以也可以视为一种新的Message，继承Message接口并拓展自己的方法，消费者购买需要发送信息，同样视为一种新的Message。
Advertise：在继承Person接口的基础上，新增属性存储广告对应的产品id，新增属性存储所发送广告产品对应的生产商，新增方法发送AdvertiseMessage和PurchaseMessage
Producer：在继承Person接口的基础上，新增属性存储生产的产品id，新增属性存储生产产品数量，以及相应产品的信息如价格等，新增方法接收PurchaseMessage并生产和发送产品
Customer：在继承Person接口的基础上，新增方法发送PurchaseMessage给相应的Advertise
AdvertiseMessage：在继承Message接口的基础上，新增属性存储对应产品id
PurchaseMessage：在继承Message接口的基础上，新增属性存储对应产品的id
NetWork：需要新增方法：添加Advertise，Producer，Customer的方法，新增AdvertiseMessage和PurchaseMessage的方法，让Advertise发送两种信息的方法，让Producer生产产品的方法，让Customer购买产品的方法。在这些方法实现中存储销售相关信息，再新增方法查询产品销售额和产品销售路径。
新增异常类如ProduceIdNotFoundException，当没有相应的产品id时抛出;AdvertiserIdnotFoundException,当对应产品没有Advertiser时抛出;AdvertiseMessageIdNotFoundException,当没有相应产品id的广告时抛出。

相应JML规格书写

发送广告

/*@ public normal_behavior
      @ requires containAdvertiseMessage(id1)&&containAdvertise(id2)&&containProducer(id3);
      @ assignable messages,customer[*].message;
      @ ensures customer.length == \old(cusromer.length);
      @ 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 < custom.length&&(\forall int j;0<=j&&j<custom[i].getMessage.size()&&
      @         \old(custom[i].getMessage).get(i+1)==custom[i].getMessage.get(i)&&custom[i].getMessage.get(0)==
      @         \old(getAdvertiseMessage(id)&&custom[i].getMessage.size=\old(custom[i].getMessage).size+1));
      @ also
      @ public exceptional_behavior
      @ assignable \nothing;
      @ requires !containAdvertiseMessage(id1) || !containAdvertise(id2) || !containProducer(id3);
      @ signals (AdvertiseMessageIdNotFoundException e) !containAdvertiseMessage(id1);
      @ signals (AdvertiserIdnotFoundException e) containAdvertiseMessage(id1) && !containAdvertise(id2)
      @ signals (ProduceIdNotFoundException e) containAdvertiseMessage(id1) && containAdvertise(id2) &&
      @         !containProducer(id3);
      @*/

生产商接收购买信息

/*@ public normal_behavior
      @ requires containPurchaseMessage(id)&&cotainProducer(producerId);
      @ assignable messages,pruducer[*].productCount;
      @ ensures pruducer.length == \old(pruducer.length);
      @ 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 (getProducerId(producerId).getProductCount=\old(getProducerId(producerId).getProductCount)+1);
      @ also
      @ public exceptional_behavior
      @ assignable \nothing;
      @ requires !containPurchaseMessage(id) || !cotainProducer(producerId) ;
      @ signals (PurchaseMessageIdNotFoundException e) !containPurchaseMessage(id);
      @ signals (ProducerIdnotFoundException e) containPurchaseMessage(id) &&  !cotainProducer(producerId);
      @*/

查询某种商品的销售额

/*@ public normal_behavior
      @ requirescotainProducer(producerId);
      @ assignable \nothing;
      @ ensures (\result=getProducerId(producerId).getProductCount);
      @ also
      @ public exceptional_behavior
      @ assignable \nothing;
      @ requires !containPurchaseMessage(id);
      @ signals (PurchaseMessageIdNotFoundException e) !containPurchaseMessage(id);
      @*/

学习体会

本单元的难度较低，作业花费的时间较之前两个单元也少了很多。通过本单元的学习认识到了什么是JML，如何通过JML完成相应的代码实现，实现并不难而写JML规格却是一件十分困难和痛苦的事情，全面地严谨地用形式化语言描述功能导致写JML困难，也正是因为如此才能做到设计者和实现者之间地契约与规范。在完成所规定地功能时也要尝试在不影响结果地情况下尽可能去优化方法，在此后地学习中也要学习规格化设计地思想，提高严谨性。

标签：OO,实现,length,博客,算法,JML,方法,id,单元
来源： https://www.cnblogs.com/YanG2k17/p/16333636.html