其他分享
首页 > 其他分享> > 2022-OO-Unit3

2022-OO-Unit3

作者：互联网

2022-Unit3

一、利用JML准备测试数据

边界数据

边界数据的构造主要由JML规格而来，比如group.size() > 1111人的数据、将3块钱红包发给5个人的数据……构造这种边界数据需要在阅读JML规格时及其细心。

压力数据

压力数据的构造比边界数据简单一些。最简单的压力数据就是N条重复指令。比如500条qlc、500条qbs、500条sim等等，简单粗暴，测试算法复杂度。

其次也可以在网络结构上做一些文章，比如可以构造一条社交链，1 link 2， 2 link 3，3 link 4……搞出上千人的社交链，用来测试各种图论算法。其实就是一些特殊的图罢了。

二、架构分析

架构设计

本单元由于JML规格的限制以及作业要求，个人感觉大部分架构都大同小异，人手必备MyMessage、MyNetwork、MyPerson、MyMessage、以及各种各样的Exception。

但是在架构方面仍然可以做出一定的优化设计，否则MyNetwork类超过500行就会被扣代码风格分了。。。

我个人的架构是建立算法包和数据结构包，单独封装所需要的结构与算法，这样，在MyNetwork中的sendIndirectMessage、queryLeastConnection、queryBlockSum等方法中直接调用相应类的方法即可，大量减少代码。

image

如图，我分别建立了algorithm和datastructure两个包，前者内置Dijkstra算法类与Kruskal算法类；后者内置边、节点、并查集结构类。需要时调用即可，这样可以大大减轻MyNetwork类中的代码量。

图模型建构与维护策略

并查集

在第一次作业中，我和大多数人一样，不约而同使用了并查集。在并查集的实现方面，网上许多博客都是利用数组实现的。但我认为用数组实现太不java了，并且在调试时可能也不太好调试。

于是我利用树结构建立了并查集，新建Node类和UnionFind类。其实每个Node类就是上文中的数组元素。这样便建立起了树形结构，在路径压缩时只需要将被压缩节点指向根节点即可。

图模型建构

在第二次作业中，我们需要求出最小生成树，这必然就需要存储图的结构，我选择用ArrayList<Edge>储存边。

在addRelation方法中，如果对两人添加了关系，我便将（id1, id2, value）作为一个边存储起来，以备之后用到。因为没有delRelation方法，所以边集只增不减。

在queryLeastConnection方法中，传入参数personId，我先由已经维护好的并查集结构找出与该person在同一连通分量的所有人，得到personIds，用ArrayList<Integer>存储。之后遍历已经维护好的edges，将该连通分量中的边全部提取出来。之后将personIds与edges全部传入Kruskal类，得到最小生成树的权值和。

在第三次作业中，我们需要求出最短路径，又是一个以图结构为基础的经典算法。这里我选择了堆优化版的Dijkstra算法（感觉绝大部分人都是这么写的）。

这里其实不需要专门做模型维护，因为每个Person对象的acquaintance和value就是天然的邻接表！只需要使用PriorityQueue类建立一个小根堆就好了。之后便一步一步按照算法来写就完全ok了。

三、性能问题及修复情况

第一次作业

第一次作业中互测被hack烂了，其原因是没有对并查集进行路径压缩。在bug修复环节，我在UnionFind类中增加了路径压缩的实现，即当将A节点的父指针指向find(A)。

第二次作业

第二次作业中的性能问题在于均值和方差的计算。我原始的方法和JML规格中的流程一模一样，直接进行暴力遍历，导致在互测中又一次被hack烂。

之后我采用了动态维护的方法，在Group类中，设置属性ageSum和agePowSum， 在addPerson时 ageSum += person.getAge()，agePowSum += person.getAge() * person.getAge()；在delPerson时，ageSum -= person.getAge()，agePowSum -= person.getAge() * person.getAge()。

这样在求均值时直接返回ageSum / people.size()即可，求方差时直接返回 (agePowSum - 2 * mean * ageSum + people.size() * mean * mean) / people.size()即可。

第三次作业

第三次作业中没有出现性能问题。

四、Network扩展及JML

架构

Advertiser、Producer、Customer继承Person类，广告消息AdvertiseMessage、PurchaseMessage继承Message类。

