其他分享
首页 > 其他分享> > 「BUAA OO」第三单元总结

「BUAA OO」第三单元总结

作者：互联网

「BUAA OO」第三单元总结

目录

零、写在前面

1、任务简介

本单元以掌握 JML 规格 为目标，需要建立一个包含人、群组、网络、消息的信息网络。其中还需要运用少量的图论知识与各种方法来进行优化；人在网络中可视作一个结点，整张网络可以视为一个图，人与人之间的熟人关系可视作带权边，于是便有了各种联通问题、通路问题。

尽管每次作业都有各种各样的函数与花里胡哨的优化操作，但是这个单元的核心应该还是在掌握 JML 的阅读与书写方式

2、JML

然而尽管本单元的主题应该是 jml 的理解与书写，但也没有太多需要赘述，指导书里写得很详尽了；而个人心得则见文末总结

3、架构设计

毕竟这个单元只需实现各个接口，我觉得架构设计实在是不必过分梳理，整体架构见前述“任务简介”即可

各种策略则见后述“性能与优化”

一、性能与优化

不同于第二单元（第二单元由于实时交互所以并不存在绝对的最优调度，因而我没什么优化的想法与动力，搞了个模拟计算动态切换策略已经属于是我最大的挣扎了），这个单元跟第一单元一样极富优化空间，所以我好好研究了一下

通用优化

这个单元通用的一个提升性能的方式是：尽量将各种 List 改写为 HashMap，以尽量避免显式的直接遍历。如网络中的群组可以按如下方式存取（id \(-\) value式的访问方式）：

点此查看JML 
//@ public instance model non_null Group[] groups;

/*@ public normal_behavior
  @ requires !(\exists int i; 0 <= i && i < groups.length; groups[i].equals(group));
  @ assignable groups;
  @ ensures groups.length == \old(groups.length) + 1;
  @ ensures (\forall int i; 0 <= i && i < \old(groups.length);
  @          (\exists int j; 0 <= j && j < groups.length; groups[j] == (\old(groups[i]))));
  @ ensures (\exists int i; 0 <= i && i < groups.length; groups[i] == group);
  @ also
  @ public exceptional_behavior
  @ signals (EqualGroupIdException e) (\exists int i; 0 <= i && i < groups.length;
  @                                     groups[i].equals(group));
  @*/
public void addGroup(/*@ non_null @*/Group group) throws EqualGroupIdException;

/*@ public normal_behavior
  @ requires (\exists int i; 0 <= i && i < groups.length; groups[i].getId() == id);
  @ ensures (\exists int i; 0 <= i && i < groups.length; groups[i].getId() == id &&
  @         \result == groups[i]);
  @ also
  @ public normal_behavior
  @ requires (\forall int i; 0 <= i && i < groups.length; groups[i].getId() != id);
  @ ensures \result == null;
  @*/
public /*@ pure @*/ Group getGroup(int id);

private final HashMap<Integer, Group> groups;

public void addGroup(Group group) throws EqualGroupIdException {
    if (groups.containsKey(group.getId())) {
        throw new MyEqualGroupIdException(group.getId());
    }
    groups.put(group.getId(), group);
}

public Group getGroup(int id) {
	return groups.get(id);
}

观察上例可以注意到，在 HashMap 的实现中可以“自动地”解决一些细节问题：如在 getGroup() 中，get() 失败会直接返回 null 所以无需特判。

借助这个性质，我们可以优化更多的函数，以尽量避免重复的查询/取值：

