BUAA OO 第三单元总结

利用JML规格准备测试数据

在课上老师推荐我们用Junit单元测试，但Junit是白盒测试，需要自己手动针对每个方法判断前提和结果约束，非常的复杂，所以最后我还是决定通过黑盒测试。

JML的规格有前置条件和后置条件，只要保证生成的数据能满足所有使用到的方法的前置条件即可，而本单元对数据限制的前置条件几乎没有，所以自动生成的数据只需要满足数据本身的结构与要求就可以。

在随机构造数据时，如果采用全随机的方式，那数据强度将会是极低的，会由于id之类的数据没有对应上而抛出异常。所以我在构造数据的时候采取了模块构造的方法，通过一个个对应的指令块来实现指令参数的对应。在一定程度上保证了数据的强度。

架构设计

本单元作业并不需要我们自己在整体上对程序的架构进行整体上的设计。

只需要我们按照接口的JML实现算法即可，所以在架构上没有什么挑战。

维护策略

因为对象和id存在一一对应的关系，而指令也要通过id查取对象，所以我使用了HashMap作为容器维护数据，以实现O(1)的查找复杂度。

同时为了降低算法的时间复杂度，对于某些属性我采取了动态维护的方式，这样可以减少一个循环遍历，而具体实现在下面的性能优化处提及。

性能优化

性能优化主要在三个方面有体现：

第一次作业中：

通过并查集算法实现了指令isCircle和qbs，并加入了非递归的路径压缩进行优化，使得算法时间复杂度大大降低。

第二次作业中：

实现了kruskal算法来生成最小生成树，并通过并查集对其进行了优化，降低了时间复杂度。

另一方面，对于指令qgvs。我通过动态维护一个属性valueSum，在每次ar，atg，dfg操作中实时更新valueSum值，使得原本O(n^2)的时间复杂度降为了O(n)。

第三次作业中：

实现了Dijkstra算法来找出最短路，并通过优先队列进行了堆优化，使得时间复杂度从O(n^2)降为了O(n*log(n))。

修复情况

本单元因为我合理的性能优化和大量的测试，公测和互测中都没有被测出BUG，不需要修复。

Network扩展

首先Advertiser、Producer以及Customer三个类都应该实现Person接口，并实现一些加入属性的方法和与具体行为相关的方法。

其次我们可以新增一个Produce类来封装商品的各种属性和相关的操作。

我选择实现发布广告、查询商品是否有库存、制造产品三个核心业务的接口方法，JML规格如下：

/*@ public normal_behavior
  @ requires product != null;
  @ assignable customers;
  @ ensures (\forall int i; 0 <= i && i < customers.length; customers[i].contains(product));
  @ ensures (\forall int i; 0 <= i && i < customers.length;
            !\old(customers[i].contains(product)) ==> 
            customers[i].product.length == \old(customers[i].product.length) + 1);
  @ ensures (\forall int i; 0 <= i && i < customers.length;
            \old(customers[i].contains(product)) ==> 
            customers[i].product.length == \old(customers[i].product.length));
  @ ensures (\forall int i; 0 <= i && i < customers.length;
            (\forall int j; 0 <= j && j < \old(customers[i].products.length); 
            (\exists int z; 0 <= k && k < customers[i].products.length; customers[i].products[k] == \old(customers[i].products[j]))));
public void advertisingProducer(Product product);
?
/*@ public normal_behavior
  @ requires product != null;
  @ requires containsProduct(product);
  @ ensures \result == productIdList.get(product);
  @ also
  @ public exceptional_behavior
  @ signals (ProductNotFoundException e) !containsProduct(product);
  @*/
public /*@ pure @*/ int haveProduct(Product product) throw ProductNotFoundException;
?
/*@ public normal_behavior
  @ requires product != null;
  @ requires number > 0;
  @ ensures containsProduct(product);
  @ ensures productIdList.get(product) = \old(productIdList.get(product)) + number;
public /*@ pure @*/ void makeProducer(Product product, int number);

学习体会

本单元我们主要学习了JML的阅读和使用。

JML可以准确刻画对类和方法的约束，避免二义性的产生，方便了不同开发者之间的合作同一个项目。

同时，在实践中我发现，JML着重与刻画约束，而不是具体的实现，在我们实现代码的时候，应该在满足JML模型约束的条件下，

采取性能最好，代码意义最清晰的的方法实现，以保证实际程序的执行性能和代码质量。