新增类Product，即商品类， 内置id、price等属性。

Advertiser类中属性：producers, advertisements

Producer类中属性：products，advertisers

Customer类新增属性：preference

PurchaseMessage类新增属性：advertiserId, ProducerId

NetWork类新增方法：addProduct(Product product)、sendAdvertiseMessage(int messageId)、sendPurchaseMessage(int messageId)、querySalesVolume(int productId)、querySalesPath(int ProductId)等方法。

JML

addProduct方法

/*@ public normal_behavior
  @ requires !(\exists int i; 0 <= i && i < products.length;products[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;
  @          products[i].equals(product));
  @*/
  public void addProduct(/*@ non_null @*/Product Product) throws EqualProductIdException;

sendPurchaseMessage方法

/*@ public normal_behavior
  @ requires containsMessage(id) && getMessage(id).getType() == 0 &&
  @ isCircle(getMessage(id).getPerson1().getId(), getMessage(id).getPerson2().getId()) &&
             \old(getMessage(id)) instanceof PurchaseMessage;
  @ assignable messages
  @ assignable getMessage(id).getPerson1().socialValue, getMessage(id).getPerson1().products;
  @ assignable getMessage(id).getPerson2().socialValue, getMessage(id).getPerson2().products;
  @ 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 \old(getMessage(id)).getPerson1().getSocialValue() ==
  @         \old(getMessage(id).getPerson1().getSocialValue()) + \old(getMessage(id)).getSocialValue() &&
  @         \old(getMessage(id)).getPerson2().getSocialValue() ==
  @         \old(getMessage(id).getPerson2().getSocialValue()) + \old(getMessage(id)).getSocialValue();
  @ ensures (\forall int i; 0 <= i && i < \old(getMessage(id)).getPerson2().products.length && 
  @           \old(getMessage(id)).getPerson2().products[id] != \old(getMessage(id)).getProductId();
  @         (\exists int j; 0 <= j && j < \old(getMessage(id)).getPerson2().products.length;
  @           \old(getMessage(id)).getPerson2().products[j].id == \old(getMessage(id)).getPerson2().products[i].id);
  @ ensures (\exists int i; 0 <= i && i < \old(getMessage(id)).getPerson2().products.length; 
  @          \old(getMessage(id)).getPerson2().products[i].id == \old(getMessage(id)).getProductId());
  @ ensures \old(getMessage(id)).getPerson2().products.length = \old(getMessage(id)).getPerson2().products + 1;
  @ 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)));
  @ ensures \old(getMessage(id)).getPerson2().getMessages().get(0).equals(\old(getMessage(id)));
  @ ensures \old(getMessage(id)).getPerson2().getMessages().size() == \old(getMessage(id).getPerson2().getMessages().size()) + 1;
  @ also
  @ public exceptional_behavior
  @ signals (MessageIdNotFoundException e) !containsMessage(id) ||
  @         containsMessage(id) && getMessage(id).getType() == 1;
  @*/
public void sendPurchaseMessage(int messageId) throws
            MessageIdNotFoundException;

querySalesVolume方法

  /*@ public normal_behavior
	@ requires containsProductId(productId);
	@ ensures \result == getProduct(productid).getSalesAmount();
	@ also
	@ public exceptional_behavior
	@ signals (ProductIdNotFoundException e) !containsProduct(productId);
	@*/
	public int querySalesVolume(int productId) throws
		ProductIdNotFoundException;

五、学习体会

本单元最大的收获是对JML规格的了解与学习，甚至应用。JML规格的的存在，使得开发人员在写代码时可以“有法可依”，但同时要保证正确理解它，这样我们的程序在正确性上便会得到保证。

此外，这一单元的作业与数据结构中的许多知识挂钩，第一次作业中的并查集、第二次作业中的Kruskal算法、第三次作业中的Dijkstra算法。三次作业均需要我们实现计算机领域中的经典算法，有助于夯实我们的算法基础。

由于我最初直接暴力循环，导致有很多数据超时。在改进算法后不禁感叹“真香！”。真切感受到算法的魅力与力量，对提出这些算法的前辈们致敬。

标签：OO,JML,查集,作业,算法,getMessage,2022,Unit3,id
来源： https://www.cnblogs.com/yjzhao-buaa/p/16340289.html