第三单元总结
作者:互联网
第三单元总结
分析在本单元自测过程中如何利用JML规格来准备测试数据
本单元自测进行得较少,自测的主要形式是和小伙伴进行对拍。由数据生成器生成若干组测试数据,再将自己和小伙伴的输出进行比对。在对拍的过程中,能够对正确性进行查验,但对复杂性的查验效果不是很好。
梳理本单元的架构设计,分析自己的图模型构建和维护策略
MyNetwork
该类实现了NetWork
接口,是整个项目的主干类。对其采取的优化策略如下。
存储Peple、Group、Message的容器选用了HashMap
代替ArrayList
,利用id
查找相应的对象,提高了查找的效率。``
在计算blockSum
时选用动态更新的方式,每次增添人员、增添关系时,对其进行更新,代替了每次调用queryBlockSum()
函数便重新计算的方式,提高了计算效率。
为实现对isCircle
的判断,采用了并查集算法,并对其进行了秩优化,在每次查找上级时,都对并查集进行更新。
为实现queryLeastConnection()
函数,选用了Prim算法,并利用并查集对该算法进行了优化,提高了性能。
为实现sendIndirectMessage()
函数,选用了迪杰斯特拉算法,并对其进行了堆优化。
NetWork
接口中的其他函数,均按照规格书写,未做相应优化。
MyGroup
该类实现了Group
接口。
采用HashMap
容器存储People
,建立了PersonId
到Person
的映射。
在计算valueSum
和ageSum
时,采用动态更新,每次增添人员和删减人员时对其进行更新,调用相关get
函数时,只是返回当前值,并不重新计算。
MyPerson类
该类实现了Person
接口。
在该类中,利用HashMap
容器存储acquaintance
,建立了PersonId
到Person
的映射,在调用isLink()
函数时,不用循环查找,提高了性能。同时利用HashMap
容器存储value
,建立了PersonId
到value
的映射,在调用queryValue()
函数时,同样提高了效率。
异常类
作业中对于异常类的要求是记录该类异常发生的总次数,及记录每个id触发异常的次数。由于各类异常记录次数的行为高度相似,因此我在每个异常类中都添加了一个相同的static
的Counter
属性,用以实现上述的计数功能,这样实现了代码的抽象和集中,便于修改和维护。以EqualPersonIdException异常为例:
按照作业分析代码实现出现的性能问题和修复情况
第一次作业
第一次作业的性能问题出现在queryBlockSum()
函数。该函数的功能是返回network的BlockSum值,修复前queryBlockSum()
函数的实现策略是:每次调用该函数,便进行一次二重循环来计算network的BlockSum值。修复后,在MyNetwork
类中新增了BlockSum
属性,每次调用addPerson()
函数和addRelation()
函数时,对BlockSum
属性进行更新。具体的更新方法是,调用addPerson()
函数时,BlockSum++
;调用addRelation()
函数时,首先判断两个被添加关系的人的根节点是否相同,如果相同,则不做操作,如果不相同,则证明这两个人在添加关系之前原本不想连,添加关系后变成了相连的,BlockSum
需要减1.
在修复时,原本以为导致CTLE的原因是并查集没有实现好,对并查集进行了秩优化后,并没有得到改观,经过朋友的提醒后,才发现是queryBlockSum()
函数的问题。写完成作业的时候,注意力全部都放在了并查集的实现上,认为会从并查集这里卡CPU的运行时间,实现并查集后就没有对其他函数进行优化,导致出现了性能问题。
第二次作业
第二次作业的性能问题出现在queryGroupValueSum()
函数。修复前,每次调用此函数,都会进行一次双重循环计算Group
的ValueSum
。第二次作业的修复策略同第一作业类似,在MyGroup
类中新增了ValueSum
属性。在调用addPerson()
,delPerson()
和addRelation()
函数时,对该属性进行动态更新。
第三次作业
第三次作业的性能问题出在了sendIndirectMessage()
函数。该函数的核心部分为最短路径的计算,初始时采用的是迪杰斯特拉算法进行最短路径的计算,并没有进行优化。修复时,采用堆优化的方式对最短路径的计算算法进行了优化。
拓展的JML规格
为了简化设计,假设每个Advertiser
只对接唯一一个Producer
,且每个Producer
可生产所有类型的商品。
生产商品
/*
@ public normal_behaviour
@ requires containsProducer(producerId);
@ assignable getProducer(producerId).goods;
@ ensures getProducer(producerId).goods.length =
@ \old(getProducer(producerId).goods.length) + 1;
@ ensures (\forall int i;0 <= i && i <\old(getProducer(producerId).goods.length);
@ getProducer(producerId).goods[i] == \old(getProducer(producerId).goods[i]));
@ ensures getProducer(producerId).goods[getProducer(producerId).goods.length - 1].type == type;
@ also
@ public exceptional_behavior
@ signals (ProducerNotFound e) !containsProducer(producerId);
*/
public void produceGoods(int type,int producerId);
该函数的功能是让id
为producerId
的producer
,生产一个类型为type
的商品,当不存在该producer
时,抛出异常。
销售商品
/*@ public normal_behavior
@ requires getAdvertiser(advertiserId).getProducer.containsGoods(type);
@ ensures getAdvertiser(advertiserId).getProducer.goods.length = \old(getAdvertiser(advertiserId).getProducer.goods.length) - 1;
@ ensures (\min int a;0 <= a && a < \old(getAdvertiser(advertiserId).getProducer.goods.length);
@ \old(getAdvertiser(advertiserId).getProducer.goods[a].type) == type);
@ ensures (\forall int i;0 <= i && i < a;\old(getAdvertiser(advertiserId).getProducer.goods[i]) == getAdvertiser(advertiserId).getProducer.goods[i]);
@ ensures (\forall int i;a < i && i < \old(getAdvertiser(advertiserId).getProducer.goods.length);\old(getAdvertiser(advertiserId).getProducer.goods[i]) == getAdvertiser(advertiserId).getProducer.goods[i - 1]);
@ ensures getAdvertiser(advertiserId).goods.length = \old(getAdvertiser(advertiserId).goods.length) + 1;
@ ensures (\forall int i;0 <= i && i <\old(getAdvertiser(advertiserId).goods.length);
@ getAdvertiser(advertiserId).goods[i] == \old(getAdvertiser(advertiserId).goods[i]));
@ ensures getAdvertiser(advertiserId).goods[getAdvertiser(advertiserId).goods.length - 1].type == type;
@ also
@ public exceptional_behavior
@ signals (GoodsNotFoundException e) !getAdvertiser(advertiserId).getProducer.containsGoods(type);
*/
public void sellGoods(int type, int advertiserId);
该函数的功能是让id
为advertiserId
的Advertiser
从他的专属生产商那里购进一个类型为type
的商品,当生产商没有该类商品的库存时,抛出异常。
购买商品
/*@ public normal_behavior
@ requires getAdvertiser(advertiserId).containsGoods(type);
@ ensures getAdvertiser(advertiserId).goods.length == \old(getAdvertiser(advertiserId).goods.length) - 1;
@ ensures (\min int a;0 <= a && a < \old(getAdvertiser(advertiserId).goods.length);
@ \old(getAdvertiser(advertiserId).goods[a].type) == type);
@ ensures (\forall int i;0 <= i && i < a;\old(getAdvertiser(advertiserId).goods[i]) == getAdvertiser(advertiserId).goods[i]);
@ ensures (\forall int i;a < i && i < \old(getAdvertiser(advertiserId).goods.length);\old(getAdvertiser(advertiserId).goods[i]) == getAdvertiser(advertiserId).goods[i - 1]);
@ ensures getCustomer(customerId).goods.length == \old(getCustomer(customerId).goods.length) + 1;
@ ensures (\forall int i;0 <= i && i <\old(getCustomer(customerId).goods.length);
@ getCustomer(customerId).goods[i] == \old(getCustomer(customerId).goods[i]));
@ ensures getCustomer(customerId).goods[getCustomer(customerId).goods.length - 1].type == type;
@ also
@ public exceptional_behavior
@ signals (GoodsNotFoundException e) !getAdvertiser(advertiserId).containsGoods(type);
*/
public void buyGoods(int type, int customerId, int advertiserId);
该函数的功能是让id
为customerId
的Customer
从id
为advertiserId
的Advertiser
那里购进一个类型为type
的商品,当中间商没有该类商品的库存时,抛出异常。
本单元学习体会
-
本单元的主要学习内容是JML规格,经过本单元的学习,我掌握了JML的基本知识,能够通过阅读规格,实现相应的功能,当然在具体实现过程中,还要关注效率和性能。
-
我也学到了有关JUit的基础知识。
-
经过本单元的学习,我认为JML规格十分重要。在软件开发和团队合作中发挥着重要的作用,因为目前代码开发量较小,且均为独立完成,规格的作用可能不是很明显。
-
在完成作业的过程中,我发现有些JML非常繁琐,很多层括号相嵌套,想要完全读懂需要一些时间,如何在保证其正确性的前提下,使规格变得更加简便易懂,是个值得思考的问题。
标签:总结,调用,函数,查集,作业,第三,advertiserId,goods,单元 来源: https://www.cnblogs.com/Natt1e/p/16343135.html