点此查看JML 
/*@ public normal_behavior
  @ requires (\exists int i; 0 <= i && i < groups.length; groups[i].getId() == id2) &&
  @           (\exists int i; 0 <= i && i < people.length; people[i].getId() == id1) &&
  @            getGroup(id2).hasPerson(getPerson(id1)) == false &&
  @             getGroup(id2).people.length < 1111;
  @ assignable getGroup(id2).people;
  @ ensures (\forall Person i; \old(getGroup(id2).hasPerson(i));
  @          getGroup(id2).hasPerson(i));
  @ ensures \old(getGroup(id2).people.length) == getGroup(id2).people.length - 1;
  @ ensures getGroup(id2).hasPerson(getPerson(id1));
  @ also
  @ public normal_behavior
  @ requires (\exists int i; 0 <= i && i < groups.length; groups[i].getId() == id2) &&
  @           (\exists int i; 0 <= i && i < people.length; people[i].getId() == id1) &&
  @            getGroup(id2).hasPerson(getPerson(id1)) == false && 
  @             getGroup(id2).people.length >= 1111;
  @ assignable \nothing;
  @ also
  @ public exceptional_behavior
  @ signals (GroupIdNotFoundException e) !(\exists int i; 0 <= i && i < groups.length;
  @          groups[i].getId() == id2);
  @ signals (PersonIdNotFoundException e) (\exists int i; 0 <= i && i < groups.length;
  @          groups[i].getId() == id2) && !(\exists int i; 0 <= i && i < people.length;
  @           people[i].getId() == id1);
  @ signals (EqualPersonIdException e) (\exists int i; 0 <= i && i < groups.length;
  @          groups[i].getId() == id2) && (\exists int i; 0 <= i && i < people.length;
  @           people[i].getId() == id1) && getGroup(id2).hasPerson(getPerson(id1));
  @*/
public void addToGroup(int id1, int id2) throws GroupIdNotFoundException, PersonIdNotFoundException, EqualPersonIdException;

public void addToGroup(int id1, int id2) throws GroupIdNotFoundException, PersonIdNotFoundException, EqualPersonIdException {
    Group group = getGroup(id2);
    if (group == null) {
        throw new MyGroupIdNotFoundException(id2);
    }
    Person person = getPerson(id1);
    if (person == null) {
        throw new MyPersonIdNotFoundException(id1);
    }
    if (group.hasPerson(person)) {
        throw new MyEqualPersonIdException(id1);
    }
    if (group.getSize() < 1111) {
        group.addPerson(person);
    }
}

上面有两个优化细节：1、注意判断条件之间的联系，实际代码实现中的 throw 其实是保证了后面的代码在执行前已经满足某个条件了，所以实现时不必像 JML 里一样对每个情况都进行逐条件的完全判断；2、利用 HashMap 获取失败返回 null 的性质，可以先直接 get() 然后再判断是否为 null，以减少一次 contains() 时的查询操作，后续取用时直接拿来用即可

第一次作业

第一次作业的性能核心在于查询是否联通以及统计连通块数目；而采用并查集是很高效的做法，再加上路径压缩可以进一步优化性能。并查集的具体介绍与实现可以参考一篇文章，这篇文章里写得很直观清晰（不过这篇文章里的路径压缩做得不是很完全，可以做得更优）

另外，在 MyPerson 类中存取 acquaintance 与 value 时，可采用如下形式以高效地存取熟人间的联系。

/*@ public instance model non_null Person[] acquaintance;
  @ public instance model non_null int[] value;
  @*/
private final HashMap<Person, Integer> acquaintanceToValue;

（其实有个细节：由于 Person 的 id 在网络中是唯一的，所以其实 new 出来后 ap() 成功的 Person 的“指针值”与其 id 是一一对应的，因此可以直接比较 Person 的“指针值”来比较 id，实现 equals 的判断。然而其实一想就能想到，这只是缘于本次作业中的约束比较严而已，实际上这应该是个很值得注意的易错点——这最终将在第三次作业里暴露出来）

第二次作业

1、表层性能

第二次作业的表层性能核心是在于最小生成树的算法。我采用了 Kruskal 算法，并采用了并查集进行优化。

为了更方便地获取边集，我维护了 LinkedList<Relation> relations 来统计边集，其中 Relation 这个实现了Comparable接口的自定义类包含了 权值、起点、终点三个信息。每调用一次 addRelation() 指令就向该边集中加一条边。在实现 queryLeastConnection() 指令时，先运用 Collections.sort(relations) 对边集进行排序，然后遍历所有节点调用 isCircle() 来判断是否相连，最后根据总节点数连出若干条边即可

