OO第三单元总结

数据构造

​ 基于JML规格构造数据本质上就是检查方法能否满足功能与异常情况，

异常检验

​ 异常一般看的是前置条件，分为抛出型异常以及隐性异常。

​ 比较常见的是抛出型异常，对于该种异常的检验，我们应针对触发异常的条件专门去构造数据，从而检查程序能否正确抛出相应异常，做到不重不漏，同时要注意不同异常触发条件间的包含关系。

​ 除此之外，隐形异常在触发后不会抛出，但会阻止原有代码，并使方法正常结束，例如在addToGroup中当Group中的people人数大于等于1111后，遍会组织新的People再加入，对此我们亦要构造相应数据，检验是否能正确处理相应异常。

功能性检验

​ 功能检验主要看的是后置条件，大致有三个方面：保持原状的成员、新加入的成员、计算所得的结果。一般来说保持原状的成员这一点如果不整什么骚操作不会导致错误，所以重点检查后两者是否正确。

​ 功能性的检验一般是在不触发异常的情况下，尽可能构造多种的情况，以检验实现过程的正确性。例如在派发Message时要检验各类Message是否正确被发送，这需要多个指令相互协作来检验；另外，对于每次作业的图论题，则是要多构造一些图，来检验图论算法的正确性。

​ 值得注意的是，由于数据量的限定，算法的时间复杂度也是一个需要注意检查的点，十分容易没想清楚最终导致超时，这在后续会再详细分析。

架构设计

任务与迭代

​ 本次作业的架构整体上都由JML给出，要求实现一个基础的社交网络，拥有主体Person、Group，主体间交互的Message，以及实现环境模拟的Network对象。除此之外，在每次作业中，都有一个图论算法需要我们去学习实现。

第九次作业

​ 第三单元的第一次作业比较基础，旨在让我们熟悉JML语言，要求实现社交网络中的人员与团体的添加、人员关联以及相关值的查询功能。

​ 其中的qci检查两人是否能通过社交链关联的指令，涉及到并查集，为了避免超时，我采用了路径压缩的优化方法，即在查询过程中，主动得将并查集的子节点连接到根节点上，如此可使每次得根节点查询优化到O(1)，极大节约了时间。

第十次作业

​ 引入了社交网络中的Message概念，需要实现Message的添加及发送，涉及到Person间的相关值变动。

​ 图论算法考察的是最小生成树，在理解JML规格要求和，不难简化出要求为求出最小生成树的边权和，我选择了prim算法，但由于实现的错误最后导致了超时，在后面的性能分析中会再次提到。

第十一次作业

​ 最后一次作业主要是丰富了Message的种类（通过继承实现），分为原来的普通，表情，红包以及emoji共四种，需要我们分辨Message的种类，并实现相应的具体功能，如此使得设计网络更丰富更贴切实际。

​ 图论考察了最短路算法，通过给出某个Person，经过ar关联关系找到另一个Person，最终返回该路径的总值。我采用了经典的迪杰斯特拉算法，并加以堆优化以提升效率，java中可以直接使用priority_queue，其帮我们完成了最小堆的构建，十分方便。

数据维护

​ 在数据维护的过程中，由于各对象具有共同特点——具有唯一id，因此在存储的时候我基本采用了HashMap来进行存储，以id为Key具体对象为Value，通过使用containsKey等方法，使得对象的检索获取等步骤极大简化，且由于哈希的特性，使得我们无须在此类操作上顾虑时间消耗。但值得注意的是，HashMap中存储为乱序，不具有List的顺序特性，需要留意JML规格是否需要该容器满足List的特性，选用正确的容器。

性能问题及修复

​ 在这个单元的作业中，性能问题是十分关键的一个点，在经过了大量随机数据的对拍检验后，在不考虑性能问题的前提下，程序的正确性基本能够得到保证。因此，由于性能问题一般是由于思维漏洞亦或是不严谨导致，往往容易被忽略，这也成为了导致强测出错以及互测hack的一个关键点。

​ 就我个人而言，本次出现的问题主要出现在query_group_value_sum和query_least_connection两个指令上。

​ qgvs需要统计Group中所有Person的Value之和，我在原来实现的是每一次查询都遍历一遍所有Person重新算一遍该值，导致我每次查询的时间复杂度都到达了O(n)，当有大量的qgvs查询时，遍很容易导致超时。对此我们需要了解到动态维护的思想，对于上述情况我们可以修改为，在每次addPerson、delPerson以及ar建立关系（即所有可能进行可能会影响到ValueSum的操作）时，动态地根据当前操作对ValueSum进行维护，这样就可以使得每一次的qgvs查询只需要O(1)的时间复杂度，极大得提升了程序的性能。

​ qlc则是一个最小生成树算法的实现，这里出现的性能问题则是我对算法的理解与实现产生了偏差。我采用了Prim算法，从某一点出发，每次找寻一条权值最小且未曾与出发点关联的边，不断进行拓展直至关联所有点。在我错误的实现中，并没有采用普遍的类似于迪杰斯特拉算法的形式，而是将所有新拓展的边加入边集中，每次找边都花费了大量时间去过滤掉那些已经处于出发点集合内的边，最终导致了超时。正确的实现方式应该是在每次拓展后，根据新拓展的边去更新到达每个点的最小边，这般便可以将每次拓展找边的时间复杂度从O(m)降低到O(n)，就不会导致超时了。可见算法的实现方式，是保证实现预期效果的重要一环。

