面向对象第三单元分析与总结
作者:互联网
面向对象第三单元分析与总结
前言
第三单元结束,面向对象课程马上就结束了,好耶!
本单元终点考察对JML规格理解与代码实现,需要了解基本的JML语法和语义,以及具备根据JML给出的规格编写Java代码的能力。在具体的作业中还兼具考察了部分图论的算法实现,练习了基于junit的程序测试方法,总的来说还是十分有趣的。
在撰写本篇博客之前,我回去认真读了我写的前两个单元的总结博客,结果看到一半直接绷不住。设想我如果是个萌新,看到这种车轱辘话来回说,除了我自己没人能看懂的博客,估计也挺崩溃的。
本次总结按照要求分为以下几个部分:
(1) 单元测试——分析在本单元自测过程中如何利用JML规格来准备测试数据
(2) 架构分析——梳理本单元的架构设计,分析自己的图模型构建和维护策略
(3) 性能与优化——按照作业分析代码实现出现的性能问题和修复情况
(4) 扩展JML实践——对Network进行扩展,并给出相应的JML规格
(5) 心得体会——本单元学习体会。
力求简洁明了,不说废话好吧。
突然明白为什么会有博客这个环节了。
1. 单元测试
首先从JML规格的特性角度考虑,JML提供了对方法和类型的规格定义手段。相比于模糊的自然语言,逻辑严格的规格对于代码的测试有着十分重要的参考意义。
在本单元作业中,对于包含具体功能的函数,我从两个方面来测试函数的正确性:一是通过保证JML的前置条件成立,测试后置条件的正确性,以及抛出异常的时机。二是随机生成大量指令与数据,广泛覆盖测试。
举一个简单的例子:
- JML规格测试
/*@ 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));
@*/
public void addPerson(/*@ non_null @*/Person person) throws EqualPersonIdException;
前置条件要求我们保证people
集合中不包含该Person
,那么我们可以通过添加重复数据来测试异常:
ap 1 p1 1
--> Ok
ap 1 p1 2
--> epi-1, 1-1
以及添加不重复的数据来测试后置条件:该person
有没有被添加进people
集合:
ap 1 p1 1
--> Ok
ap 2 p2 2
--> Ok
- 随机测试
在随机数据生成测试中,首先生成一批基础指令(ap, ag等)测试异常,再生成其他查询指令测试正确性。(仅参考,实际数据生成可以更加随机)
for (int i = 0; i < num; i++) { //ap指令
System.out.println("ap " + i + " P_" + i + " " + r.nextInt(200));
}
HashSet<Integer> set = new HashSet<>();
for (int i = 0; i < num; i++) { // ar指令
for (int j = 0; j < num; j++) {
if (!set.contains(j) && i != j) {
System.out.println("ar " + i + " " + j + " " + r.nextInt(1000));
}
}
set.add(i);
}
/*
am, ag, atg, sei等,遵守指导书数据限制
*/
2. 架构分析
由于JML是高度规格化的语言,我们只需在充分理解的基础上加以实现即可。接下来按照作业的顺序分析一下我自己的架构设计。
第九次作业
JML语言中对于集合的描述基本都采用数组的模式,在具体实现时可以灵活采用相应的数据结构与对应关系。
为了方便查询与计算,数据多采用HasMap
的形式。对于正确的输入数据,其id
唯一,即采用id
作为Key
。
在isCircle
函数中,我们需要查询图中两个点是否连通,我采用并查集的方法,添加专门的类UnionFind
并作为Network
的属性。
第十次作业
新添加了Message
,但没什么影响,同样是使用HashMap
存储。
在queryLeastConnection
函数中要求计算最小生成树,这里要用到边集,于是我新添加Edge
类,作为MyNetwork
的属性,每当添加关系(addRelation
)的时候就添加一条边。
public class Edge {
private int id1;
private int id2;
private int edge;
}
第十一次作业
新增NoticeMessage
, RedEnvelopeMessage
, EmojiMessage
全部继承原先的Message
接口。为了充分利用前几次作业的代码,我采用“继承+实现”的结构,三个新增类实现对应的接口,同时继承前几次作业的MyMessage
类(因为Message
本身没有变化),并按要求更改构造函数。
public class MyEmojiMessage extends MyMessage implements EmojiMessage {}
public class MyNoticeMessage extends MyMessage implements NoticeMessage {}
public class MyRedEnvelopeMessage extends MyMessage implements RedEnvelopeMessage {}
在sendIndirectMessage
函数中需要计算最短路径,于是我添加Dijkstra
类。由于在前次作业中已经存储了一个边集,这里最短路径算法就可以直接拿来用,以邻接表计算。
3.性能与优化
本单元最关键的优化点在于规避多层循环。其中主要有两方面:降低查询开销以及优化算法复杂度。
降低查询开销
-
使用
HashMap
,HashSet
等来存储数据,避免使用List
。 -
数据边读入边计算,随时更新,调用函数时只需读取结果即可,避免多次重复无意义的计算。
优化算法
第九次作业中的isCircle
要求我们找出关系图中两点是否连通,这里使用路径压缩的并查集实现。在实际使用时,与降低查询开销的道理一样,需要在添加数据时就更新结果,这样调用函数的时候就可以直接查询结果,避免无意义的重复计算,下面几次作业都同理。
第十次作业中的queryLeastConnection
要计算最小生成树,但由于图本身不保证全连通,所以是求一个点所在的连通分量的最小生成树。我是直接用kruskal
算法求直接求最小生成森林,再遍历这个森林的根节点找出给定点所在的最小生成树。
第十一次作业中的sendIndirectMessage
函数需要计算最短路径,这个就是最短路径算法的直接实践。我这里用的是邻接表实现,对稀疏图效果很好。在某一次实验代码中给出了一个小根堆的实现,用来优化最短路径挺好的。java本身也有PriorityQueue
这样的数据结构可以直接拿来用,逻辑是一样的。
4. 扩展JML实践
假设出现了几种不同的Person
- Advertiser:持续向外发送产品广告
- Producer:产品生产商,通过Advertiser来销售产品
- Customer:消费者,会关注广告并选择和自己偏好匹配的产品来购买 -- 所谓购买,就是直接通过Advertiser给相应Producer发一个购买消息
- Person:吃瓜群众,不发广告,不买东西,不卖东西
如此Network可以支持市场营销,并能查询某种商品的销售额和销售路径等 请讨论如何对Network扩展,给出相关接口方法,并选择3个核心业务功能的接口方法撰写JML规格(借鉴所总结的JML规格模式)
Advertiser
, Producer
, Customer
这三个可以继承原有的Person
, 实现时就可以利用原有的MyPerson
类,同时添加各自独有的方法。
添加两个Message
的子类AdvertiseMessage
和ShoppingMessage
.
与上述生产产品对应,Network
中添加产品集合。
核心功能接口方法:
Advertiser
发广告addAdvertiseMessage
/*@ public normal_behavior
@ requires containsMessage(id) && getMessage(id) instanceof AdvertiseMessage
@ assignable 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 < people.length; (\old(getMessage(id)).getPerson1().isLinked(people[i]) && people[i] instanceof Customer) ===> (people[i].getMessages().get(0).equals(\old(getMessage(id)))));
@ ensures (\forall int i; 0 <= i && i < people.length; (\old(getMessage(id)).getPerson1().isLinked(people[i]) && people[i] instanceof Customer) ===> (people[i].getMessages().size() == \old(people[i].getMessages().size()) + 1));
@ also
@ public exceptional_behavior
@ signals (MessageIdNotFoundException e) !containsMessage(id);
@ signals (AdvertiseMessageNotFoundException e) containsMessage(id) && !(getMessage(id) instanceof AdvertiseMessage);
@*/
public void addAdvertiseMessage(int id) throws MessageIdNotFoundException, AdvertiseMessageNotFoundException;
Producer
制造产品:
/*@ public normal_behavior
@ requires !(\exists int i; 0 <= i && i < products.length; peoducts[i].equals(product));
@ assignable products;
@ ensures products.length == \old(products.length) + 1;
@ ensures (\forall int i; 0 <= i && i < \old(products.length); (\exists int j; 0 <= j && j < products.length; products[j] == (\old(products[i]))));
@ ensures (\exists int i; 0 <= i && i < products.length; products[i] == product);
@ also
@ public exceptional_behavior
@ signals (EqualProductIdException e) (\exists int i; 0 <= i && i < products.length; peoducts[i].equals(product));
@*/
public void addProduct(Product product) throws EqualProductIdException;
Customer
购买产品:
/*@ public normal_behavior
@ requires contains(personId) && getPerson(personId) instanceof Customer
@ requires containsMessage(messageId) && getMessage(messageId) instanceof ShoppingMessage
@ requires getPerson(personId).hasAdvertiseMessage(getPerson(personId).productId) && getPerson(personId).getAdvertiseMessage(getPerson(personId).productId).getPerson1().equals(getMessage(messageId).getPerson1())
@ assignable messages;
@ assignable sellOutList;
@ ensures !containsMessage(messageId) && 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(messageId)).getPerson2().getMessages().get(i+1) == \old(getMessage(messageId).getPerson2().getMessages().get(i)));
@ ensures \old(getMessage(messageId)).getPerson2().getMessages().get(0).equals(\old(getMessage(messageId)));
@ ensures \old(getMessage(messageId)).getPerson2().getMessages().size() == \old(getMessage(messageId).getPerson2().getMessages().size()) + 1;
@ ensures (\exist int i; 0 <= i && i < productIdList && productIdList[i] == getPerson(personId).productId; sellOutList[i] == \old(sellOutList[i]) + 1)
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(personId);
@ signals (NotCustomerException e) contains(personId) && !(getPerson(personId) instanceof Customer)
@ signals (MessageIdNotFoundException e) !containsMessage(messageId);
@ signals (NotShoppingMessageException e) containsMessage(messageId) && !(getMessage(messageId) instanceof ShoppingMessage);
@ signals (NoAdvertiseMessageException) !(getPerson(personId).hasAdvertiseMessage(getPerson(personId).productId) && getPerson(personId).getAdvertiseMessage(getPerson(personId).productId).getPerson1().equals(getMessage(messageId).getPerson1()))
@*/
public void shopping(int personId, int messageId) throws MessageIdNotFoundException, NotShoppingMessageException, PersonIdNotFoundException, NotCustomerException, NoAdvertiseMessageException;
5. 心得体会
相比于前两个单元,本单元的难度显著降低,因为我们不需要自己去设计复杂的方法,只需在JML规格的基础上对已有接口中的函数进行实现即可。稍难的算法部分其实原理都在离散数学中都学过,这次只是将其用代码实现。
相对于写代码,我认为本单元更适合着眼于测试。程序测试本身也是一门学问,懂得如何测试程序,在之后的学习工作中都十分重要。这次我们学习了用Junit来测试,但其工具链我觉得不太好用,经常会报一些莫名其妙的错误,当然重要的在于方法不是工具。
理论课上讲的契约式编程,还有研讨课上大佬分享的测试机制都让我受益匪浅。
本单元的正确率其实我不太满意,在难度下来之后也暴露出我一个问题,对于细节的把控不太好。比如在实现最短路径算法的时候将person
的id
直接拿来当做index
使用,结果不出意外数组溢出。当然我自己过于薄弱的测试也是主要原因。后续针对程序测试部分也要多作学习。
标签:总结,&&,int,测试,public,面向对象,JML,id,单元 来源: https://www.cnblogs.com/135qaz/p/16345825.html