值得一提的是：一开始我以为排序算法比较费时，所以在维护插入边集时便采用二分插入，保证边集有序；结果实测这样挺慢......经过查阅资料后发现 java 自带的 sort() 方法是很优的，所以最终还是采取了每来一次 qlc 就调用一次 sort()

2、暗藏杀机

事情开始于一个周三的晚上，当我搞了一通优化+跟 jbt 对了拍以后，我发现我在稀疏群组下的效率较高，而他在稠密群组下的效率较高。起初我没太在意，不过到了大概周四晚上以后，我开始研究其中的差异，结果发现了 qgvs 的磅礴杀机：若直接按照 JML 的规格来书写，当群组里很单纯地有 1111 个人时，即使他们互不为熟人，我的 qgvs 耗时也是惊人的；而 jbt 则由人出发遍历其熟人然后查询其熟人是否在群里，在上述情况下耗时就很短。在意识到这个问题后，我立即做了优化：若某人熟人多，则遍历群组；若熟人少，则遍历熟人。优化后我就起飞了，并且以此构造出了一个蛮有效的 hack 思路，这思路／数据不知道经过各种途径传给了多少人：）

另外，群组内维护一个 ageSum 是必要的，否则 qgav 会超时（至于是否维护各项平方之和 age²Sum，实际测了一下，起码对于我的架构来说应该是不用，维护它反而会更慢；类似地，对于 qgvs，如果直接在 atg、dfg 时维护 value总和，实测在 10w+ 条加人/删人指令下会变得极慢，且在低指令数下也并未比直接遍历求和快——由此可见“优化”也不能想当然地优化，必须要结合实践测试才行）

第三次作业

1、最短路径

我采用的是堆优化的 Dijkstra 算法。不得不说，这次百度百科真是超神了，以文末的模板为参考可以光速写完本次作业中的 sim()。不过其中还有2个优化的空间：

2、移除技巧

众所周知，直接用 for each 边遍历边删除是不行的，一般应该用 Iterator 来一边遍历一边删除。很有意思的是，在我用 Iterator 进行书写后，IDEA 立即标黄提示我优化，于是我便参悟了这样的写法：

public int deleteColdEmoji(int limit) {
    emojiIdToHeat.values().removeIf(heat -> heat < limit);
    messages.values().removeIf(message -> (message instanceof EmojiMessage &&
            !containsEmojiId(((EmojiMessage) message).getEmojiId())));
    return emojiIdToHeat.size();
}

我查看源码后，发现其底层倒也就是用 Iterator 来实现的；但是这样用 removeIf 与 lambda 表达式的写法实在是很优雅

二、测试

这个单元我总算是自己搭了个评测机了！（前两个单元我真就随手搓了点数据然后随便测测就完事）

数据构造

随机数据

这个单元的数据构造不能太随意，需要控制指令比例、指令先后顺序、异常产生等要素。所以随机数据的构造分为两大环节：1、构筑单条指令；2、控制各随机指令的顺序与比例

第一次作业的数据生成器是由 jbt 提供给我的，他完成了各单条指令的构建与简单的全指令生成；然后我写了稍微更强一点的指令顺序、比例控制的内容。其中，对已添加的 person、group、acquaintance 等都进行了存取与维护，并依概率来决定是否产生异常，如下例：

class Data:
    def __init__(self):
        self.people = []
        self.people_acquaintances = {}
        self.groups = []
        self.group_people = {}
        self.messages = []          #这是第二次作业引入的
        self.emoji_library = []     #这是第三次作业引入的

    def ap(self):
        if random.random() < 0.90 or len(self.people) == 0:
            id_ = random.randint(1, 2500)
            if id_ not in self.people:
                self.people.append(id_)
                self.people_acquaintances[id_] = []
        else:
            id_ = random.choice(self.people)
        name = [random.choice(alphabet) for _ in range(random.randint(4, 10))]
        name = ''.join(name)
        age = random.randint(0, 200)
        return 'ap ' + str(id_) + ' ' + name + ' ' + str(age) + '\n'

值得一提的是，为了充分验证 qci() 与 qbs()，我适量控制了 ap() 与 ar() 的比例，使得图的稠密度较为适中

