第三单元总结

目录

• 1. 测试
  • 1.1 两种测试方法对比
  • 1.2 bug与测试
  • 1.3 数据生成策略
  • 1.4 互测
• 2. 架构
  • 2.1 工具包utils
  • 2.2 图的构建和维护
• 3. 关于程序性能
  • 3.1 并查集
  • 3.2 Kruskal算法
  • 3.3 堆优化的Dijkstra算法
• 4. Network扩展
• 5. 个人体会
  • 5.1 关于规格化
  • 5.2 关于作业

本单元主要进行基于规格的层次化设计，在给定JML规格的基础上实现一个社交网络模拟系统。

1. 测试

在本单元的测试中，我选择了传统的随机生成数据的测试方法，事实证明我的这种选择是一把双刃剑。

1.1 两种测试方法对比

传统的随机数据方法的优点有：

1. 测试过程不依赖于对JML规格的理解，只要对拍的人员内有人正确理解JML即可成功测试
2. 本次作业中，单个方法的体量较小，进行单元测试耗时较长，随机数据测试效率更高
3. 方便对拍，无需手动构造正确结果

缺点有：

1. 无法保证数据覆盖全面（对象状态无法覆盖全面）
2. 无法基于规格测试，若实现与规格不符也不一定检测的出来

总的来说，既然已经给定JML规格，要求实现满足规格的程序，那么 理应使用单元测试来保证实现与规格的一致性。然而考虑到OO课程作业采用的”短快平“模式，作为学生，开发效率可能比严格保证正确性更重要，因此我无奈选择了传统方式进行测试。

单元测试可保证每个小模块的行为正确，再由程序员保证小模块组装逻辑正确。这种测试在每个小模块内部逻辑复杂，小模块间的逻辑不复杂时十分有效。

1.2 bug与测试

在自测过程中，我发现了一个bug。在sendMessage函数中，为了是if语句内部条件更为简洁，我使用了以下写法：

public void sendMessage(int id)
throws RelationNotFoundException, MessageIdNotFoundException, PersonIdNotFoundException {
    if (!containsMessage(id))
    {
        throw new MyMessageIdNotFoundException(id);
    }
    MyMessage msg = (MyMessage)getMessage(id);
    remove(msg);

    if (msg.getType() == 0) {
        MyPerson p1 = (MyPerson)msg.getPerson1();
        MyPerson p2 = (MyPerson)msg.getPerson2();
        if (!p1.isLinked(p2)) {
            throw new MyRelationNotFoundException(p1.getId(), p2.getId());
        }
    } else {
        MyPerson person = (MyPerson)msg.getPerson1();
        MyGroup group = (MyGroup)msg.getGroup();
        if (!group.hasPerson(person)) {
            throw new MyPersonIdNotFoundException(person.getId());
        }
        sendGroupMessage(msg);
    }
}

上述代码第8行对消息进行了移除，而有两种异常的判断在移除之后，这就导致该方法不符合JML规格，该方法的JML规格规定异常抛出时不能进行消息的移除。

由于自己测试时使用了随机数据生成的方法，而随机数据是针对一些特定算法构造的（例如最短路等），因此在随机性不强时，这个bug没有被发现，在作业截止前一个小时使用他人的数据测试时才发现这个bug。

这次经历告诉我，不使用单元测试的结果是，实现与规格可能有不一致的情况。我们的随机数据生成时又没有很强的随机性，因此没有发现这个bug。这说明，在给定JML规格情况下，单元测试还是非常必要的。

1.3 数据生成策略

在我们的随机数据生成时，主要构造了两类数据：

1. 针对典型算法的测试：并查集、最小生成树、最短路
2. 针对其他函数的测试：收发消息等

针对算法的测试中，我将图分为了以下三种分别构造：

1. 近似菊花图：若干个菊花图相连，对于并查集的测试效率高
2. 近似完全图：边数很多，可用于测试最小生成树和最短路
3. 随即图：先生成一颗随机树，随机加边得到随机图
   在这三种图的基础上测试并查集、最小生成树、最短路算法。

1.4 互测

互测中主要使用白盒测试，阅读他人的代码并考虑是否满足JML规格。在白盒测试的过程中，规格化的优势体现得很好。由于每个方法都有相应的规格，若已保证规格正确，程序出现的bug一定能找到实现与规格不一致的地方。

2. 架构

2.1 工具包utils

在本单元作业中，我实现了一个工具包：

|- utils
    |- Edge
    |- Graph
    |- UnionSet

工具包中实现了有关图的抽象的数据结构。

Edge类表示一条有权值的边。

UnionSet类维护了一个集合簇（集合的集合）。初始情况下该集合簇为空集。支持以下操作：

