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

OO - 第三单元总结

作者:互联网

OO第三单元总结


要求

单元总结要求



第一次作业总结

分析


基本思路


具体实现


关键算法

并查集



基于度量的程序结构分析



第二次作业总结

分析


需求变更

新增内容:

数据限制变更:

迭代开发

新增:

修改:



关键算法

最小生成树算法



基于度量的程序结构分析



第三次作业总结

分析


需求变更

新增内容:

数据限制变更:

迭代开发

新增:

修改:



关键算法

最短路径算法



基于度量的程序结构分析



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



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



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



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

  /*@ public normal_behavior
    @ requires !(\exists int i; 0 <= i && i < getPerson(personId).products.length; getPerson(personId).products[i].getId() == id);
    @ assignable getPerson(personId).products ;
    @ ensures (\forall int i; 0 <= i && i < \old(getPerson(personId).products.length) ;
    @          getPerson(personId).products[i].getId() == id );
    @ ensures getPerson(personId).products.length == \old(getPerson(personId).products.length) + 1 ;
    @ ensures getPerson(personId).hasProduct(id);
    @ also
    @ public exceptional_behavior
    @ signals (EqualAdvertiseIdException e) (\exists int i; 0 <= i && i < getPerson(personId).products.length;
    @                                     getPerson(personId).products[i].getId() == id) ;
    @*/

    public void addProduct(String personId, Advertisement id);
/*@ public normal_behavior
       @ requires (\exists int i; 0 <= i && i < advertisers.length;
       @ advertisers.get(i).equals(advertiser));
       @ ensures money == \old(money) - product.getValue();
       @ ensures production.length == \old(production).length + 1;
       @ ensures (\exists int i; 0 <= i && i < production.length;
       @ production.get(i).equals(product));
       @*/
     public /*@ pure @*/ void buy(Advertiser advertiser, Product product);
 /* @ public normal_behavior
    @ requires (\exists int i; 0 <= i && i < customers.length;
    @ customers.get(i).equals(customer));
    @ ensures customer.getAdvertisements.length ==
    @ \old(customer.getAdvertisements).length + 1;
    @ ensures (\exists int i; 0 <= i && i < customer.getAdvertisements.length
    @ customer.getAdvertisements.get(i).equals(advertisement));
    @*/
    public /*@ pure @*/ void sendAdvertisement(Customer customer, Advertisement advertisement);


本单元学习体会



author: 20373864 谭立德

标签:OO,总结,代码,add,分组,JML,message,Id,单元
来源: https://www.cnblogs.com/master-tan/p/16347868.html