第二次作业的数据生成器由我自己从头写了一个（因为 jbt 上次作业里单条指令的构建写得有点儿烂，还是自己来写比较安心）。为了充分检验 qgvs、qlc，我设置指令数量如下：ar() > ap() >> ag()，即图偏稠密且群组内人数较多

第三次作业的数据生成是最讲究的：

手搓数据

随机数据主要是整体检验，要论“定点爆破”还是得自己搓：

image

第一、二次作业手搓数据时我还是很认真的，特化性强，每一个数据基本只含几个针对性指令，对易错点/易超时的地方进行了精心设计，实测比随机生成的数据更靠谱

然而第三次作业嘛......看文件名也看得出来，我没咋手搓，基本是仅将自动评测时使周边同学们出错的数据部分记录下来了而已（名字已全部匿名替换为xxx）——这是因为第三次作业针对性手搓数据的难度在我看来实在过大，并且感觉没啥可专门构造超时的爆破点（不像 qgvs）；同时自动评测机的效率也已经比较高了，基本不超过 10+ 组数据就能测出大家的 bug

正确性检验

这个单元采用对拍检验，简单写个对拍器即可（别一帮人全寄就行）

时间测试

评测机除了正确性检验以外，还给出了运行的总时长。出乎我事先预料的是，时间反馈信息在本单元里为我提供了最大的帮助——当我发现我在某些数据下明显偏慢时，我就能立马知道我有的地方没有优化到位，然后要做的就是进一步的优化了

三、bug分析

自身bug

强测、互测都全部通过了，自测也没有出过bug（但在优化上做了很多很多个测试／改进版本）

他人bug（互测前）

帮小伙伴们评测时测出了挺多bug，凭印象记录一下（这里的bug专指正确性问题，至于优化不到位在此就不提了）：

第一次作业：几乎没人有错（然而由于自动数据构造上出了瑕疵，直到最后10min我临时手搓的数据才测出了我室友的一个bug（┯_┯））

第二次作业：周边约半数的同学在第一次写 qlc(最小生成树) 的时候都有些奇奇怪怪的错误，不过问题不大（）

第三次作业：周边朋友几乎都被我hack中了起码一次，bug主要还是集中在以下2种：

互测bug

第一次作业：全房没有一个人有bug

第二次作业：早上9点我抛出 qgvs 以 ctle 炸了2个人（也不知道我在群里冒了个泡以后，qgvs() 到底 hack 了多少人），然后就没有测出其他 bug 了（但是互测结束后发现有一个同学被另一个人以 RUNTIME_ERROR 给hack中了一次，这其实说明了我的数据构造并不够全面）

第三次作业：唯一的bug是有一个同学 qgvs() 优化了但优化得不够彻底而依然 ctle，我怀疑上次作业他们房里 qgvs 的构造可能不够强

总的说来，这个单元大家 bug 都蛮少的，毕竟 jml 很明确，每个函数都分别写好的话就是不应该有bug才对，正确性bug基本都集中在第三次作业的 cn() 里了；然而在性能上必须得好好优化一番才能避免 ctle

四、功能拓展

任务需求

假设出现了几种不同的Person

如此 Network 可以支持市场营销，并能查询某种商品的销售额和销售路径等

分析解读

Person 就站一边吃瓜去：）

三者的逻辑

Network 新增操作

加人：加入Advertiser/Producer/Customer/Person

加广告：加入Advertiser不指定其广告内容，当进行该操作时再建立其与Producer及产品的联系

购买产品：Customer花钱买商品，Producer、Advertiser获利

查询某种商品的销售额：查询该种商品在网络中的销售总额（注意：即使是同种商品，经由不同 Advertiser 售出的话，其售价亦可能不同）

查询某种商品的销售路径：应当对所有包含该商品的 Advertiser 进行查询并反馈，最后应当得到一个集合

简化设计

为了简化操作，我们不妨进行这样的规定（同时后续可进行再扩展）：

接口方法

（仅展示Network内新增的属性、方法）

