标签:OO Network JML Person 规格 getMessage 2022 Unit3 id
2022-OO-Unit3
mashiroly
1. 概述
又到轻松愉快的博客周了(赫赫,hw13似乎不是很容易呢),回顾一下过去一个月做了什么吧。
本单元的目标是学习基于规格的层次化设计,需求是在JML规格的指导下,实现一个模拟社交关系系统。作业重点是阅读和理解JML规格,掌握异常处理和测试方法,体会设计和实现的分离。
2. 架构设计
2.1 图结构
引入图的划分Partition
,可将社交网络如下图建模,基本囊括了所有关联关系。
具体而言,自上而下的构建可分为以下几步:
-
Network
中维护三个集合。为方便查找,使用HashMap<id, Class>
。 -
引入新类
Relation
(也就是Edge
类),维护关联的Person
和value
。在
Network
中维护id(自增),同样将HashMap<id,Edge> EdgeSet
作为属性。 -
引入新类
Partition
,表示以Person
通过Relation
关联的连通子图(划分)。其保存划分内部的所有Vectex(Person)
和Edge(Relation)
,方便查询。在
Network
中维护id(并查集更新根结点id),同样将HashMap<id,Partition>PartitionSet
作为属性。 -
根据JML规格撰写三个类,对于集合能用
HashMap<id, Class>
尽用。注意Person
的MessageSet
需要维护队列。
设计与实现分离初步体现于此,我们不需要如JML描述逐个遍历,只要保证符合规格,可以选择合适的数据结构。
2.2 维护策略
不涉及Partition
的结构维护:
- 基本策略:由于大量使用HashMap,几乎只需要使用
put()
进行添加操作 。有遍历时删除操作的Map可以使用线程安全的ConcurrentHashMap。Arraylist的删除使用removeIf()
。 - 不降复杂度的维护:部分指令复杂度无法优化到O(1),且随图结构更新改变,如
qrm
,sim
。维护一个有效位。
三次作业经历的最大“重构”应该是:为提高并查集+kruskal的效率,从hw9到hw10引入Partition
,维护也需要更多操作。
- 并查集:路径压缩。
ar
指令执行时合并划分,更新划分属性,将划分内所有Person
新定义的ParentId
属性设为划分内的某个id,这个id更新为Network
中该划分在Map中的key。 - 平均年龄、方差等
Group
属性:Group
自身维护ageSum
,ageSquareSum
,在atg
,dfg
时更新,时间复杂度能做到O(1)。
公式$$D(X)=E(X2)-E^2(X)$$计算方差,与JML描述精度不同。
参考讨论区帖子,有以下公式不丢失精度:$$D(X) = \frac{\Sigma X^2 -2\overline{X}}{n}+(\overline{X})^2$$
3. 性能问题和bug修复
3.1 hw9(悲
周六下午,才测出未堆优化的Prim被链式数据+qci打穿了,临时改写不带并查集的kruskal,结果完全写错。强测也寄的很惨。
此次作业未引入并查集和划分,qbs在ar时更新,复杂度O(1)。
3.2 hw10
强测未发现bug。
引入了并查集+kruskal,将qci复杂度优化到O(nlogE) 。
但是qgav复杂度O(n^2),被hack TLE了。之后将qgvs和qgav均优化到O(1)
3.3 hw11
强测未发现bug。
sim使用堆优化的dijkstra,复杂度为O(nlogE)。
互测也没有被卡性能,但是dce规格理解有误,以为是删去所有EmojiMessage,被hack了。感谢仅10条指令让我一眼看出bug的好哥哥!
4. 测试设计
1. Junit实践
使用Junit编写测试方法,个人的操作是通过完全遵守JML规格重新撰写方法,用assertEquals()
判断方法实现是否符合不变式。庞大的测试类也需要维护一系列属性(全局变量),也需要面向对象,也需要封装好各种修改图结构的方法。
但实际编写中,不可能完全照搬JML,例如sim
,qlc
等方法,规格上就有“寻找一个集合(子图,链)”。随着方法更加复杂,测试方法写得越来越像实现的方法。hw10和hw11中,也因此被劝退,没有继续进行Junit编写。
2. 随机数据生成与对拍
最后还是采用python写随机数据生成器,并进行覆盖性测试。为保证数据质量,生成器也要维护好Person、Group、Message集合(使用id),并从集合中取出id生成指令。为保障异常覆盖率,我人为地设置随机数按一定比例生成错误指令。同时手动构造边界数据,如链式图、完全图、1111等。
这是10w条+5k人的数据,可以看到覆盖率还是有保证的。未覆盖的方法几乎都是规格有定义、但实现上没有使用的方法。
正确结果唯一就是好啊,不用写正确性判断,和小伙伴对拍就好了。(
5. Network拓展
假设出现了几种不同的Person
- Advertiser:持续向外发送产品广告
- Producer:产品生产商,通过Advertiser来销售产品
- Customer:消费者,会关注广告并选择和自己偏好匹配的产品来购买 -- 所谓购买,就是直接通过Advertiser给相应Producer发一个购买消息
- Person:吃瓜群众,不发广告,不买东西,不卖东西
如此Network可以支持市场营销,并能查询某种商品的销售额和销售路径等 请讨论如何对Network扩展,给出相关接口方法,并选择3个核心业务功能的接口方法撰写JML规格(借鉴所总结的JML规格模式)
- 新增
Advertiser
,Producer
,Customer
类继承Person
类; - 新增
Product
类; - 新增
PurchaseMeassage
,Advertisement
类继承Message
类;
Network
中应该新增方法:添加产品,发送广告,购买商品,查询商品销售额,查询商品销售路径等。
public interface Network {
/*@ public instance model non_null Produce[] produces;
@ ...
@*/
}
- 添加产品
addProducer
/*@ public normal_behavior
@ requires (\exists int i;0 <= i && i < people.length;people[i].getId() == id && people[i] instance of Procuder);
@ requires !(\exists int i;0 <= i && i < produces.length; produces[i].equals(produce));
@ assignable people;
@ ensures produce.length == \old(produce.length) + 1;
@ ensures (\forall int i; 0 <= i && i < \old(produces.length);
@ (\exists int j; 0 <= j && j < produces.length; produces[j] == (\old(produces[i]))));
@ ensures (\exists int i; 0 <= i && i < people.length; people[i] == person);
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) (\forall int i; 0 <= i && i < people.length);
@ people[i].getId() != id
@ || (people[i].getId() == id && !(people[i] instance of Producer));
@ public exceptional_behavior
@ signals (EqualProduceIdException e) (\exists int i; 0 <= i
@ && i < produces.length;produces[i].equals(person));
@*/
public void addProduce(/*@ non_null @*/int id, Produce produce)
throws PersonIdNotFoundException, EqualProduceIdException;
- 发送广告
sendAdvertisement
/*@ public normal_behavior
@ requires getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
getMessage(id).getPerson1() != getMessage(id).getPerson2();
@ requires containsMessage(id) && getMessage(id) instanceof Advertisement getMessage(id).getType() == 0 &&;
@ assignable messages;
@ assignalbe getMessage(id).getPerson2().messages;
@ 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 (\forall int i; 0 <= i && i < \old(getMessage(id).getPerson2().getMessages().size());\old(getMessage(id)).getPerson2().getMessages().get(i+1) == \old(getMessage(id).getPerson2().getMessages().get(i)));
@ also
@ public exceptional_behavior
@ requires containsMessage(id) && getMessage(id).getType() == 1 && getMessage(id) instanceof Advertisement
@ requires getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1());
@ assignable people[*].messages
@ 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 (\forall Person p; \old(getMessage(id)).getGroup().hasPerson(p);(\forall int i; 0 <= i && i < \old(p.getMessages().size());\old(p.getMessages().get(i+1) == \old(p.getMessages().get(i))));
@ signals (MessageIdNotFoundException e) !containsMessage(id);
@ signals (MessageIdNotFoundException e) containsMessage(id) && !(getMessage(id) instanceof Advertisement);
@ signals (RelationNotFoundException e) containsMessage(id) && getMessage(id) instanceof Advertisement && getMessage(id).getType() == 0 &&!(getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()));
@ signals (PersonIdNotFoundException e) containsMessage(id) && getMessage(id) instanceof Advertisement && getMessage(id).getType() == 1 && !(getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1()));
@ */
public void sendAdvertisement(int id) throws MessageIdNotFoundException,PersonIdNotFoundException,RelationNotFoundException;
- 查询产品销售额
queryPrice
/*@ public normal_behavior
@ requires (\exists int i; 0 <= i && i < produces.length);produces[i].getId() == id);
@ assignalbe none;
@ ensures (\exists int i; 0 <= i && i < produces.length);produces[i].getId() == id && \result == produces[i].getPrice());
@ public exceptional_behavior
@ signals (ProduceIdNotFoundException e) !(\exists int i; 0 <= i && i < produces.length);produces[i].getId() == id);
@ */
public void queryPrice(/*@ non_null @*/int id) throws ProduceIdNotFoundException
标签:OO,Network,JML,Person,规格,getMessage,2022,Unit3,id
来源: https://www.cnblogs.com/mashiroly/p/16348328.html
本站声明:
1. iCode9 技术分享网(下文简称本站)提供的所有内容,仅供技术学习、探讨和分享;
2. 关于本站的所有留言、评论、转载及引用,纯属内容发起人的个人观点,与本站观点和立场无关;
3. 关于本站的所有言论和文字,纯属内容发起人的个人观点,与本站观点和立场无关;
4. 本站文章均是网友提供,不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属;如您发现该文章侵犯了您的权益,可联系我们第一时间进行删除;
5. 本站为非盈利性的个人网站,所有内容不会用来进行牟利,也不会利用任何形式的广告来间接获益,纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。