其他分享
首页 > 其他分享> > BUAA_OO_Unit3 总结

BUAA_OO_Unit3 总结

作者:互联网

BUAA_2022_Unit3总结

分析在本单元自测过程中如何利用JML规格来准备测试数据

根据是否触发异常来准备测试数据

JML规格一般包含normal情况的输入数据和会触发异常的数据,构造和输入normal情况的数据要保证不会触发异常,而构造和输入异常数据则要保证异常的顺利触发。

@ public normal_behavior
@ requires !(\exists int i; 0 <= i && i < people.length; people[i].equals(person));
@ assignable people;
@ ensures people.length == \old(people.length) + 1;
@ ensures (\forall int i; 0 <= i && i < \old(people.length);
@          (\exists int j; 0 <= j && j < people.length; people[j] == (\old(people[i]))));
@ ensures (\exists int i; 0 <= i && i < people.length; people[i] == person);
@ also
@ public exceptional_behavior
@ signals (EqualPersonIdException e) (\exists int i; 0 <= i && i < people.length;
@                                     people[i].equals(person));

根据normal情况的边界来准备测试数据

JML规格中的正常情况根据边界条件分为多种,如本单元中Network类的addToGroup方法,当人数超过1111时,虽然不会触发异常,但也无法顺利添加。

@ public normal_behavior
@ requires (\exists int i; 0 <= i && i < groups.length; groups[i].getId() == id2) &&
@           (\exists int i; 0 <= i && i < people.length; people[i].getId() == id1) &&
@            getGroup(id2).hasPerson(getPerson(id1)) == false &&
@             getGroup(id2).people.length < 1111;
@ assignable getGroup(id2).people;
@ ensures (\forall Person i; \old(getGroup(id2).hasPerson(i));
@          getGroup(id2).hasPerson(i));
@ ensures \old(getGroup(id2).people.length) == getGroup(id2).people.length - 1;
@ ensures getGroup(id2).hasPerson(getPerson(id1));
@ also
@ public normal_behavior
@ requires (\exists int i; 0 <= i && i < groups.length; groups[i].getId() == id2) &&
@           (\exists int i; 0 <= i && i < people.length; people[i].getId() == id1) &&
@            getGroup(id2).hasPerson(getPerson(id1)) == false && 
@             getGroup(id2).people.length >= 1111;
@ assignable \nothing;

根据JML规格的前提构造覆盖所有真值情况的数据

JML规格的前提字段(requires)一般包含一条或多条真值语句,构造数据应尽可能覆盖所有真值组合。

@ requires (\exists int i; 0 <= i && i < groups.length; groups[i].getId() == id2) &&
@           (\exists int i; 0 <= i && i < people.length; people[i].getId() == id1) &&
@            getGroup(id2).hasPerson(getPerson(id1)) == true;

白盒测试

除了构造数据进行黑盒测试,白盒测试则是将实现的方法与JML规格进行细致比对,从而找出错误。(特别是在对拍后有分歧时)

梳理本单元的架构设计,分析自己的图模型构建和维护策略

为了满足基本的JML规格要求,图模型只需要:

但为了顺利通过测试,我还做了如下维护:

按照作业分析代码实现出现的性能问题和修复情况

作业一:

若queryBlockSum方法按照JML规格采用双循环实现,复杂度最高为O(n*n),但可能由于java的各种封装的类的实现原因,在实际使用中时间大于O(n*n),于是最终被hack。

修复时:参考了同组一个人的代码,发现queryBlockSum()的本质是图中分支的总数,只要维护一个初始值为0的变量,每次addPerson时增一,addRelation且不增加闭环时减一,即为所求总数。

作业二:

queryLeastConnection方法实际为求最小生成树的问题,可以按评论区里的用prim算法加堆优化或者kruskal算法加并查集来取得最佳效果。我选择了后者,且在测试中没有出现问题。

作业三:

sendIndirectMessage方法为求最短路径的算法,使用dijkstra算法的时间复杂度为O(n*n),我没有吸取第一次作业的教训去很好地优化他,结果测试又挂了。一种比较简单粗暴的方法是在每次使用dijkstra算法时会计算出除目标两点外的其他最短路径,将他们统统存在Map里,即可达到很好地时间复杂度(但空间复杂度高)。另一种优化方法是对路径进行堆排序。

请针对下页ppt内容对Network进行扩展,并给出相应的JML规格

假设出现了几种不同的Person

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

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

public interface Network {

