2022 BUAA OO 第三单元总结
作者：互联网
一、测试数据的准备
课程组在第一次作业的时候推荐了JUnit测试。使用JUnit编写单元测试的好处在于，我们可以非常简单地组织测试代码，并随时运行它们，JUnit就会给出成功的测试和失败的测试，并且JUnit的测试是针对于每一个方法来进行的，理论上来说可以做到全面的检测。在尝试使用JUnit的时候，原本以为可以自动生成数据，最后发现测试数据都需要自己编写，因此简单尝试了一下这种方式就放弃了。
之后我选择了自动生成器准备测试数据并且与其他人对拍的方式来测试自己的程序，这个单元的自动数据生成写起来还是比较简单的，困难的点在于为了能更全面地测试自己的程序，生成的数据也不能过于随意。需要给代码添加一些限制，我的采用了一种方案为：有两种生成模式，一种模式是随意的生成数据，另一种模式是先addPerson，再addRelation，这种模式会保证不会出现那么多的异常，这两种生成模式以一定的比例交替生成数据。但测试中还有一个点没涉及到就是运行时间的问题，使用了python中的time这个函数获取运行jar之前和之后的时间，不知道正确不正确，课下跑的时候时间倒是没问题，但是在最后一次强测中还是TLE了一次。
二、架构设计
我认为这个单元利用了JML规格已经限制了很多，自己基本上没有太多的架构方面的设计。跟JML有一点不一样的点在于：JML描述的的数据存储都是数组存储，这种静态方式很不利于我们的程序，由于Person、Group、Message、Network都是有单独的id的，因此很自然的使用hashmap来存储数据。
由于JML只针对于某一个方法的实现功能，并不能利用整体的结构来进行优化，这一点需要我们自己来优化。我做了大概一下两个点优化：
-
对于Group中缓存一个valueSum，AgeSum等数据，这样在查询的时候直接获取数据而不需要再次计算。
-
对于Network中的一些查询方法，我实现了一个Blocks类，这个类其实是利用了并查集的方式来管理整个图，缓存了一些图的一些性质，利于查询。
三、性能问题和修复情况
每次作业都有一个需要注意性能的指令。
-
第一次作业isCircle，这个指令只需要查询两个点的连通性，通过Blocks中缓存的连通性性质可以很简单的查询。
-
第二次作业qlc，这个指令其实就是在求解最小生成树，使用为没任何优化的Prim算法就够用了，求解出来的数据也可以缓存在Blocks中，如果下次改变之前图没有变化便可以直接使用该数据。
-
第三次作业sim，这个指令是求解最短路径，使用了堆优化的Dijikstra。
第三次作业中的Dijikstra出现了两个问题。
-
一个是堆优化的实现，最开始我直接自己写了一个小顶堆，自己写的堆出现了一些问题导致出现了bug，解决方法：直接使用PriorityQueue来实现最小堆。
-
另一个是获取图的方式有问题，因为我每次都是从存储了所有人的hashmap里面找人，虽然hashmap查找很快，但是hashmap中contains以及containsKey这两个方法的实现其实是使用循环遍历查找的，这种方法时间复杂大直接O(n)，导致我获取图的时候的时间复杂度就已经高达O(n^2)。使用idea中的Windows Async Profiler来分析时间发现整个Dijikstra实现中的Dijikstra算法只占了很小一部分。结果就是有一个点CTLE了。结局方法：利用图的关系，直接从某一个person获取与他相连的其他person。
四、Network的JML扩展
/*@ public normal_behavior
@ assignable customers[].ads;
@ requires (\exists int i; 0 <= i && i < people.length;
@ people[i].getId() == id && people[i] instanceof Advertiser);
@ ensures (\forall int i; 0 <= i && i < customers.length;
@ (\forall int j; 0 <= j && j < ((Advertiser)getPerson(id)).ads.length);
@ customers[i].ads.contains((Advertiser)getPerson(id)).ads[j])))
@ ensures (\forall int i; 0 <= i && i < customers.length;
@ (\forall int j; 0 <= j && j < \old(customers[i].ads).length;
@ (\exits int k; 0 <= k; && k < customers[i].ads.length; \old(customers[i].ads[j]) == customers[i].ads[k])));
@ ensures (\forall int i; 0 <= i && i < customers.length;
@ customers[i].length = \old(customers[i].length) +
@ (\sum int j; 0 <= j && j < ((Advertiser)getPerson(id)).ads.length) &&
@ !(\exits int k; 0 <= k && k <= \old(customers[i].ads); \old(customers[i].ads[k]) == (Advertiser)getPerson(id)).ads[j]);
@ 1)
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id);
@*/
public void sendAds(int id);
/*@ public normal_behavior
@ requires (\exists int i; 0 <= i && i < people.length;
@ people[i].getId() == id && people[i] instanceof Producer);
@ assignable producers[].products, advertisers[].ads, products;
@ ensures getProducer(id).products.length == \old(getProducer(id).products.length) + 1;
@ ensures (\exists int i; 0 <= i && i < getProducer(id).products.length;
@ getProducer(id).products[i] == product);
@ ensures (\forall int i; 0 <= i && i < \old(getProducer(id).products.length);
@ (\exists int j; 0 <= j && j < getProducer(id).products.length;
@ getProducer(id).products[j] == (\old(getProducer(id).products[i])));
@ ensures (\forall int i; 0 <= i && i <= advertisers.length;
@ advertisers[i].ads.length == \old(advertisers[i].ads.length) + 1)
@ ensures (\forall int i; 0 <= i && i <= advertisers.length;
@ (\forall int j; 0 <= j && j <= \old(advertisers[i].ads.length);
@ (\exits int k; 0 <= k && k <= advertisers[i].ads.length; advertisers[i].ads[k] == \old(advertisers[i].ads[j]))));
@ ensures (\forall int i; 0 <= i && i <= advertisers.length;
@ (\exits int j; 0 <= j && j <= advertisers[i].ads.length; advertisers[i].ads[j] == product.id));
@ ensures products.length == \old(products.length) + 1;
@ ensures (\exists int i; 0 <= i && i < products.length; products[i] == product);
@ ensures (\forall int i; 0 <= i && i < \old(products.length);
@ (\exists int j; 0 <= j && j < products.length; products[j] == \old(products[i]))));
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id);
@ public exceptional_behavior
@ signals (EqualProductException e) (\exits int i; 0 <= i && i <= \old(getProducer(id).products.length);
@ \old(getProducer(id).products[i]]) == product);
@*/
public void addProduct(int id, Product product);
/*@ public normal_behavior
@ requires (\exists int i; 0 <= i && i < people.length;
@ people[i].getId() == id && people[i] instanceof Customer);
@ requires (\exists int i; 0 <= i && i < products.length; products[i].id == productId);
@ assignable customers[].products, products;
@ ensures getCustomer(id1).products.length == \old(getProducer(id).products.length) + 1;
@ ensures (\exists int i; 0 <= i && i < getCustomers(id1).products.length;
@ getCustomers(id1).products[i] == getProduct(productId));
@ ensures (\forall int i; 0 <= i && i < \old(getCustomers(id1).products.length);
@ (\exists int j; 0 <= j && j < getCustomers(id1).products.length;
@ getCustomers(id1).products[j] == (\old(getCustomers(id1).products[i])));
@ ensures products.length == \old(products.length) - 1;
@ ensures (\forall int i; 0 <= i && i < \old(products.length) && \old(products[i]).id != productId;
@ (\exists int j; 0 <= j && j < products.length; products[j] == \old(products[i]))));
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id);
@ public exceptional_behavior
@ signals (ProductIdNotFoundException e) !(\exits int i; 0 <= i && i <= \old(products.length); \old(products[i]).id == productId);
*/
public void bugProduct(int id, int productId);
五、心得总结
-
有JML之后写代码确实轻松了很多，但是JML也是真的很难写，虽然JML语言描述的很全面，但同时也带来了冗余。而且从网上我也并没有找到很多应用JML的例子，感觉这个技术还不是很成熟。
-
JML针对每个类的实现都有一个明确的描述，这种描述往往不考虑实现的复杂度，我们在实现的过程中难免要进行优化，这个时候就要慎重，仔细检查自己实现的行为和JML描述的是否相等。
-
不要以为用了HashMap之后干啥都是O(1)，对于contains和containsKey这种操作的复杂度还是O(n)。
-
尽可能地使用高级工具，比如最小堆的实现，有优先队列就直接用，自己写的大概率没有库函数好用。不过自己学习算法实现的时候倒是应该自己写写底层代码。
标签：OO,ensures,int,BUAA,length,products,2022,forall,id 来源： https://www.cnblogs.com/pc-hao/p/16347948.html