第三单元博客总结
作者：互联网
第三单元总结性博客作业
一、测试部分
测试数据的准备
对于这次的作业，我们可以根据JML规格的描述来构造测试数据，对每一个方法做出专门的测试。任何一个方法的JML规格都是由requires，assignable，ensures三部分组成，对于有不同情况需要有不同操作的方法，会有多个requires(also)，assignable，ensures。当我们构造测试程序时，要充分考虑这三个部分。
首先是requires(also)部分，这部分是方法正确执行后面内容的前提条件，是方法能够保证正确性的数据范围。对一个或者多个requires(also)部分，我们的测试数据应该保证充分覆盖，要求每一个requires(also)都要有对应的3-5条数据。
其次是ensures部分，按照我的理解，这一部分是对程序执行完此方法之后会对内部数据的改变和返回值进行一个规定。在我们编写测试程序的时候 ，应该考虑“我们的程序在这个方法执行的时候可能犯什么错？”，根据较容易犯错的地方进行专门的数据构造。同时这一部分在编写测试程序验证正确性时也较为有用。
最后是assignable，这部分在我们检查正确性的时候需要格外注意。因为我们在编写程序的时候，这一行小字常常被粗心的同学遗忘和忽略，很容易在编写程序的时候违反assignable的规定。
这里我们拿storeEmojiId函数来举例子。
/*@ public normal_behavior
@ requires !(\exists int i; 0 <= i && i < emojiIdList.length; emojiIdList[i] == id);
@ assignable emojiIdList, emojiHeatList;
@ ensures (\exists int i; 0 <= i && i < emojiIdList.length; emojiIdList[i] == id && emojiHeatList[i] == 0);
@ ensures emojiIdList.length == \old(emojiIdList.length) + 1 &&
@ emojiHeatList.length == \old(emojiHeatList.length) + 1;
@ ensures (\forall int i; 0 <= i && i < \old(emojiIdList.length);
@ (\exists int j; 0 <= j && j < emojiIdList.length; emojiIdList[j] == \old(emojiIdList[i]) &&
@ emojiHeatList[j] == \old(emojiHeatList[i])));
@ also
@ public exceptional_behavior
@ signals (EqualEmojiIdException e) (\exists int i; 0 <= i && i < emojiIdList.length;
@ emojiIdList[i] == id);
@*/
首先是requires(also)部分，我们可以看到requires(also)部分将情况分为了两种一种是emojiIdList没有该元素，一种是emojiIdList中有该元素。在构造数据的时候就应该按照其中有该元素和没有该元素两种。再看ensures部分，第一个和第二个ensures是表示将该元素插入emojiIdList和emojiHeatList之中，第三个ensures则是表示原有的元素和emojiHeatList对应关系不变。因此在构造数据的时候，我们不仅要构造将该元素插入空emojiIdList的数据，也要构造里面有一些别的元素然后再插入元素的数据以便检查能否满足这三个ensures。最后是assignable这部分我们要保证不去改变除了emojiIdList和emojiHeatList之外的数据。
测试工具
使用了这么多次大佬的测试工具以后，我终于第一次编写出了属于我自己的测试工具>_<。
首先是测试数据，测试数据我分为两个部分：
-
根据
JML规格自己手搓的测试数据。 -
根据随机数随机生成的大量数据。
在正确性检查这部分，我同样也是分为两个部分。手搓数据那一部分，由于数据较有针对性并且数据量很小，我自己根据逻辑写出正确结果进行对比。对于随机数生成的大量数据，由于这次作业比较容易对拍，我找到几个同学的代码一起对拍。
根据不同情况生成指令代码如下（以ar为例）：
int id1(){
return (rand()%count);
}
int i = id1();
if(rand()%3!=0){
fprintf(out,"ar %d %d %d\n",id1(),id1(),age());
} else{
fprintf(out,"ar %d %d %d\n",i,i,age());
}
二、架构设计
首先是图节点存储。由于在这次作业中，图节点都是使用同一的id来查询，使用hashmap()来存取最为合适。但是有一些时候我们还需要知道节点顺序或者需要遍历，ArrayList()也有优势之处。因此我是用hashmap()存取为主，ArrayList()存取为辅的方式存取数据（虽然这样做比较浪费空间，维护起来也略微麻烦）。
private HashMap<Integer, Person> mapOfPeople;
private ArrayList<Person> people;
三、性能问题和修复情况
在性能问题这方面，我觉得我还是比较有发言权的>_<，三次作业无一不产生了性能问题。
首先，是第一次作业，我以为本单元作业只需要将JML规格照葫芦画瓢翻译成JAVA就行了，于是我的第一次作业所有的数据都是ArrayList，所有的查询都是一重套一重循环。于是第一次作业我就成功TLE了。
后来我将所有需要查询的数据采用HashMap存取，实现了O(1)查询。并且对于循环中多次使用的节点，采用零时变量存下来，避免一次又一次的查询。
public int getAgeVar() {
int i;
int sum = 0;
int ageMean = getAgeMean();
for (i = 0; 0 <= i && i < people.size(); i++) {
sum = sum + (people.get(i).getAge() - ageMean)
* (people.get(i).getAge() - ageMean);
}
return (people.size() == 0 ? 0 : (sum / people.size()));
}
在第一次作业中，还有qci也是比较难的一个点。由于我傻乎乎的沿着图一点点的查询，于是又TLE。对于这个问题，我才用并查集的方式，将联通的所有节点放在一个容器中。这样，我们只需要查询两个节点是否在一个容器里就可以知道他们是否是连起来的了。
第二次作业是qgvs。我没有将每一个类的valueSum动态维护，而是在查询的时候二重循环计算数值。导致在一些抗压性测试下无法通过。于是，我将程序中便于维护，经常查询的量全部都动态维护起来，提高了性能。
private int valueSum;
public void addPerson(Person person) {
//require
if (!hasPerson(person)) {
people.add(person);
int i;
for (i = 0; i < people.size(); i++) {
if (person.isLinked(people.get(i))) {
valueSum = valueSum + 2 * person.queryValue(people.get(i));
}
}
} else {
System.out.println("input is not meet addPerson's require");
}
}
public int getValueSum() {
return valueSum;
}
第三次是sim。对于dijkstra算法，我们需要找到权值最小的节点进行下一次操作，然而，我在找权值最小的节点时居然使用的是排序……
waitQueue.sort((a, b) -> {
return minLink.get(a) - minLink.get(b);
});
于是我把这个排序改掉，变成遍历，我的朴素dijkstra算法复杂度从O(n^2logn)变成O(n^2)后通过了测试。
public int findMiniWay(HashMap<Integer, Person> personHashMap, Message handleMessage) {
handleMessage.getPerson2().getMessages().add(0, handleMessage);
HashMap<Integer, Integer> minLink = new HashMap<>();
ArrayList<Integer> waitQueue = new ArrayList<>();
waitQueue.add(handleMessage.getPerson1().getId());
minLink.put(handleMessage.getPerson1().getId(), 0);
ArrayList<Person> peopleNext = ((MyPerson) handleMessage.getPerson1()).getAcquaintance();
ArrayList<Integer> valueNext = ((MyPerson) handleMessage.getPerson1()).getValue();
for (int i = 0; i < peopleNext.size(); i++) {
Person person = peopleNext.get(i);
if (!waitQueue.contains(person.getId())) {
waitQueue.add(person.getId());
}
if (minLink.containsKey(person.getId())) {
if (minLink.get(person.getId()) > valueNext.get(i)) {
minLink.put(person.getId(), valueNext.get(i));
}
} else { minLink.put(person.getId(), valueNext.get(i)); }
}
int k = 1;
while (waitQueue.size() > k) {
if (waitQueue.get(k - 1) == handleMessage.getPerson2().getId()) {
break; }
int min = 0;
int mini = 0;
for (int i = k; i < waitQueue.size(); i++) {
if (i == k) {
min = minLink.get(waitQueue.get(i));
mini = k;
} else if (min > minLink.get(waitQueue.get(i))) {
min = minLink.get(waitQueue.get(i));
mini = i; } }
if (mini != k) {
int t = waitQueue.get(mini);
waitQueue.remove(waitQueue.get(mini));
waitQueue.add(mini, waitQueue.get(k));
waitQueue.remove(waitQueue.get(k));
waitQueue.add(k, t);
}
peopleNext = ((MyPerson) personHashMap.get(waitQueue.get(k))).getAcquaintance();
valueNext = ((MyPerson) personHashMap.get(waitQueue.get(k))).getValue();
for (int i = 0; i < peopleNext.size(); i++) {
Person person = peopleNext.get(i);
if (!waitQueue.contains(person.getId())) {
waitQueue.add(person.getId());
}
if (minLink.containsKey(person.getId())) {
if (minLink.get(person.getId()) >
minLink.get(waitQueue.get(k)) + valueNext.get(i)) {
minLink.put(person.getId(),
minLink.get(waitQueue.get(k)) + valueNext.get(i));
}
} else {
minLink.put(person.getId(), minLink.get(waitQueue.get(k)) + valueNext.get(i));
}
}
k++;
}
return minLink.get(handleMessage.getPerson2().getId());
}
四、Network进行扩展
假设出现了几种不同的Person
Advertiser：持续向外发送产品广告
Producer：产品生产商，通过Advertiser来销售产品
Customer：消费者，会关注广告并选择和自己偏好匹配的产品来购买 -- 所谓购买，就是直接通过Advertiser给相应Producer发一个购买消息
Person：吃瓜群众，不发广告，不买东西，不卖东西
如此Network可以支持市场营销，并能查询某种商品的销售额和销售路径等 请讨论如何对Network扩展，给出相关接口方法，并选择3个核心业务功能的接口方法撰写JML规格（借鉴所总结的JML规格模式）
/*@ public normal_behavior
@ requires advertisers.contains(advertiser);
@ assignable advertiser.getAdvertisements();
@ ensures (\forall int i; 0 <= i && i < \old(advertiser.getAdvertisements().size());
@ (\exists int j; 0 <= j && j < advertiser.getAdvertisements().size();
@ advertiser.getAdvertisements().get(j) == \old(advertiser.getAdvertisements()).get(i)));
@ ensures \old(advertiser.getAdvertisements().size()) == advertiser.getAdvertisements().size() - 1;
@ ensures (\exists int i; 0 <= i && i < advertiser.getAdvertisements().size();
@ advertiser.getAdvertisements().get(i) == advertisement)
@ also
@ public exceptional_behavior
@ signals (AdvertiserNotFoundException e) !advertisers.contains(advertiser);
*/
public void sendAdvertisement(Advertiser advertiser,Advertisement advertisement) throws AdvertiserNotFoundException;
//将广告发送给advertiser；
/*
@ public normal_behavior
@ requires contains(personId) && (getPerson(personId) instanceof Customer) && contains(productId)
@ assignable getPerson(personId).products;
@ ensures (\forall Product i; \old(getPerson(personId).hasProduct(i));
@ getPerson(personId).hasProduct(i));
@ ensures getPerson(personId).hasProduct(productId);
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !(\exists int i; 0 <= i && i < people.length; people[i].getId() == id )
@ signals (PersonTypeException e) (\exists int i; 0 <= i && i < people.length; people[i].getId() == id ) && !(getPerson(personId) instanceof Customer)
@ signals (ProductNotFoundException e) (\exists int i; 0 <= i && i < people.length; people[i].getId() == id ) && (getPerson(personId) instanceof Customer) && !(\exists int i; 0 <= i && i < products.length; products[i].getId() == productId);
*/
public void setPreference(int personId, int productId) throws PersonIdNotFoundException, ProductIdNotFoundException;
//设置消费者偏好
/*@ public normal_behavior
@ assignable messages
@ requires contains(customerId) && contains(advertiserId) && contains(product.getProducer);
@ requires getPerson(advertiserId).containsProduct(product);
@ ensures (\forall int i; 0 <= i && i < \old(messages.length);
@ (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
@ ensures (\exists int i; 0 <= i && i < messages.length; messages[i].equals(message) && message.getPerson1.equals(getPerson(advertiserId)) && message.getPerson2.equals(product.getProducer);
@ ensures messages.length == \old(messages.length) + 1;
@ ensures !getPerson(advertiserId).containsProduct(product);
@ also
@ public exceptional_behavior
@ signals (PeronIdNotFoundException) getPerson(advertiserId).containsProduct(product) && !contains(customerId);
@ also
@ public exceptional_behavior
@ signals (PeronIdNotFoundException) getPerson(advertiserId).containsProduct(product) && contains(customerId) && !contains(advertiserId);
@ also
@ public exceptional_behavior
@ signals (PeronIdNotFoundException) (PeronIdNotFoundException) getPerson(advertiserId).containsProduct(product) && contains(customerId) && contains(advertiserId) && !contains(product.getProducer);
@ also
@ public exceptional_behavior
@ signals (ProductIdNotFoundException) (PeronIdNotFoundException) getPerson(advertiserId).containsProduct(product) && contains(customerId) && contains(advertiserId) && contains(product.getProducer) && !getPerson(advertiserId).containsProduct(product);
@*/
void addBuyProductMessages(int customerId, int advertiserId, Product product);
//购买产品
五、本单元学习体会
就个人体验而言，这一单元我的oo课程体验不是很好。虽然得的分数也不少，但是在做作业的过程中被一个接一个的性能问题搞得晕头转向。所以在这我想建议课程组在以后的课程设计中能优化一下课程体验，开开心心的学到知识总比愁眉苦脸的学到知识要好得多。
再说说学习收获。随着这一单元的学习逐步深入，我对JML规格的看法也是逐步改变。在第一次作业的时候，我其实并不能真正理解JML规格的优点。看着比实现代码还要长的JML规格，我内心有一个声音一直在问“我为啥要学这奇怪的东西？”。再加上第一次接触这种规格，读规格可以说是非常费劲。尤其是长长一串规格，认真分析好久之后发现它只是想表达一个很简单的意思的时候，感觉十分恶心，让我对这个东西的实用性产生了深深的怀疑。但是随着作业的进行，我发现我之前的观点是不对的。当我完成到第二次作业的时候，我，站在一个底层程序员的视角，觉得这种规格还是十分有价值的。我发现通过JML规格来写代码，能够很轻松的避免软件开发过程种交流的歧义。回想第二单元，第一单元，每一次指导书下发之后，助教都会因为初版指导书内容描述不清，或者是表达有歧义，不完全，而对指导书进行修改。而第三单元并没有这种情况，也没有同学对指导书有歧义的地方进行质疑。设想一个软件开发团队，由两个人组成，一个是叫做“课程组”的程序员，一个是叫做“学生”的程序员。“课程组“负责软件的框架设计、功能设计，而”学生“需要负责将”课程组“的设计实现成真正的代码。如果不使用类似JML这类工具，”学生“很可能无法真正理解”课程组“的设计，从而写出错误的代码。
在oo课程之外，我也和别人组团写过代码。写代码之前，我们一起做过规划，你写这一部分，我写这一部分，他写这一部分。当我们将自己完成的那一部分代码放在一起的时候，我们傻眼了，我们发现：有一些代码由于沟通不完全，实现的功能和负责设计的同学设想的有些不太一样；有一些代码虽然在逻辑上没有太大问题，但是由于接口不匹配很难融入到我们的设计框架里面……通过这一单元的学习，我觉得之后我在团队编码的时候，可以尝试用类似JML规格的方式让团队协作更加紧密有效。
标签：总结,ensures,get,int,博客,person,minLink,waitQueue,单元 来源： https://www.cnblogs.com/minili0111/p/16345797.html