标签：OO old int mid Summary getMessage && Unit3 message

OO Unit3 Summary

目录

• 一、测试方法

• 二、架构设计及图模型

• 三、性能问题及修复

• 四、扩展作业

• 五、学习体会

一、测试方法

本单元我采用的测试方法分为两种：一是针对某些复杂指令，基于其JML规格的测试，保证单个方法运行的正确性；二是随机数据生成测试，从全局保证程序正确性。

1. 基于JML规格的测试

对于某个特定的方法基于JML规格进行针对性测试，要点在于覆盖方法的所有前置条件，从而对所有相应后置条件情况进行正确性判断。要想覆盖所有前置条件，不仅要根据JML规格进行分类考虑，还要求对该类的状态变化具有全面的把握。对于后置条件的正确性判断，异常行为较容易进行判定，只需要观察相应异常即可。对于常规行为，需要基于数据计算正确结果进行比对(准备难度大但准确率能充分保证)，或者采用对拍的方式(准备难度低但准确率只能相对保证)。下面进行举例说明：

/*@ public normal_behavior
  @ requires !(\exists int i; 0 <= i && i < messages.length; messages[i].equals(message)) &&
  @           (message instanceof EmojiMessage) ==> containsEmojiId(((EmojiMessage) message).getEmojiId()) &&
  @            (message.getType() == 0) ==> (message.getPerson1() != message.getPerson2());
  @ assignable messages;
  @ ensures messages.length == \old(messages.length) + 1;
  @ ensures (\forall int i; 0 <= i && i < \old(messages.length);
  @          (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
  @ ensures (\exists int i; 0 <= i && i < messages.length; messages[i].equals(message));
  @ also
  @ public exceptional_behavior
  @ signals (EqualMessageIdException e) (\exists int i; 0 <= i && i < messages.length;
  @                                     messages[i].equals(message));
  @ signals (EmojiIdNotFoundException e) !(\exists int i; 0 <= i && i < messages.length;
  @                                       messages[i].equals(message)) &&
  @                                       (message instanceof EmojiMessage) &&
  @                                       !containsEmojiId(((EmojiMessage) message).getEmojiId());
  @ signals (EqualPersonIdException e) !(\exists int i; 0 <= i && i < messages.length;
  @                                     messages[i].equals(message)) &&
  @                                     ((message instanceof EmojiMessage) ==>
  @                                     containsEmojiId(((EmojiMessage) message).getEmojiId())) &&
  @                                     message.getType() == 0 && message.getPerson1() == message.getPerson2();
  @*/
public void addMessage(Message message) throws
        EqualMessageIdException, EmojiIdNotFoundException, EqualPersonIdException;

addMessage指令有四类可能的前置条件，分别是：

1. 网络中已存在相同messageId的情况

2. message是EmojiMessage但网络中不包含该Emoji

3. message是单发消息但发送者和接收者相同的情况

4. 上述三种情况均非的正常情况。

所以在覆盖这四种情况的时候，首先要构造出相应状态的网络类。

• 对于情况1，可以先在网络中添加一个Id的message，然后再添加重复Id进行测试。如：

  am 1 100 0 1 2
  am 1 200 1 3 4

• 对于情况2，可以直接添加一个EmojiMessage(因为初始状态网络中不包含Emoji)

  aem 1 1 0 1 2

• 对于情况3，可以直接添加一个type为0且两personId相同的message。

  am 1 100 0 1 1

• 对于情况4，可以先添加一个Emoji，再添加一个type为0且收发人不同的EmojiMessage。

  sei 1
  aem 1 1 0 1 2

观察后置条件时，对于前三种情况，观察对应异常输出即可。对于最后一种情况，可以在输入构造指令前后对message容器遍历输出，观察是否满足条件。

2. 随机数据测试

随机数据生成中，首先在开头生成若干ap、ag、ar、atg、sei、am等指令，为后续指令测试准备的同时测试这些指令的异常情况。之后，再以均等概率生成各类指令进行测试。

def datagenerator(self):
    data = ''
    self.names = copy.deepcopy(names)
    for j in range(self.pre_person):
        pid = self.generatorPerson()
        name = self.rdname()
        age = self.rdage()
        data += ("ap " + str(pid) + " " + name + " " + str(age) + "\n")
    # 生成 ap
    
    for i in range(num):
        instr = self.rdInstr()
        # 随机确定一个instr
        
        if (instr == 'qgps'):
            gid = self.getGroup()
            data += ("qgps " + str(gid) + " " + "\n")
        # 生成一个指令
        
    return data

数据生成以后，再利用数据进行对拍。实现自动化测评。

3. 测试总结

基于JML规格测试从理论上来说，只要保证了前置条件全覆盖，相应后置条件输出全部正确，就能保证单个方法的正确性。但是程序运行不仅是单个方法的问题。方法运行改变类的状态，不同类交互构成了程序。因此我们还需要测试类的状态改变以及不同类之间的交互，此时测试的构建难度加大了很多，由于完成作业时间有限，因此又采取了随机数据生成+对拍的方式进行自动测试。二者互补，相得益彰。