• addElement：向集合簇中添加一个集合（新增集合初始状态下只有一个元素）
• merge：合并集合簇中已有的两个集合，使他们成为一个集合
• inSameSet：查询两个元素是否位于该集合簇中的同一个集合内
• getSetAmount：查询集合簇内的集合数量
  除此之外，还实现了一些其他的private方法。可以看出，这种集合簇的维护，可以使用并查集高效完成。

Graph类维护了一个无向图，主要支持：

• addEdge：增加一条边
• minimalSpanningTree：求最小生成树的权
• shortestPath：求两点间的最短路

构造这个工具包，是基于 ”抽象“ 思想的考虑。JML规要求我们查询社交网络中的连通性isCircle方法，还要求查询图的最小生成树和最短路径。为了
使MyNetwork更加简洁，同时使并查集、图等数据结构易于复用，因此我将这些类进行了抽象，并封装在了工具包中。

在作业迭代中，第一次作业只需查询连通性，第二次作业增加了最小生成树的查询。由于我使用Kruskal算法，仍需动态维护图的连通性，此时只需要在Graph类中
实例化一个UnionSet，在生成最小生成树时使用即可。

2.2 图的构建和维护

在MyNetwork类中，我使用以下属性维护了所有信息：

private final HashMap<Integer, Person> people = new HashMap<>();
private final HashMap<Integer, Group> groups = new HashMap<>();
private final HashMap<Integer, Message> messages = new HashMap<>();
private final HashMap<Integer, Emoji> emojis = new HashMap<>();
private final UnionSet acqUnionSet = new UnionSet();    // 维护集合簇
private final Graph graph = new Graph();                // 维护图

在addRelation方法中，要对acqUnionSet和graph对象进行更新：

public void addRelation(int id1, int id2, int value)
throws PersonIdNotFoundException, EqualRelationException {
    // ...
    acqUnionSet.merge(person1.getId(), person2.getId());
    graph.addEdge(id1, id2, value);
    graph.addEdge(id2, id1, value);
    // ...
}

在查询时，只需调用graph和acqUnionSet对象的相关方法：

• 连通性：acqUnionSet.inSameSet(person1.getId(), person2.getId())
• 最小生成树：g.minimumSpaningTree()（需要重新构造一个图g）
• 最短路：graph.shorestPath(person1.getId(), person2.getId())
  可以看出，工具包的架构设计大大简化了MyNetwork类的复杂性。

3. 关于程序性能

3.1 并查集

使用按秩合并的并查集，单次查询的均摊时间复杂度为\(\Theta (1 + \log^*n)\)，可完全满足题目要求。若不使用按秩合并，至少也应完成路径压缩（否则树形结构可能退化成一条链）。

public class UnionSet {
    private final HashMap<Integer, Integer> father = new HashMap<>();
    private final HashMap<Integer, Integer> rank = new HashMap<>();   // 维护秩
    private int setAmount = 0;

    public void merge(int e1, int e2) {
        int r1 = getRepresentative(e1);
        int r2 = getRepresentative(e2);
        if (r1 != r2) {
            --setAmount;
            if (rank.get(r1) < rank.get(r2)) {      // 按秩合并
                father.put(r1, r2);
            } else if (rank.get(r1) > rank.get(r2)) {
                father.put(r2, r1);
            } else {
                father.put(r2, r1);
                rank.merge(r1, 1, Integer::sum);
            }
        }
    }