/*@ public instance model non_null String[] procuctList;
  @ public instance model non_null int[] procuctSaleVolumeList;
  @*/

/*@ public normal_behavior
  @ requires contains(id1) && contains(id2) && (getPerson(id1) instanceof Advertiser) &&
  @          (getPerson(id2) instanceof Producer) && !((Advertiser)getPerson(id1)).onSale &&
  @          !(\exists int i; 0 <= i && i < procuctList.length; procuctList[i].equals(getPerson(id2).name));
  @ assignable getPerson(id1).producer, getPerson(id1).sale, procuctList, procuctSaleVolumeList;
  @ ensures ((Advertiser)getPerson(id1)).producer == getPerson(id2);
  @ ensures ((Advertiser)getPerson(id1)).sale == true;
  @ ensures procuctList.length == \old(procuctList.length) + 1;
  @ ensures procuctSaleVolumeList.length == \old(procuctSaleVolumeList.length) + 1;
  @ ensures (\exists int i; 0 <= i && i < procuctList.length;
  @          procuctList[i] == getPerson(id2).name && procuctList[i] == 0);
  @ ensures (\forall int i; 0 <= i && i < \old(procuctList.length);
  @          (\exists int j; 0 <= j && j < procuctList.length; procuctList[j] == (\old(procuctList[i])))) &&
  @           procuctSaleVolumeList[j] == \old(procuctSaleVolumeList[i])));
  @ also
  @ public normal_behavior
  @ requires contains(id1) && contains(id2) && (getPerson(id1) instanceof Advertiser) &&
  @          (getPerson(id2) instanceof Producer) && !((Advertiser)getPerson(id1)).onSale && 
  @          (\exists int i; 0 <= i && i < procuctList.length; procuctList[i].equals(getPerson(id2).name));
  @ assignable ((Advertiser)getPerson(id1)).producer, ((Advertiser)getPerson(id1)).sale
  @ ensures ((Advertiser)getPerson(id1)).producer == getPerson(id2);
  @ ensures ((Advertiser)getPerson(id1)).sale == true;
  @ also
  @ public exceptional_behavior
  @ assignable \nothing;
  @ requires !contains(id1) || !contains(id2) || getPerson(id1).onSale;
  @ signals (PersonIdNotFoundException e) !contains(id1);
  @ signals (PersonIdNotFoundException e) contains(id1) && !contains(id2);
  @ signals (WrongIdentityException e) contains(id1) && contains(id2) &&
  @          !(getPerson(id1) instanceof Advertiser);
  @ signals (WrongIdentityException e) contains(id1) && contains(id2) &&
  @          (getPerson(id1) instanceof Advertiser) && !(getPerson(id2) instanceof Producer);
  @ signals (ProductDuplicatedException e) contains(id1) && contains(id2) &&
  @          (getPerson(id1) instanceof Advertiser) && (getPerson(id2) instanceof Producer) &&
  @          ((Advertiser)getPerson(id1)).onSale;
  @*/
public void addAdvertisement(int id1, int id2) throws
    PersonIdNotFoundException, WrongIdentityException, ProductDuplicatedException;
// id1表示Advertiser的id
// id2表示Producer的id
// 方法所表达的含义即为：让Advertiser为Producer进行销售