二、架构设计及图模型

1. 架构分析

由于是根据接口实现的各个类，关键方法已经注明且各个类之间的关系较为清晰，此处不再画UML图进行展示分析，只简略介绍各类的设置。

1. 第九次作业

• MyPerson类：

  • 使用HashMap容器存储acquaintance和value键值对，原因是JML规格中这对数据绑定。

  • 使用HashSet容器存储所处的group。

• MyGroup类：

  • 使用HashMap容器存储people，原因是方便检索。

  • 设置valueSum维护组value值。

• MyNetwork类：

  • 使用HashMap容器管理people和groups

  • 包含DisjointSet类方便图管理。

• DisjointSet类：

  • 方便图管理的类，包含实现并查集的属性和方法。

2. 第十次作业

• MyPerson类：

  • 使用LinkedList容器管理messages，原因是要求messages有序且sendMessage方法为头插操作。

• MyGroup类：

  • 设置ageSum维护组age值

• MyNetwork类：

  • 使用HashMap管理messages

  • 新增Graph类方便图管理。

• Graph类：

  • 方便图管理的类，维护的是person-relation的网络，包含prim方法。

• Edge类：

  • 实现Graph类所用

• MyMessage类：

  • 按规格实现。

3. 第十一次作业

• MyNetwork类：

  • 使用HashMap管理emojiId和heat键值对

• Graph类：

  • 新增dijkstra方法。

• 各类Message类：

  • 按规格实现。

2. 图构建和维护策略

社交网络以Network类为整个网络，Group类为簇，Person类为结点，relation为边。对该社交网络定义了一系列方法，可以采用修改网络时维护图的属性的方式，降低查询方法的复杂度。这是图构建维护的整体思路。下面以各查询方法为出发点进行分析：

• isCircle / qureyBlockSum：用并查集简化操作。具体来说，在addPerson时给并查集增加节点，在addRelation时合并并查集。isCircle时只需要调用并查集判断连通性操作，qureyBlockSum只需要查询并查集有几组。

• getValueSum / getAgeMean / getAgeVar ：给每个组维护一个valueSum和一个ageSum，在给组内增加删减person或在给组内的人增加删减relation时要对这两个变量维护。在查询时只需要以O(1)或O(n)的复杂度执行。

• sendIndirectMessage / queryLeastConnection : 用Graph类简化操作。具体来说，维护一个简单的person-relation图类，在addPerson时给Graph增加结点，在addRelation时给Graph增加边。在调用sendIndirectMessage 和 queryLeastConnection时，只需要调用Graph类的dijkstra方法和prim方法。注意在实现这两个方法时要使用堆优化保证性能。

三、性能问题及修复

社交网络中有两个性能提升点：

1. 管理的对象使用HashMap提高检索速度。

2. 各个图查询方法按照JML规格实现其时间复杂度将会非常高。具体处理方法参见 二、2. 图构建和维护策略。

由于在架构设计和图维护时考虑了方法性能问题，因此我没有出现性能问题。

四、扩展作业

假设出现了几种不同的Person

• Advertiser：持续向外发送产品广告

• Producer：产品生产商，通过Advertiser来销售产品

• Customer：消费者，会关注广告并选择和自己偏好匹配的产品来购买 --- 所谓购买，就是直接通过Advertiser给相应Producer发一个购买消息

• Person：吃瓜群众，不发广告，不买东西，不卖东西

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

• 新增类：

  • Advertiser、Producer、Customer 继承 Person

  • AdvertiseMessage、PurchaseMessage 继承 Message

    • AdvertiseMessage包含属性int productId, int producerId，person1 为 advertiser

    • PurchaseMessage包含属性int productId，person1 为 advertiser，person2 为 producer.

  • 新增异常类

• 类扩充：

  • Network 新增 int[] productIdList 属性和 int[] productSaleList 属性。

  • Customer新增属性int productId，对应偏好产品。