拓展设计

根据要求，我们对Person进行继承拓展，新增一下三种Person

• Advertiser：持续向外发送产品广告
• Producer：产品生产商，通过Advertiser来销售产品
• Customer：消费者，会关注广告并选择和自己偏好匹配的产品来购买 -- 所谓购买，就是直接通过Advertiser给相应Producer发一个购买消息

除此之外，为了直线上述Person间的交互，还需新增相应的Message种类

• AdvertiseMessge：Advertiser告知Customer，向其发送产品广告
• PurchaseMessage：Advertiser给相应Producer发送购买信息，帮助Customer购买产品

核心业务功能接口方法的JML规格

• 委托销售，即将对应产品委托Advertiser推销，id1为产品id，id2为PersonId

/*@ public normal_behavior
@ requires (\exists int i; 0 <= i && i < persons.length; persons[i].getId() == id2)&&
@         (\exists int i; 0 <= i && i < products.length; products[i].getId() == id1) &&
@ assignable getPerson(id2);
@ ensures (\forall Procut i; \old(getPerson(id2).hasProduct(i));
@          getPerson(id2).hasProduct(i));
@ ensures getPerson(id2).hasProduct(getPerson(id1));
@ also
@ public exceptional_behavior
@ signals(PersonIdNotFoundException e)!(\exists int i; 0 <= i && i <persons.length;
@          persons[i].getId() == id2);
@ signals(ProductIdNotFoundException e)(\exists int i; 0 <= i && i <persons.length;
@       persons[i].getId() == id2)&&!(\exists int i; 0 <= i && i < products.length;
@           product[i].getId() == id1);
@ signals (EqualProductIdException e) (\exists int i;0 <= i && i < personss.length;
@        groups[i].getId() == id2) && (\exists int i; 0 <= i && i <product.length;
@           people[i].getId() == id1) && getPerson(id2).hasProduct(getPerson(id1));
@*/
	public void promoteProduct(int id1, int id2, int id3) throws PersonIdNotFoundException, ProductIdNotFoundException, EqualProductIdException;

• 发送广告
  • id1为广告商id，id2为顾客id，id3为产品id

/*@ public normal_behavior 
@ requires containsAdvertiser(id1) && containsCustomer(id1) && containsProduct(id3)
@ assignable messages;
@ ensures (\exist AdvertiserMessage i; i.getTyper() == 0 && 
@ i.getPerson1().getId() == id1 && i.getPerson2().getId() == id2 && 
@ i.getProduct().getId() == id3) && 
@ containsMessage(i.getId()) && 
@ (\all AdvertiserMessage i; (\old)contains(i.getId()) ==> contains(i.getId))
@ public exceptional_behavior
@ sinals (AdvertiserIdNotFound e) !containsAdvertiser(id1)
@ sinals (CustomerIdNotFound e) !containsCustomer(id1)
@ sinals (ProductIdNotFound e) !containsProduct(id3)
@*/
public void addAdvertisement(int id1, int id2, int id3) throws AdvertiserIdNotFound, CustomerIdNotFound, ProductIdNotFound;

• 购买产品：顾客给钱（允许欠钱），同时添加广告商发送给厂家的购买信息
  • id1为顾客id，id2为产品id，id3为广告商id

/*@ public normal_behavior
@ requires containsPerson(id1) && ContainsProduct(id2) && containsAdvertiser(id3)
@ assignable messages getPerson(id1).money
@ ensures (\old(getPerson(id1).money) == getPerson(id1).money + getProduct(id2).value) &&
@ ensures (\exist PurchaseMessage i; i.getPerson1() == getAdvertiser(id3) && i.getPerson2() == getProduct(id2).getProduce; containsMessage(i.getId()))
@ also
@ public exceptional_behavior
@ sinals (PersonIdNotFound e) !containsPerson(id1)
@ sinals (ProductIdNotFound e) !containsProduct(id2)
@ sinals (AdvertiserIdNotFound e) !contasinAdvertiser(id3)
@*/
	public void purchase(int id1, int id2) throws PersonIdNotFound, ProductIdNotFound, AdvertiserIdNotFound;

学习心得

​ 通过本单元的学习，了解了JML规格描述基础知识，并锻炼了将JML从阅读理解到实现的能力。在以前我写代码都有些“随心所欲”，认为只要实现功能就可以，不注重代码的规范性。但在本单元的学习与训练中，我逐渐领会到了规范性的优点与必要性。对于JML规格描述乃至其他的规范描述，我认为有几处优点：一是其最基础的作用，通过规范的描述，使得程序员在实现程序的过程中保证正确的理解，避免常规描述产生的理解二异性；二是任务明晰，降低了思考的难度，也减少了出错的可能。通过这个单元的锻炼，我写代码的风格更加规范明晰，注重架构设计，同时还努力去避免繁杂的冗余代码，深刻体会到了规范之于代码的重要性。

​ 除此之外，在这个单元，我有了更多的对拍经历，自己去尝试写一个简易的评测机，实现数据的生成与构造，也收获到许多。总体来说，这个单元的所学所写，都十分得有意义，对于我今后的代码生涯起到了很大的指导和启发作用，再次感谢老师和助教们精选的教学设计，令我受益匪浅。

标签：OO,总结,id2,id3,id1,Person,&&,id,单元
来源： https://www.cnblogs.com/kingimtk/p/16348480.html