/*@ public normal_behavior
  @ requires contains(id1) && contains(id2) && (getPerson(id1) instanceof Customer) &&
  @          (getPerson(id2) instanceof Advertiser) && ((Advertiser)getPerson(id2)).onSale;
  @ assignable getPerson(id1).money, getPerson(id2).money, ((Advertiser)getPerson(id2)).producer.money,
  @            procuctSaleVolumeList;
  @ ensures getPerson(id1).money == \old(getPerson(id1).money) - getPerson(id2).age -
  @          ((Advertiser)getPerson(id2)).producer.age;
  @ ensures getPerson(id2).money == \old(getPerson(id2).money) + getPerson(id2).age;
  @ ensures ((Advertiser)getPerson(id2)).producer.money == \old(((Advertiser)getPerson(id2)).producer.money) +
  @          ((Advertiser)getPerson(id2)).producer.age;
  @ ensures (\exists int i; 0 <= i && i < procuctList.length &&
  @          procuctList[i] == ((Advertiser)getPerson(id2)).producer.name;
  @           procuctSaleVolumeList[i] == \old(procuctSaleVolumeList[i]) + getPerson(id2).age +
  @            ((Advertiser)getPerson(id2)).producer.age);
  @ also
  @ public exceptional_behavior
  @ assignable \nothing;
  @ requires !contains(id1) || !contains(id2) || !getPerson(id1).onSale;
  @ signals (PersonIdNotFoundException e) !contains(id1);
  @ signals (PersonIdNotFoundException e) contains(id1) && !contains(id2);
  @ signals (WrongIdentityException e) contains(id1) && contains(id2) &&
  @          !(getPerson(id1) instanceof Customer);
  @ signals (WrongIdentityException e) contains(id1) && contains(id2) &&
  @          (getPerson(id1) instanceof Customer) && !(getPerson(id2) instanceof Advertiser);
  @ signals (NotOnSaleException e) contains(id1) && contains(id2) &&
  @          (getPerson(id1) instanceof Customer) && (getPerson(id2) instanceof Advertiser) &&
  @          !((Advertiser)getPerson(id2)).onSale;
  @*/
public void purchase(int id1, int id2) throws
    PersonIdNotFoundException, WrongIdentityException, NotOnSaleException;
// id1表示Customer的id
// id2表示Advertiser的id

/*@ public normal_behavior
  @ requires (\exists int i; 0 <= i && i < procuctList.length; procuctList[i] == name);
  @ ensures (\exists int i; 0 <= i && i < procuctList.length; procuctList[i] == name &&
  @          \result == procuctSaleVolumeList[i]);
  @ also
  @ public exceptional_behavior
  @ requires !(\exists int i; 0 <= i && i < procuctList.length; procuctList[i] == id);
  @ signals_only ProductNotFoundException;
  @*/
public /*@ pure @*/ int queryProductSaleVolume(String name) throws ProductNotFoundException;

/*@ public normal_behavior
  @ requires (\exists int i; 0 <= i && i < procuctList.length; procuctList[i] == name);
  @ ensures \forall int i; 0 <= i && i < people.length && (people[i] instanceof Advertiser) &&
  @          ((Advertiser)people[i]).producer.name == name; \result.contains(people[i].name);
  @ also
  @ public exceptional_behavior
  @ requires !(\exists int i; 0 <= i && i < procuctList.length; procuctList[i] == name);
  @ signals_only ProductNotFoundException;
  @*/
public /*@ pure @*/ Set<String> queryProductSaleWays(String name) throws ProductNotFoundException;
// Set的每个元素为：Advertiser.name

五、心得体会

JML

解读&书写

在这里简述一下我解读 jml 的方法：

书写的话，顺序略作调动即可：明确要干什么 -> 理清各种情况 -> 对各个情况分别进行书写

感受

解读 jml 感觉这种语言描述确实无比清晰明确；但一想到如果要自己来书写，就立马头疼不已——课程组的老师、助教们真的辛苦了，最小生成树与最短路径的写法着实令人大开眼界

其实我感觉，与其花大力气写一个大篇幅又间接的 jml，不如用日常语言尽可能描述清楚并给出一些样例，我认为这样明显更直观且更省力——我也由此很好奇在现实里到底有哪些地方在使用 jml

特别鸣谢

首先是 jbt 同学，感谢他在凌晨一直跟我唠嗑，让我在大半夜凹优化时一点儿也不困

这个单元进行本地测评时对拍几乎是必要的，所以我收到了很多同学的jar包，也在帮大家 debug／测时间 时进行了交流——在此感谢与我进行交流的所有同学，如此交流互鉴式的学习使彼此都收获颇丰（前两个单元的作业完全是单打独斗，这个单元的交流收获了更多的乐趣）

标签：OO,Advertiser,id2,作业,BUAA,getPerson,优化,bug,单元
来源： https://www.cnblogs.com/zhengxingyu/p/16345798.html