面向对象设计与构造 第三单元总结
作者：互联网
利用JML规格准备测试数据
没有使用Junit工具，而是采用生成大量数据与同学程序对拍的方法。为了保证数据的覆盖率，采用以下几点措施：
1、在数据开始时添加大量的点，减少无用的加边操作。
2、灵活控制每条指令的权重，根据测试的需要进行调整。
3、为了构造特殊数据，在每次生成数据前随机把一部分指令的权重变为零。
4、控制点数，使得图即不会太稀疏也不会太小。
当然，也会手动构造一些测试数据以测试特殊的JML规格（如每组人数\(1111\)的限制）。
本单元架构设计及图模型构建和维护策略
这一单元似乎并不很强调架构设计，因为JML已经把要怎么做给规定好了。
图模型的构建：
将人看做点，关系看作边，value看作边权，可以建出一张图。
对于某一个人，用HashMap维护其连出去的所有边：key为边的另一个人，value为这条边的边权（即value）。
维护策略：
由于指令数不多，给的时间也十分充足，很多信息不需要动态维护，只需要低于平方级别的复杂度内完成一次询问即可。
比如：
qci：用并查集维护，总复杂度\(\mathcal{O}(n\alpha(n))\)。
qlc：用Kruskal算法，单次询问复杂度\(\mathcal{O}(m\log m)\)。
sim：用Dijkstra算法，单词询问复杂度\(\mathcal{O}((n+m)\log n)\)。
其它指令均按照JML规格暴力搞即可。（qgvs除外，按照JML的写复杂度为\(\mathcal{O}(n^2)\)，但应该写成\(\mathcal{O}(m)\)的）。
由于每个指令至多加入一个点或一条边，设\(T=\)总的指令条数，所以\(n,m\le T\)，总复杂度为\(\mathcal{O}(T^2\log T)\)。
代码实现出现的性能问题和修复情况
仅有第二次作业的强测没有得到满分，原因是中测数据太弱，dfg指令我没有把人删掉也没有测出来。
其实我有对拍，拍了几万组数据都没有问题。但我突然发现我qgvs的写法会超时，改了写法之后再对拍，似乎是对拍的参数设置错了，没有拍出来。
加了一两行就修复了。
Network拓展
Advertiser类：投放广告
每个 advertiser 有待投放的广告列表，以及可能的目标人群。
在投放广告的时候，针对特定的消费者人群，不浪费资源。
实现抽象方法：void putAdvertise(int id)，投放编号为 id 的广告，如果不存在对应 id 的广告，抛出异常。
JML规格如下：
public interface Advertiser {
/*@ public instance model non_null Person[] people;
@ public instance model non_null Advertise[] advertise;
@*/
//@ ensures \result == (\exists int i; 0 <= i && i < advertise.length; advertise[i].getId() == id);
public /*@ pure @*/ boolean contains(int id);
/*@ public normal_behavior
@ requires contains(id);
@ assignable people[*].receivedAd;
@ ensures people.length == \old(people.length);
@ ensures (\forall int i; 0 <= i && i < \old(people.length);
@ (\exists int j; 0 <= j && j < people.length; people[j] == \old(people[i])));
@ ensures (\forall int i; 0 <= i && i < people.length && !(people[i] instanceof Customer); \not_assigned(people[i].receivedAd));
@ ensures (\forall int i; 0 <= i && i < people.length && (people[i] instanceof Customer) ==>
@ ( (people[i].receivedAd.length == \old(people[i].receivedAd.length) + 1) &&
@ (\forall int k; 0 <= k && k < \old(people[i].receivedAd.length);
@ (\exists int j; 0 <= j && j < people[i].receivedAd.length; people[i].receivedAd[j] == \old(people[i].receivedAd[k]))) &&
@ (\exists int j; 0 <= j && j < people[i].receivedAd.length; people[i].receivedAd[j] == advertise[id]) );
@ also
@ public exceptional_behavior
@ assignable \nothing;
@ requires !contains(id1);
@ signals (AdvertiseIdNotFoundException e) !contains(id);
@*/
public void putAdvertise(int id) throws AdvertiseIdNotFoundException;
}
Producer类：销售商品
类中维护该 producer 销售的商品列表、商品的库存量以及营业额。
实现抽象方法：void sellCommodity(int id)，销售编号为 id 的商品，销售商品时，如果不存在对应 id 的商品，抛出异常。
JML规格如下：
public interface Producer {
/*@ public instance model non_null Commodity[] commodity;
@ public instance model non_null int[] turnover;
@ public instance model non_null int[] storage;
@*/
//@ ensures \result == (\exists int i; 0 <= i && i < commodity.length; commodity[i].getId() == id);
public /*@ pure @*/ boolean contains(int id);
/*@ public normal_behavior
@ requires contains(id);
@ assignable turnover, storage;
@ ensures turnover.length == \old(turnover.length);
@ ensures storage.length == \old(storage.length);
@ ensures (\forall int i; 0 <= i && i < commodity.length && (commodity[i].getId() != id) == >
@ ( turnover[i] == \old(turnover[i]) && storage[i] == \old(storage[i]) ) );
@ ensures (\forall int i; 0 <= i && i < commodity.length && (commodity[i].getId() == id) == >
@ ( turnover[i] == \old(turnover[i]) + cnt * commodity.price && storage[i] == \old(storage[i]) - cnt ) );
@ also
@ public exceptional_behavior
@ assignable \nothing;
@ requires !contains(id1);
@ signals (CommodityIdNotFoundException e) !contains(id);
@*/
public void sellCommodity(int id, int cnt) throws CommodityIdNotFoundException;
}
Customer类：选择自己偏好匹配的产品购买
类中维护该 customer 拥有的商品 id、收到的广告、拥有的钱、对商品的偏好（假设对所有商品的偏好值都不同）。
实现抽象方法：int buyCommodity()，根据当前收到的广告、拥有的钱和商品的偏好，购买一种商品，返回对应的商品 id。若当前的钱不足以购买任意一种商品，返回\(-1\)。
JML规格如下：
public interface Customer {
/*@ public instance model int[] commodity;
@ public instance model Advertise[] receivedAd;
@ public instance model int money;
@ public instance model Map<Integer, Integer> preference;
@*/
/*@ public normal_behavior
@ requires (\exist int i; 0 <= i && i < receivedAd.length; receivedAd[i].commodity.price <= \old(money));
@ assignable commodity, money;
@ ensures (\exist int i; 0 <= i && i < receivedAd.length; receivedAd[i].commodity.getId() == \result && money == \old(money) - receivedAd[i].commodity.getPrice());
@ ensures !(\exist int i; 0 <= i && i < receivedAd.length; \old(money) >= receivedAd[i].commodity.getPrice() &&
@ preference.get(receivedAd[i].commodity.getId()) > preference.get(\result));
@ ensures commodity.length == \old(commodity.length) + 1;
@ ensures (\forall int i; 0 <= i && i < \old(commodity.length);
@ (\exists int j; 0 <= j && j < commodity.length; people[j] == \old(commodity[i])));
@ ensures (\exist int i; 0 <= i && i < commodity.length); commodity[i] == \result);
@ also
@ public normal_behavior
@ assignable \nothing;
@ requires (\forall int i; 0 <= i && i < receivedAd.length; receivedAd[i].commodity.price > \old(money));
@ ensures \result == -1;
@*/
public int buyCommodity();
}
本单元学习体会
本单元学习了JML规格，在我看来是一种形式化表述，规定了程序应该达到怎样的效果。阅读JML规格其实并没有太大障碍，即使没有系统地学习，也能猜个大概。但编写JML规格确实挺困难的，一方面写出来的不规范，一方面总会遗漏掉一些条件。如果真的想学好的话，还是应该多练练。另外，本单元的测试格外重要，花在测试上的时间甚至比编写代码的时间还要长。测试的时候一定要认真仔细，一不小心就翻车了。
标签：总结,instance,int,id,面向对象,JML,model,public,单元 来源： https://www.cnblogs.com/tybblog/p/16345794.html