    private int getRepresentative(int id) {
        int rep;
        for (rep = id; father.get(rep) != rep; rep = father.get(rep)) {}    // 寻找祖先
        father.put(id, rep);    // 路径压缩
        return rep;
    }

3.2 Kruskal算法

Kruskal算法和并查集共同使用，给边集进行排序后，依次遍历并使用并查集判断该边两点是否联通即可，复杂度为\(\Theta(e\log e + \log^* n)\)，其中\(e\)是边的数量。

public int minimumSpaningTree() {
    UnionSet unionSet = new UnionSet(n);
    Collections.sort(edges);
    int answer = 0;
    for (int i = 0; unionSet.getSetAmount() > 1; ++i) {
        Edge e = edges.get(i);
        if (!unionSet.inSameSet(e.getV1(), e.getV2())) {
            answer += e.getWeight();
            unionSet.merge(e.getV1(), e.getV2());
        }
    }
    return answer;
}

3.3 堆优化的Dijkstra算法

传统的Dijkstra算法维护了起始节点到其他所有节点的最短路径长度，每次选出与其距离最小的点确定其最短路径，并以此松弛其他点的路径。可以看出，该算法每次需要取出一个数组中的最小值，这非常适合使用堆进行维护。

在实际实现中，我们需要构造一个堆，支持以下操作：

• 增加点
• 删除点（某点最短路确定后要从堆中删除，也可不支持该操作，堆中取出后判断该点最短路是否已确定即可）
• 取出值最小的点
  我们可以使用堆实现支持上述操作的数据结构，封装到工具包中，也可以直接使用PriorityQueue。

public int shorestPath(int source, int destination) {
    PriorityQueue<VwithDist> heap = new PriorityQueue<>(11, VwithDist::compareTo);
    HashSet<Integer> found = new HashSet<>();

    heap.add(new VwithDist(source, 0));
    while (!heap.isEmpty()) {
        VwithDist current = heap.poll();
        if (current.getV() == destination) {
            return current.getDist();
        }
        if (found.contains(current.getV())) {
            continue;
        }
        found.add(current.getV());
        for (Edge e : edgeTableHead.get(current.getV())) {
            if (!found.contains(e.getV2())) {
                heap.add(new VwithDist(e.getV2(), current.getDist() + e.getWeight()));
            }
        }
    }
}

这里使用了内置类VwithDist。

4. Network扩展

假设出现了几种不同的Person

• Advertiser：持续向外发送产品广告
• Producer：产品生产商，通过Advertiser来销售产品
• Customer：消费者，会关注广告并选择和自己偏好匹配的产品来购买 -- 所谓购买，就是直接通过Advertiser给相应Producer发一个购买消息
• Person：吃瓜群众，不发广告，不买东西，不卖东西

如此Network可以支持市场营销，并能查询某种商品的销售额和销售路径等。请讨论如何对Network扩展，给出相关接口方法，并选择3个核心业务功能的接口方法撰写JML规格（借鉴所总结的JML规格模式）

增加以下类：

• PurchaseMessage继承Message，表示购买的消息
• AdvertiseMessage继承Message，表示广告消息
• Product：表示产品
• Advertiser、Producer、Customer继承Person

/*@ public normal_behavior
  @ requires containsMessage(id) && (getMessage(id) instance of AdvertiseMessage) && 
  @          getMessage(id).getType() == 0 &&
  @          getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
  @          getMessage(id).getPerson1() != getMessage(id).getPerson2();
  @ assignable messages;
  @ assignable getMessage(id).getPerson1().socialValue;
  @ assignable getMessage(id).getPerson2().messages, getMessage(id).getPerson2().socialValue, 
  @ assignable getMessage(id).getPerson2().ads;
  @ ensures !containsMessage(id) && messages.length == \old(messages.length) - 1 &&
  @         (\forall int i; 0 <= i && i < \old(messages.length) && \old(messages[i].getId()) != id;
  @         (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
  @ ensures \old(getMessage(id)).getPerson1().getSocialValue() ==
  @         \old(getMessage(id).getPerson1().getSocialValue()) + 
  @         \old(getMessage(id)).getSocialValue() &&
  @         \old(getMessage(id)).getPerson2().getSocialValue() ==
  @         \old(getMessage(id).getPerson2().getSocialValue()) + \old(getMessage(id)).getSocialValue();
  @ ensures (\forall int i; 0 <= i && i < \old(getMessage(id).getPerson2().getMessages().size());
  @          \old(getMessage(id)).getPerson2().getMessages().get(i+1) == 
  @          \old(getMessage(id).getPerson2().getMessages().get(i)));
  @ ensures \old(getMessage(id)).getPerson2().getMessages().get(0).equals(\old(getMessage(id)));
  @ ensures \old(getMessage(id)).getPerson2().getMessages().size() == 
  @         \old(getMessage(id).getPerson2().getMessages().size()) + 1;
  @ ensures \old(getMessage(id)).getPerson2().containsAdvertisement(id);
  @ ensures !\old(getMessage(id).getPerson2().containsAdvertisement()) ==> 
  @         (\old(getMessage(id)).getPerson2().getAdvertisement().size() == 
  @         \old(getMessage(id).getPerson2().getAdvertisement().size()) + 1);
  @ also
  @ public normal_behavior
  @ requires containsMessage(id) && (getMessage(id) instance of AdvertiseMessage) && 
  @          getMessage(id).getType() == 1 &&
  @          getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1()) &&
  @          getMessage(id).getPerson1() != getMessage(id).getPerson2();
  @ assignable people[*].socialValue, people[*].advertisement;
  @ ensures !containsMessage(id) && messages.length == \old(messages.length) - 1 &&
  @         (\forall int i; 0 <= i && i < \old(messages.length) && \old(messages[i].getId()) != id;
  @         (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
  @ ensures (\forall Person p; \old(getMessage(id)).getGroup().hasPerson(p); p.getSocialValue() ==
  @         \old(p.getSocialValue()) + \old(getMessage(id)).getSocialValue());
  @ ensures (\forall int i; 0 <= i && i < people.length && 
  @         !\old(getMessage(id)).getGroup().hasPerson(people[i]);
  @          \old(people[i].getSocialValue()) == people[i].getSocialValue());
  @ ensures (\forall int i; 0 <= i && i < people.length && 
  @         \old(getMessage(id)).getGroup().hasPerson(people[i]); people[i].containsAd(id));
  @ ensures (\forall int i; 0 <= i && i < people.length && 
  @         \old(getMessage(id)).getGroup().hasPerson(people[i]); !\old(people[i].containsAdvertisement(id)) ==> 
  @         people[i].ads.size() == \old(people[i].advertisement.size()) + 1);
  @ also
  @ public exceptional_behavior
  @ signals (MessageIdNotFoundException e) !containsMessage(id);
  @ signals (RelationNotFoundException e) containsMessage(id) && getMessage(id).getType() == 0 &&
  @          !(getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()));
  @ signals (PersonIdNotFoundException e) containsMessage(id) && getMessage(id).getType() == 1 &&
  @          !(getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1()));
  @*/
public void sendAdvertisement(int id)
throws RelationNotFoundException, MessageIdNotFoundException, PersonIdNotFoundException;

/*@ public normal_behavior
  @ requires contains(producerId) && containsProduct(productId) && (getPerson(producerId) instanceof 
  @        Producer);
  @ assignable getProducer(producerId).productCount;
  @ ensures getProducer(producerId).getProductCount(productId) ==
  @           \old(getProducer(producerId).getProductCount(productId)) + 1;
  @ also
  @ public exceptional_behavior
  @ signals (PersonIdNotFoundException e) !contains(producerId);
  @ signals (ProductIdNotFoundException e) contains(producerId) && !containsProduct(productId)
  @*/
public void produceProduct(int producerId, int productId)
throws PersonIdNotFoundException, ProductIdNotFoundException;

/*@ public normal_behavior
  @ requires containsProduct(productId);
  @ ensures \result == productList(id).getSalesAmount();
  @ also
  @ public exceptional_behavior
  @ signals (ProductIdNotFoundException e) !containsProduct(productId);
  @*/
public int querySalesAmount(int productId) throws ProductIdNotFoundException； 

5. 个人体会

5.1 关于规格化

在软硬件的开发中，可大致分为设计和实现两个步骤。在开发具有一定复杂性的系统时，设计和实现难以合并，需要分开进行。为了保证开发成品的质量，可分别保证：

1. 设计正确
2. 实现与设计一致

本单元所学习的规格化，我认为主要是为设计提供了一种形式化工具。JML通过定义语法形式，并给JML规格赋予了特定的语义，完成了对方法行为的描述，其本质是通过特制的表意符号表述自然语言中的命题（JML中，表述的命题局限于软件中方法行为）。

将设计形式化的优点之一是无二义性，对方法行为的描述准确严谨。另一个优点是，可通过逻辑方式对设计进行验证。在已经定义语法和语义的基础上，可再定义一系列推理规则，从而构建出一套完整的验证体系（这与数理逻辑中的公理系统一致）。这为设计正确性的保证带来了很多便利。

因此，规格化重点体现在软硬件的设计上。在已经保证设计的正确性后，只需保证实现与设计相一致即可。这个过程也有形式化工具的支持（例如前两个单元已接触过的正则表达式和有效自动机理论）。另外，单元测试也是保证实现与设计一致性的一种方法。

设计：规格
 |
 | 一致性保证：单元测试、形式化方法
 |
实现：算法

5.2 关于作业

个人认为本单元作业并没有体现出JML规格在软件开发过程中的作用。课程组给定的JML规格已经保证了设计的正确性，学生只需使用一定的算法进行实现，并保证实现与设计的一致性即可。由于OO课程作业的“短快平”模式，每周一次的作业仅由逻辑较为简单的方法拼接而成，保证设计和实现的一致性较为简单，甚至不需要使用单元测试。在实现方面，每次作业需要使用一种经典算法，这是可以在本单元进行训练的。

如果本单元作业能涉及到“设计”层面的验证（例如自己设计规格），或要求进行单元测试（例如将方法复杂化），可能能使收获更大。

最后还要感谢一起进行测试的龚悦同学，虽然这次测试工作做的不是很到位，但幸好没有翻车。

标签：总结,int,第三,public,getMessage,&&,new,id,单元
来源： https://www.cnblogs.com/StyWang/p/16348091.html