标签：OO int BUAA Person 规格 getMessage JML id 单元
BUAA OO 第三单元总结
JML规格和测试
本单元的主题是根据JML规格编写代码，架构设计方面只需要严格地按照JML规格即可。相应地，在测试方面也可以根据JML规格进行相对应的测试。课程组的建议是使用JUnit，但是在简单尝试后觉得时间成本比较高，加上舍友完成了对拍机，遂选择和舍友对拍进行主要测试，自测只针对边缘数据和效率问题进行测试。在自测的过程中，相比前两个单元的作业，有了JML规格，所有的情况其实都穷举了出来，所以在构造数据时可以参考的准则有：
-
对于高复杂度的方法进行单元测试
由JML规格的长度和循环的次数可以初步判断一个方法的复杂与否，在完成一些高复杂度的方法时，例如第二次作业中的
queryLeastConnection方法，第三次作业中的sendIndirectMessage方法等，可以相对应地构造一些简单（指令单一）的数据进行测试，以初步确保正确性和效率问题，更进一步的测试需要更大的数据量实现。 -
构造数据以满足JML规格中不同的前置条件
JML规格给出了不同的前置条件下正确的行为，自然地，根据JML规格构造出数据以满足不同的前置条件是测试一个方法的合理思路。例如第三次作业中的
sendMessage方法，可以构造数据：- 一部分数据满足异常行为的前置条件，如构造包含相同
id的message的数据，构造relationNotFound的数据等； - 一部分数据分别满足不同正常行为的前置条件，如一些为
RedEnvelogeMessage，一些为EmojiMessage，一些为1类型的Message，一些为2类型的Message等等。
由于JML规格详细地穷举了所有的可能，因此这样构造出的数据能够进一步提高数据的覆盖率，在JML规格的指导下，构造数据的难度并不大。
- 一部分数据满足异常行为的前置条件，如构造包含相同
图模型构建和维护策略
本单元的主题是实现一个简单的社交网络，在基本的图模型基础上，主要涉及到的图论知识有：连通分支的查询（两点是否连通以及连通分支数），最小生成树的查询，最短路的查询。这些方法的JML规格都比较复杂，如果严格按照JML规格实现存在效率问题，应当合理优化以确保方法复杂度都在\(O(n^2)\)以下。具体实现过程中主要是用了以下几个方法或者技巧，在下面的具体实现过程中会加以体现：
-
使用最优算法
必要性不言而喻，具体的实现可以参照网络上的教程，毕竟OO主要考察的还是设计。
-
合理使用容器
由于
HashSet（以及HashMap对key）的查询复杂度都是\(O(n)\)，肯定比ArrayList要来得快，因此尽可能使用HashSet以及HashMap能一定程度上提高效率。 -
维护查询变量
构造一个变量，将方法复杂度平摊到每次改变其中参数的维护过程中。
-
使用缓存机制
参考TLB机制，对于通过复杂的方法得出的结果可以缓存，并标记（已查询且无需修改），下次查询时便可以直接获取。
第一次作业
第一次作业开始需要对图的信息进行读入和存储，使用的容器基本为HashSet以及HashMap。例如：
private HashMap<Integer, Person> people;
private HashMap<Integer, Group> groups;
//其中，Key为元素的id，value为元素
从而查询方法的复杂度就是\(O(1)\)。
第一次作业中可能存在效率问题的是查询连通分支数量的指令qbs，以及指令qgav。两条指令如果严格根据JML规格写的话复杂度为\(O(n^2)\)，在互测部分可能会损失一定的分数。因此需要进行相应的优化
qbs指令
一个合理地解决方案是使用并查集，并维护一个blockSum变量，这里我使用的是按秩合并以及路径压缩版本的并查集。由于只有这一条指令需要用到，所以没有考虑那么多，直接将并查集内嵌在了MyNetwork内，使得整体的结构并没有那么明晰，在第二次作业中改进为了新建一个DisjoinSet类。
qgav指令
通过维护\(\sum{age^2}\)和\(\sum{age}\)，再利用getAgeMean()，即可优化为\(O(1)\)复杂度。
第二次作业
第二次作业主要需要优化的方法是最小生成树查询方法（对应指令qlc）。我采取的策略是将并查集DisjoinSet单独建为类，同时新建Block类，使用基于并查集的kruskal算法，同时将最小生成树的值进行缓存。
具体来说，我在使用并查集的同时维护了网络中所有的连通块，也就是Block，其属性为：
private HashSet<Person> items = new HashSet<>();//连通块中的所有人
private Person father;//并查集中的头部变量，该连通块中所有人的father为同一个元素
private int leastValue;//查询最小生成树的结果
private int sign;//是否可以直接获取leastValue的标志
而在实际的查询过程中，首先取得Person对应的Block，如果sign为0，则直接获取结果，否则运用kruskal算法更新leastValue的值，再将sign置为0，并返回。在更新的过程中需要对边进行遍历，所以方法的复杂度为\(O(n)\)。
值得说明的一点是：并不是所有修改了Block的情况下都需要修改sign，当两个连通块由于一条边的添加而合并为一条连通块时，如果两个连通块的leastValue均可以直接获取，则合并连通块的leastValule可以直接用两个连通块的leastValue相加，再加上该边的值即可。这个可以稍稍提高一点效率。
第三次作业
第三次作业主要需要优化的方法是最短路的查询（对应指令sim）。我采用的策略是使用堆优化的dijkstra方法，具体的实现参照了网络上的教程，主要是用的容器是HashMap和HashSet。实现过程中出了一个难以溯源的BUG，将在后续的性能问题及其修复部分讨论。
性能问题及其修复
得益于舍友高覆盖率的数据生成器，本单元的作业中测，强测，互测均未被发现BUG。但是在实现过程中，以及hack过程中发现的BUG依然值得探讨。
实现过程中的BUG
实现过程中的BUG主要集中在第三次作业中。
一个BUG是因为对JML理解产生偏差，认为一个EmojiId对应的MessageId是唯一的，从而造成BUG，这里就不细说了。另一个BUG就是堆优化的dijkstra实现过程中由于对堆理解不够深刻导致的BUG。
具体而言，我有问题的版本的实现如下：
private int dijkstra(Person person1, Person person2) {
HashMap<Person, Integer> distance = new HashMap<>();
HashSet<Person> visited = new HashSet<>();
Comparator<Person> disComparator = Comparator.comparingInt(distance::get);
PriorityQueue<Person> personPriorityQueue = new PriorityQueue<>(disComparator);
distance.put(person1, 0);
personPriorityQueue.add(person1);
while (!personPriorityQueue.isEmpty()) {
Person person = personPriorityQueue.poll();
if (visited.contains(person)) {
continue;
}
visited.add(person);
for (Person p : ((MyPerson) person).getAcquaintanceValueMap().keySet()) {
if (!visited.contains(p) && (!distance.containsKey(p) ||
distance.get(p) > distance.get(person) + person.queryValue(p))) {
distance.put(p, distance.get(person) + person.queryValue(p));
personPriorityQueue.add(p);
}
}
}
return distance.get(person2);
}
同一个Person会被反复添加到优先队列中，同时该Person在优先队列中的所有“副本”对应的距离都为同一个值（因为对距离的获取是基于一个HashMap(Person, int)实现的），这就会导致在Person被加入时，之前已加入优先队列中的Person的“副本”的距离都会被改变但是该优先队列只会调整一次，这就会导致小根堆的结构崩溃。具体可以参考以下的样例：
解决方案就是新建一个Node类，属性为Person以及Distance，每次插入的都是新的节点，从而不会改变已在堆中的节点的值，堆的结构也就因此能够得以维持。
Hack过程中发现的BUG
本单元总共成功hack他人7次，都是CTLE的问题，使用的策略都是构造单一种类复杂指令的数据，例如qbs指令，qgvs指令等。修复的策略就是进行优化，具体可以参照本文图模型构建和维护策略 部分的内容。
对Network的扩展
要求
假设出现了几种不同的Person
- Advertiser：持续向外发送产品广告
- Producer：产品生产商，通过Advertiser来销售产品
- Customer：消费者，会关注广告并选择和自己偏好匹配的产品来购买 -- 所谓购买，就是直接通过Advertiser给相应Producer发一个购买消息
- Person：吃瓜群众，不发广告，不买东西，不卖东西
如此Network可以支持市场营销，并能查询某种商品的销售额和销售路径等，请讨论如何对Network扩展，给出相关接口方法，并选择3个核心业务功能的接口方法撰写JML规格。
接口与方法设计
首先，将Advertiser，Producer，Customer设计为Person子接口，新增BuyingMessage，AdertisementMessage为Message的子接口，新增Product类。
接口和类中新增方法定义如下：
Advertiser:
List<> getProducers()//返回合作的生产商
List<> getProducts()//返回推销的产品
Producer:
Product getProduct()//产品
Product:
int getId()//产品ID
int getPrice()//产品价格（顾客）
int getProfit()//产品利润（生产商）
int getSales()//销售额
Customer:
List<> getAdvertisements()//返回收到的广告信息
List<> getPreferProducts()//返回希望入手的产品
AdvertisementMessage:
Advertiser getAdvertiser()
Customer getCustomer()
Product getProduct()
BuyingMessage:
//两个构造方法，分别对应顾客购买请求信息和广告商的转述信息
BuyingMessage(Customer,Advertiser)
BuyingMessage(Advertiser,Producer)
int getBuyingType()//返回购买消息类型
Product getProduct()//产品
int getNumber()//购买额
Mynetwork:
Advertiser getAdvertiser(int id)
Customer getCustomer(int id)
Producer getProducer(int id)
Product getProduct(int id)
//相应的还应该由containsXXX()方法
void sendBuyingMessage(int messageid)//顾客向广告商发出购买请求或者广告商向生产商转述购买请求。
boolean ableToBuy(int customerId,int productId)//检查顾客是否能够购买产品，当且仅当顾客通过广告商向对应的生产商发送了购买请求时返回True。
boolean buyProduct(int customerId,int productId,int number)//顾客购买产品，如果顾客ID不存在，抛出异常，如果产品ID不存在，抛出异常,如果对应Product不在顾客偏好产品中，抛出异常。
void sendAdvertisement(int messageId)//投递广告
void addPreferProduct(int customerId,int productId)//添加偏好产品
int queryProductSales(int productId)//查询产品销售额
List<> queryProductSalePath(int productId)//查询销售路径
JML规格撰写
-
buyProduct(int customerId,int productId,int number)/*@ public normal_behavior @ requires (containsCustomer(id1) && containsProduct(id2) && number > 0 && ableToBuy(id1, id2)); @ assignable getCustomer(id1).money,getProduct(id2).sales; @ ensures getProduct(id2).getSales() == \old(getProduct(id2).getSales()) + getProduct(id2).getPrice() * num; @ ensures getCustomer(id1).getMoney() == \old(getCustomer(id1).getMoney()) - getProduct(id1).getPrice() * num; @ ensures \result == true; @ also @ public normal_behavior @ requires (containsCustomer(id1) && containsProduct(id2) && num <= 0 && ableToBuy(id1, id2)); @ assignable \nothing; @ ensures \result == false; @ also @ public exceptional_behavior @ signals (CustomerIdNotFoundException e) !containsCustomer(id1)); @ signals (ProductIdNotFoundException e) (containsCustomer(id1) && !containsProduct(id2)); @ signals (NotAbleToBuyException e) (containsCustomer(id1) && !containsProduct(id2) && !ableToBuy(id1, id2)); @*/ public boolean buyProduct(int id1, int id2, int number) throws CustomerIdNotFoundException, ProductIdNotFoundException，NotAbleToBuyException; -
sendAdvertisement(int id)/*@ public nomal_behavior @ requires containsMessage(id) && (getMessage(id) instance of BuyingMessage) && ((BuyingMessage(getMessage(id))).getBuyingType() == 0) @ && getMessage(id).getType() == 0 && @ getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) && @ getMessage(id).getPerson1() != getMessage(id).getPerson2(); @ assignable messages; @ assignable getMessage(id).getPerson1().socialValue, getMessage(id).getPerson2().socialValue; @ assignable getMessage(id).getPerson2().messages; @ assignable getMessage(id).getPerson1().money; @ assignable ((Customer)getMessage(id).getPerson2()).getAdvertisements(); ((Customer)\old(getMessage(id)).getPerson2()).getAdvertisements() @ 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().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; @ ensures (\forall int i; 0 <= i && i < ((Customer)\old(getMessage(id)).getPerson2()).getAdvertisements().size()); @ ((Customer)\old(getMessage(id)).getPerson2()).getAdvertisements().get(i+1) == ((Customer)\old(getMessage(id)).getPerson2()).getAdvertisements().get(i))); @ ensures ((Customer)\old(getMessage(id)).getPerson2()).getAdvertisements().get(0).equals(\old(getMessage(id))); @ ensures ((Customer)\old(getMessage(id)).getPerson2()).getAdvertisements().size() == \old(((Customer)\old(getMessage(id)).getPerson2()).getAdvertisements().size()) + 1; @ also @ public exceptional_behavior @ signals (MessageIdNotFoundException e) !containsMessage(id); @ signals (NotBuyingMessageException e) containsMessage(id) && !(getMessage(id) instance of BuyingMessage); @ signals (RelationNotFoundException e) containsMessage(id) && (getMessage(id) instance of BuyingMessage) && !getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2())); @ signals (PersonIdNotFoundException e) containsMessage(id) && (getMessage(id) instance of BuyingMessage) && !getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1())); @*/ public void sendAdvertisement(int id) throws NotAdvertiseMessageException, MessageIdNotFoundException, RelationNotFoundException, PersonIdNotFoundException; -
int queryProductSales(int productId)/*@ public normal_behavior @ requires containsProduct(id); @ assignable \nothing; @ ensures \result == getProduct(id).sales; @ also @ public exceptional_behavior @ signals (ProductNotFoundException e) !containsProduct(id)); @*/ public int queryProductSales(int id) throws ProductIdNotFoundException;
学习体会和收获
- 本单元是第一次接触JML语言，感觉到在由JML规格的指导下，需求十分明确，代码的书写比较简单，降低了产生BUG的可能。同时JML规格还有助于测试数据的构造，方便了测试。另一方面，在尝试书写JML的时候，也感觉到需要全面地考虑各种情况的困难所在，严格的语法要求使得JML规格动辄长达数十行。所以如果需要自己书写JML规格并完成代码撰写的话难度并不亚于直接书写代码。（
也就是说本单元感觉到难度下降只不过是有助教们在负重前行） - 本单元主要考察的是图模型的搭建和维护，由于需要对效率问题进行考虑，采取了各种优化的方法或者技巧。本单元的学习让我对网络的模型理解更加深刻，也掌握了一些常用的优化技巧，对一些数据结构算法也更加熟悉，总的来说收获很大。
标签：OO,int,BUAA,Person,规格,getMessage,JML,id,单元 来源： https://www.cnblogs.com/Longxmas/p/16341933.html
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。