其他分享
首页 > 其他分享> > 面向对象第三单元分析与总结

面向对象第三单元分析与总结

作者:互联网

面向对象第三单元分析与总结


前言

第三单元结束,面向对象课程马上就结束了,好耶!

本单元终点考察对JML规格理解与代码实现,需要了解基本的JML语法和语义,以及具备根据JML给出的规格编写Java代码的能力。在具体的作业中还兼具考察了部分图论的算法实现,练习了基于junit的程序测试方法,总的来说还是十分有趣的。

在撰写本篇博客之前,我回去认真读了我写的前两个单元的总结博客,结果看到一半直接绷不住。设想我如果是个萌新,看到这种车轱辘话来回说,除了我自己没人能看懂的博客,估计也挺崩溃的。

本次总结按照要求分为以下几个部分:

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

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

(3) 性能与优化——按照作业分析代码实现出现的性能问题和修复情况

(4) 扩展JML实践——对Network进行扩展,并给出相应的JML规格

(5) 心得体会——本单元学习体会。

力求简洁明了,不说废话好吧。

突然明白为什么会有博客这个环节了。


1. 单元测试

首先从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, RedEnvelopeMessageEmojiMessage全部继承原先的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.性能与优化

本单元最关键的优化点在于规避多层循环。其中主要有两方面:降低查询开销以及优化算法复杂度。

降低查询开销

优化算法

第九次作业中的isCircle要求我们找出关系图中两点是否连通,这里使用路径压缩的并查集实现。在实际使用时,与降低查询开销的道理一样,需要在添加数据时就更新结果,这样调用函数的时候就可以直接查询结果,避免无意义的重复计算,下面几次作业都同理。

第十次作业中的queryLeastConnection要计算最小生成树,但由于图本身不保证全连通,所以是求一个点所在的连通分量的最小生成树。我是直接用kruskal算法求直接求最小生成森林,再遍历这个森林的根节点找出给定点所在的最小生成树。

第十一次作业中的sendIndirectMessage函数需要计算最短路径,这个就是最短路径算法的直接实践。我这里用的是邻接表实现,对稀疏图效果很好。在某一次实验代码中给出了一个小根堆的实现,用来优化最短路径挺好的。java本身也有PriorityQueue这样的数据结构可以直接拿来用,逻辑是一样的。


4. 扩展JML实践

假设出现了几种不同的Person

如此Network可以支持市场营销,并能查询某种商品的销售额和销售路径等 请讨论如何对Network扩展,给出相关接口方法,并选择3个核心业务功能的接口方法撰写JML规格(借鉴所总结的JML规格模式)

Advertiser, Producer, Customer这三个可以继承原有的Person, 实现时就可以利用原有的MyPerson类,同时添加各自独有的方法。

添加两个Message的子类AdvertiseMessageShoppingMessage.

与上述生产产品对应,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来测试,但其工具链我觉得不太好用,经常会报一些莫名其妙的错误,当然重要的在于方法不是工具。

理论课上讲的契约式编程,还有研讨课上大佬分享的测试机制都让我受益匪浅。

本单元的正确率其实我不太满意,在难度下来之后也暴露出我一个问题,对于细节的把控不太好。比如在实现最短路径算法的时候将personid直接拿来当做index使用,结果不出意外数组溢出。当然我自己过于薄弱的测试也是主要原因。后续针对程序测试部分也要多作学习。

标签:总结,&&,int,测试,public,面向对象,JML,id,单元
来源: https://www.cnblogs.com/135qaz/p/16345825.html