其他分享
首页 > 其他分享> > 第三单元总结

第三单元总结

作者:互联网

第三单元总结

第一次作业

本次作业思路

本次作业的bug

第二次作业

本次作业思路

本次作业bug

第三次作业

本次作业思路

本次作业bug

测试数据的准备

Network扩展

 /*@ public normal_behavior
      @ requires (\exists int i; 0 <= i && i < people.length; people[i].getId() == id2) &&
      @           (\exists int i; 0 <= i && i < advertisers.length; advertisers[i].getId() == id1) &&
      @            getPerson(id2).hasAdvertiser(getAdvertiser(id1)) == false;
      @ assignable getPerson(ide2).advertisers;
      @ ensures (\forall Advertiser i; \old(getPerson(id2).hasAdvertiser(i));
      @          getPerson(id2).hasAdvertiser(i));
      @ ensures \old(getPerson(id2).advertisers.length) == getPerson(id2).advertisers.length - 1;
      @ ensures getPerson(id2).hasAdvertiser(getAdvertiser(id1));
      @ also
      @ public exceptional_behavior
      @ signals (advertiserIdNotFoundException e) !(\exists int i; 0 <= i && i < advertisers.length;
      @          advertisers[i].getId() == id1);
      @ signals (PersonIdNotFoundException e) (\exists int i; 0 <= i && i < advertisers.length;
      @          advertisers[i].getId() == id1) && !(\exists int i; 0 <= i && i < people.length;
      @           people[i].getId() == id2);
      @ signals (EqualadvertiserIdException e) (\exists int i; 0 <= i && i < advertisers.length;
      @         advertisers[i].getId() == id1) && (\exists int i; 0 <= i && i < people.length;
      @           people[i].getId() == id2) && getPerson(id2).advertisers(getAdvertiser(id1));
      @*/
    public void addAdvertiserToPerson(/*@ non_null @*/int id1,int id2) throws advertiserIdNotFoundException e,PersonIdNotFoundException,EqualadvertiserIdException;
/*@ public normal_behavior
      @ requires (\exists int i; 0 <= i && i < advertiser.length; advertiser[i].getId() == id1) &&
      @           (\exists int i; 0 <= i && i < getAdvertiser(id1).commodities.length; commodities[i].getId() == id2) 
      @ ensures (\forall commodity i; \old(getAdvertiser(id1).hasCommodities(i));
      @          getAdvertiser(id1).hasCommodities(i));
      @ ensures \old(getAdvertiser(id2).commodities.length) == getAdvertiser(id1).commodities.length ;
      @ ensures \result == getAdvertiser(id1).getCommidity(id2).price;
      @ also
      @ public exceptional_behavior
      @ signals (advertiserIdNotFoundException e) !(\exists int i; 0 <= i && i < advertisers.length;
      @          advertisers[i].getId() == id1);
      @ signals (CommodityIdNotFoundException e) (\exists int i; 0 <= i && i < advertisers.length;
      @          advertisers[i].getId() == id1) && !(\exists int i; 0 <= i && i < getAdvertiser(id1).commodities.length.length;
      @           getAdvertiser(id1).commodities[i].getId() == id2);@/
    public int addAdvertiserToPerson(int id1,int id2) throws advertiserIdNotFoundException,CommodityIdNotFoundException;
/*@ public normal_behavior
      @ requires (\exists int i; 0 <= i && i < people.length; people[i].getId() == personId);
       @ requires (\exists int i; 0 <= i && i < advertiser.length; advertiser[i].getId() == advertiserId) &&
      @           (\exists int i; 0 <= i && i < getAdvertiser(id1).commodities.length; commodities[i].getId() == commodityId) 
      @ ensures getPerson(personId).money = \old(getPerson(personId).money) - getProduct(commodityId).getValue;
      @ ensures getSaler(advertiserId).getProduct(commodityId).getLeftNum() = \old(getSaler(advertiserId).getProduct(commodityId).getleftNum()) - 1;
      @also
      @ public exceptional_behavior
      @ signals (PeronIdNotFoundException) !(\exists int i; 0 <= i && i < people.length; people[i].getId() == personId);
      @ also
      @ public exceptional_behavior
      @ signals (PeronIdNotFoundException) (\exists int i; 0 <= i && i < people.length; people[i].getId() == personId)&&!(\exists int i; 0 <= i && i < advertiser.length; advertiser[i].getId() == advertiserId);
      @ also
      @ public exceptional_behavior
      @ signals (commodityIdNotFoundException) (\exists int i; 0 <= i && i < people.length; people[i].getId() == personId)&&
      @(\exists int i; 0 <= i && i < advertiser.length; advertiser[i].getId() == advertiserId)&&
      @!(\exists int i; 0 <= i && i < getAdvertiser(id1).commodities.length; commodities[i].getId() == commodityId) ;
      @*/
    public /*@ pure @*/void purchaseProduct(int personId, int commodityId, int advertiserId) throws PeronIdNotFoundException, commodityIdNotFoundException;

作业感想

标签:总结,函数,bug,记录,作业,节点,第三,id,单元
来源: https://www.cnblogs.com/stubborn-rookie/p/16343069.html