    /*@ public instance model non_null Producer[] producers;
      @ public instance model non_null Customer[] customers;
      @ public instance model non_null Advertiser[] advertiser;
      @ public instance model non_null Advert[] adverts;
      @*/


    /*@ public normal_behavior
      @ requires !(\exists int i; 0 <= i && i < adverts.length; adverts[i].equals(advert));
      @ assignable adverts;
      @ ensures adverts.length == \old(adverts.length) + 1;
      @ ensures (\forall int i; 0 <= i && i < \old(adverts.length);
      @          (\exists int j; 0 <= j && j < adverts.length; adverts[j].equals(\old(adverts[i]))));
      @ ensures (\exists int i; 0 <= i && i < adverts.length; adverts[i].equals(advert));
      @*/
    //由Advertiser调用,投放广告.
    public void sendAdvert(Advert advert);

    /*@ public normal_behavior
      @ requires advertisers.contains(advertiser);
      @ assignable advertiser.getAdvert();
      @ ensures \old(advertiser.getAdvert().size()) == advertiser.getAdvert().size() - 1;
      @ ensures (\forall int i; 0 <= i && i < \old(advertiser.getAdvert().size());
      @         (\exists int j; 0 <= j && j < advertiser.getAdvert().size();
      @             advertiser.getAdvert().get(j) == \old(advertiser.getAdvert()).get(i)));
      @ ensures (\exists int i; 0 <= i && i < advertiser.getAdvert().size();
      @             advertiser.getAdvert().get(i) == advert)
      @*/
    //由Producer调用,传给Advertiser,让Advertiser投放广告.
    public void sendAdvert(Advertiser advertiser, Advert advert);

    /*@ public normal_behavior
      @ requires customers.contains(customer);
      @ assignable customer.getBag();
      @ ensures \old(customer.getBag().size()) == customer.getBag().size() - 1;
      @ ensures (\forall int i; 0 <= i && i < \old(customer.getBag().size());
      @         (\exists int j; 0 <= j && j < customer.getBag().size();
      @             customer.getBag().get(j) == \old(customer.getBag()).get(i)));
      @ ensures (\exists int i; 0 <= i && i < customer.getBag().size();
      @             customer.getBag().get(i) == product)
      @*/
    //由Producer调用,完成购买信息。
    public void sendProduct(Customer customer, Product product);

    /*@ public normal_behavior
      @ requires advertisers.contains(advertiser);
      @ assignable advertiser.getOffer();
      @ ensures \old(advertiser.getOffer().size()) == advertiser.getOffer().size() - 1;
      @ ensures (\forall int i; 0 <= i && i < \old(advertiser.getOffer().size());
      @         (\exists int j; 0 <= j && j < advertiser.getOffer().size();
      @             advertiser.getOffer().get(j) == \old(advertiser.getOffer()).get(i)));
      @ ensures (\exists int i; 0 <= i && i < advertiser.getOffer().size();
      @             advertiser.getOffer().get(i) == offer)
      @*/
    //由Customer调用,发送给Advertiser购买消息.
    public void sendOffer(Advertiser advertiser, Offer offer);

    /*@ public normal_behavior
      @ requires producers.contains(producer);
      @ assignable producer.getOffer();
      @ ensures \old(producer.getOffer().size()) == producer.getOffer().size() - 1;
      @ ensures (\forall int i; 0 <= i && i < \old(producer.getOffer().size());
      @         (\exists int j; 0 <= j && j < producer.getOffer().size();
      @             advertiser.getOffer().get(j) == \old(producer.getOffer()).get(i)));
      @ ensures (\exists int i; 0 <= i && i < producer.getOffer().size();
      @             producer.getOffer().get(i) == offer)
      @*/
    //由Advertiser调用,发送给Producer购买信息.
    public void sendOffer(Producer producer, Offer offer);
}

感想

​ 任务相对轻松的一个单元,但JML规格设计思想以及规范,Junit单元化测试,都是重点难点。

​ 但纸上得来终觉浅,没有一个庞大的工程来做印证,我始终无法切身体会到这份重要。

​ 另外由于Junit的使用比较麻烦,我只在第一次作业时进行了尝试,后来还是改用手撸评测机进行对拍测试,因为比较方便,看到别人能对JML进行几乎100%覆盖率的测试,自愧不如,也是本单元最大的遗憾了。

标签:OO,测试,normal,BUAA,Person,规格,JML,Unit3,public
来源: https://www.cnblogs.com/pxtttt/p/16343685.html