• 核心方法扩充：

  1. 发布广告 advertise：

     Advertiser将向所有关联的Customer发送信息。

     /*@ public normal_behavior
       @ requires containsMessage(id) && getMessage(id) instanceof AdvertiseMessage
       @ assignable messages;
       @ assignable getMessage(id).getPerson1().socialValue;
       @ 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 \old(getMessage(id)).getPerson1().getSocialValue() ==
       @         \old(getMessage(id).getPerson1().getSocialValue()) + \old(getMessage(id)).getSocialValue() &&
       @ ensures (\forall int i; 0 <= i && i < people.length; (\old(getMessage(id)).getPerson1().isLinked(people[i]) && people[i] instanceof Customer) ===> (\forall int j; 0 <= j && j < \old(people[i].getMessages().size());
       @          people[i].getMessages().get(j+1) == people[i].getMessages().get(j)));
       @ ensures (\forall int i; 0 <= i && i < people.length; (\old(getMessage(id)).getPerson1().isLinked(people[i]) && people[i] instanceof Customer) ===> (people[i].getMessages().get(0).equals(\old(getMessage(id)))));
       @ ensures (\forall int i; 0 <= i && i < people.length; (\old(getMessage(id)).getPerson1().isLinked(people[i]) && people[i] instanceof Customer) ===> (people[i].getMessages().size() == \old(people[i].getMessages().size()) + 1));
       @ also
       @ public exceptional_behavior
       @ signals (MessageIdNotFoundException e) !containsMessage(id);
       @ signals (NotAdvertiseMessageException e) containsMessage(id) && !(getMessage(id) instanceof AdvertiseMessage);
       @*/
     public void advertise(int id) throws MessageIdNotFoundException, NotAdvertiseMessageException;

  2. 购买产品 purchase

     customer根据已经收到的广告和偏好购买产品。具体行为是customer找到对应广告信息，然后advertiser向producer发送信息。其中getAdvertisement()方法是根据productId返回person.messages中首个关于该产品的广告信息，hasAdvertisement()则是根据productId判断是否有该产品的广告信息。

     /*@ public normal_behavior
       @ requires contains(pid) && getPerson(pid) instanceof Customer
       @ requires containsMessage(mid) && getMessage(mid) instanceof PurchaseMessage
       @ requires getPerson(pid).hasAdvertisement(getPerson(pid).productId) && getPerson(pid).getAdvertisement(getPerson(pid).productId).getPerson1().equals(getMessage(mid).getPerson1())
       @ assignable messages;
       @ assignable getMessage(mid).getPerson1().socialValue;
       @ assignable getMessage(mid).getPerson2().socialValue;
       @ assignable productSaleList;
       @ ensures !containsMessage(mid) && 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 \old(getMessage(mid)).getPerson1().getSocialValue() ==
       @         \old(getMessage(mid).getPerson1().getSocialValue()) + \old(getMessage(mid)).getSocialValue() &&
       @         \old(getMessage(mid)).getPerson2().getSocialValue() ==
       @         \old(getMessage(mid).getPerson2().getSocialValue()) + \old(getMessage(mid)).getSocialValue();
       @ ensures (\forall int i; 0 <= i && i < \old(getMessage(id).getPerson2().getMessages().size());
       @          \old(getMessage(mid)).getPerson2().getMessages().get(i+1) == \old(getMessage(mid).getPerson2().getMessages().get(i)));
       @ ensures \old(getMessage(mid)).getPerson2().getMessages().get(0).equals(\old(getMessage(mid)));
       @ ensures \old(getMessage(mid)).getPerson2().getMessages().size() == \old(getMessage(mid).getPerson2().getMessages().size()) + 1;
       @ ensures (\exist int i; 0 <= i && i < productIdList && productIdList[i] == getPerson(pid).productId; productSaleList[i] == \old(productSaleList[i]) + 1)
       
       @ also
       @ public exceptional_behavior
       @ signals (PersonIdNotFoundException e) !contains(pid);
       @ signals (NotCustomerException e) contains(pid) && !(getPerson(pid) instanceof Customer)
       @ signals (MessageIdNotFoundException e) !containsMessage(mid);
       @ signals (NotPurchaseMessageException e) containsMessage(mid) && !(getMessage(mid) instanceof PurchaseMessage);
       @ signals (NoAdvertisementException) !(getPerson(pid).hasAdvertisement(getPerson(pid).productId) && getPerson(pid).getAdvertisement(getPerson(pid).productId).getPerson1().equals(getMessage(mid).getPerson1()))
       @*/
     public void purchase(int pid, int mid) throws MessageIdNotFoundException, NotPurchaseMessageException, PersonIdNotFoundException, NotCustomerException, NoAdvertisementException;

  3. 查询商品销售额 searchProductSale
     具体行为是根据某productId查询其销售额。

     /*@ public normal_behavior
       @ requires containsProduct(id)
       @ ensures (\exists int i; 0 <= i && i < productIdList.length && productIdList[i] == id; \result == productSaleList[i]);
       @ also
       @ public exceptional_behavior
       @ signals (ProductIdNotFoundException e) !containsProduct(id);
       @*/
     public /*pure*/ int searchProductSale(int id) throws ProductIdNotFoundException;

五、学习体会

• 第三单元作业难度相对下降，因为不需要对类的交互过程进行复杂的构思设计，只需要在保证性能的前提下实现接口提供的方法即可。因此写作业的过程还是比较顺利的。

• 第三单元我投入了更多的精力在测试上，包括构造数据基于JML规格测试（可惜之处是课程组推荐的Junit只是浅尝辄止），以及三次作业开发迭代测评机。通过较为完备的测试，我对第三单元作业的正确性还是很有信心的。

• 第三单元最大的收获个人认为是理论课传授的知识，学习了JML规格，了解了契约式编程的思想。这将是日后学习、工作的重要基石之一。

标签：OO,old,int,mid,Summary,getMessage,&&,Unit3,message
来源： https://www.cnblogs.com/sleepEarlyGuy/p/16343838.html

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。