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

OO第三单元总结

作者:互联网

OO第三单元总结

一、梳理架构设计

1.1 整体架构分析与图的模型构建

1.1.1 架构梳理

这一单元的作业要求我们完成一个简单的社交关系网络,其最终结构大致如下:

而本单元最终的目标是构建上述的社交网络,并实现以下功能:

1.1.2 图的模型构建

由上述的梳理,我们可以自然而然的得到一个带权无向图,其中,人(person)是图中的节点,关系(relation)是图中的带权边,而认识的人(acquaintance)可以看做是邻接表,群组(group)则是节点集的子集。在维护这个图结构时,我们通过add_personadd_relation等指令来构建这个图,并通过其他的指令来完善每一个人或群组的信息。

1.1.3 作业难点分析

本次作业如果仅仅按照JML规格进行书写,必然不会是一个优秀的代码实现,我们必须要寻求时间复杂度较低的算法来进行优化、或是对某些信息进行动态维护,才能够保证程序运行不会超时。

第九次作业

第九次作业的难点主要在于实现可关联的人的查询,即query_circle指令(qci)与query_block_sum指令(qbs)。这两条指令要求我们找出两个人之间的联系,若两个人之间可以通过其他人获得关联,则为有联系。这就要求我们在图中找到任意两个节点之间的一条通路,或是找到连通分支,判断两个人是否在同一个连通分支当中。

第十次作业

第十次作业的难点主要有以下几点:

  1. 计算群组内所有人的年龄的方差时,必须用公式进行简化,否则会有较高的时间复杂度。
  2. 计算群组内所有人的认识的人的价值总和时,建议动态维护,或是对集合的大小进行判断再进行遍历,否则会有较高的时间复杂度。
  3. 找出与某个人关联的所有人,并找出这个关联,其权值之和最小,即query_least_connection指令(qlc)。这要求我们在图中找到节点所在的最小生成树。
第十一次作业

第十一次作业的难点主要在于发送间接的消息,即若两个人没有直接的联系,则找出两个人之间的权值最小的一条通路,将消息发送出去,即send_indirect_message指令(sim)。这要求我们在图中找到两个节点之间的最短路径。

1.2 数据维护策略与算法实现

1.2.1 基本数据的动态维护

在这个单元的作业中,要想避免超时,就需要对某些数据进行动态维护。

  1. 在群组中查询所有人年龄的平均值与方差时,如果采用直接遍历的方法,对于平均值,时间复杂度为\(O(n)\),对于方差,时间复杂度就会变为\(O(n^2)\)。而采用数学公式推导可得:

    \[var= \frac{n∑x^2−2⋅(⌊\frac{\sum x}{n}⌋)⋅∑x+n⋅(⌊\frac{\sum x}{n}⌋)^2}{n} \]

    故我们应当维护两个变量ageSumageSqrSum分别代表年龄和与年龄的平方和,然后用上述公式进行计算,可得到\(O(1)\)的时间复杂度

  2. 在群组中查询所有人的认识的人的价值时,也可以动态维护一个变量valueSum。这需要我们每往群组中加一个人时,就要遍历其熟人集合,将同在当前群组中的人的价值加进valueSum中。同时,在添加联系(relation)时,还要考虑这两个人所在的群组,将涉及到的群组的valueSum进行更新。

1.2.2 并查集

在实现qbsqci指令时我们需要用到并查集来简化时间复杂度。

并查集的思路其实很简单,我们知道每一个相连通的节点都在同一个连通分支中,而连通分支就必然有一个生成树,我们只需要为每一个节点维护一个父节点,则在同一个连通分支中的节点都有着同一个父节点。这样我们在查询两个人之间是否有关联时,只需要查询两个人的父节点是否相同即可。

具体来说,我们需要实现以下几个函数:

  1. find函数用来找节点的父节点,这里我们用到了路径压缩,将寻找过程中找到的每一个节点的父节点均更新:

    public Person find(Person person) {
        Person father = people.get(person);
        if (person != father) {
        	father = find(father);
        }
        people.put(person, father);
        return father;
    }
    
  2. isSameSet函数用来判断两个节点是否在同一个连通分支中:

    public boolean isSameSet(Person person1, Person person2) {
    	return find(person1).equals(find(person2));
    }
    
  3. union函数用来将两个连通分支合并:

    public void union(Person person1, Person person2) {
        Person head1 = find(person1);
        Person head2 = find(person2);
    
        if (!head1.equals(head2)) {
            int rank1 = rank.get(head1);
            int rank2 = rank.get(head2);
            if (rank1 > rank2) {
                people.put(head2, head1);
                rank.put(head1, rank.get(head1) + rank.get(head2));
        	}
            else {
                people.put(head1, head2);
                rank.put(head2, rank.get(head2) + rank.get(head1));
            }
            setsCount -= 1;
        }
    }
    

1.2.3 最小生成树——Kruskal算法

在实现qlc指令时我们需要找最小生成树,这里我们使用Kruskal算法,结合并查集来简化时间复杂度。

其具体实现如下:

public int queryLeastConnection(int id) throws PersonIdNotFoundException {
    if (!contains(id)) {
    	throw new MyPersonIdNotFoundException(id);
    }
    else {
        int sum = 0;
        Collections.sort(edgeSet);
        DisjointSetUnion tmpSet = new DisjointSetUnion();
        int tmpId = this.people.find(id);
        for (int item : this.people.getLink().keySet()) {
            if (this.people.find(item) == tmpId) {
                tmpSet.getLink().put(item, item);
                tmpSet.getRank().put(item, 1);
                tmpSet.addSetsCount();
            }
        }
        int edgeNum = this.people.getRank().get(tmpId) - 1;
        int findNum = 0;
        for (int i = 0; i < edgeSet.size(); i++) {
            if (findNum == edgeNum) {
            	break;
            }
            Edge tmpEdge = edgeSet.get(i);
            int tmpPerson1 = tmpEdge.getPerson1();
            int tmpPerson2 = tmpEdge.getPerson2();
            if (!tmpSet.getLink().containsKey(tmpPerson1)) {
            	continue;
            }
            if (tmpSet.find(tmpPerson1) != tmpSet.find(tmpPerson2)) {
                sum += tmpEdge.getWeight();
                tmpSet.union(tmpPerson1, tmpPerson2);
                findNum++;
            }
        }
        return sum;
    }
}

1.2.4 单源最短路径——堆优化的Dijkstra算法

在实现sim指令时我们需要找两个节点之间的单源最短路径,这里我们使用堆优化的Dijkstra算法来简化时间复杂度。

其具体实现如下:

private int dijkstra(int id1, int id2) {
    HashMap<Integer, Boolean> visited = new HashMap<>();
    HashMap<Integer, Integer> dist = new HashMap<>();
    int tmpId = this.people.find(id1);
    for (int item : this.people.getLink().keySet()) {
        if (this.people.find(item) == tmpId) {
            visited.put(item, false);
            dist.put(item, Integer.MAX_VALUE);
        }
    }

    PriorityQueue<Dedge> pq = new PriorityQueue<>();
    pq.offer(new Dedge(id1, 0));
    dist.put(id1, 0);

    while (!pq.isEmpty()) {
        if (visited.get(id2)) {
        	break;
    	}
        int destination = pq.poll().getTo();
        if (visited.get(destination)) {
            continue;
        }
        visited.put(destination, true);
        for (Person item : ((MyPerson)(getPerson(destination))).getAcquaintance().keySet()) {
            int to = item.getId();
            if (visited.get(to)) {
            	continue;
        	}
        	int len = ((MyPerson)(getPerson(destination))).getAcquaintance().get(item);

            if (dist.get(to) > dist.get(destination) + len) {
                dist.put(to, dist.get(destination) + len);
                pq.offer(new Dedge(to, dist.get(to)));
            }
        }
    }
    return dist.get(id2);
}

二、基于JML规格的测试

2.1 正确性检验与性能测试

  1. 首先我们需要参考JML规格,针对方法的执行逻辑,构造相应的数据来测试方法的正确性。
  2. 进一步,我们还需要找到每个方法的边界条件,手动构造数据,测试是否会在边界条件出错
  3. 最后,我们还需要对时间复杂度进行针对性测试。这一部分需要我们手动构造一些针对性数据,来测试程序是否会在极限情况下运行超时。例如,对于qgavqgvsqlcqci指令,都可以构造出十分耗时的数据,来测试性能情况

2.2 随机数据生成与自动化测试

为了保证程序的正确性,我们最好还是采用随机生成数据与多人对拍的方法进行更为全面的测试。

在这一单元的自动化测试中,鸣谢zxy、jbt两位大佬的编写的评测机。我也试着参考了他们的数据生成器尝试了自己的评测机的编写,整个过程让我获益良多。

三、性能分析与bug分析

3.1 性能分析

3.2 bug分析

得益于和几位大佬的对拍,本单元的三次作业在强测和互测中均未出现bug。

在课下自己测试与互测时,发现的bug主要有两个方面:

  1. 性能方面:

    • 如果qbsqci指令没有使用并查集,而是使用bfsdfs,可能会出现超时。
    • qgavqgvs等指令如果只是用简单的二重循环遍历,则会导致超时。
  2. 正确性方面:

    • qlc指令计算错误,应该是指针问题。
    • qm指令精度计算错误。

四、心得与体会

本单元的目的主要是让我们学习契约式编程的思想,并通过对JML规格的阅读以及按照规格撰写代码来训练我们契约式编程的能力。通过这一单元的学习,我熟悉了JML规格的阅读,并了解到了在今后的学习与开发中,契约式编程的重要性与实际应用。

五、Network扩展与规格撰写

5.1 题目

假设出现了几种不同的Person

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

5.2 接口方法设置

规定

新增接口

新增属性与方法

新增异常

新增接口、属性与方法简要源码

public interface Advertiser extends Person {
}

public interface Producer extends Person {
    //@ public instance model int cost; 商品的成本
    //@ public instance model int productNum; 剩余商品的数量
    
    //@ ensures \result == productNum;
    public /*@ pure @*/ int getProductNum();
    
    /*@ public normal_behavior
      @ assignable socialValue;
      @ ensures money == \old(money) - cost;
      @ ensures productNum == \old(productNum) + 1;
      @*/
    public int produce();
}

public interface Customer extends Person {
    //@ public instance model non_null int[] preferenceId; 喜好商品的id
    //@ public instance model non_null int[] ownProductId; 已经购买的商品id
}

public interface AdvertisementMessage extends Message {
    //@ public instance model int productId; 广告宣传的商品的id
	//@ public instance model int money;广告消息的成本
    
    //@ public invariant socialValue == productName * 2;

    //@ ensures \result == productName;
    public /*@ pure @*/ int getProductId();
    
    //@ ensures \result == money;
    public /*@ pure @*/ int getMoney();
}

public interface BuyProductMessage extends Message {
    //@ public instance model int advertiserId; 中转的广告商Id
    //@ public instance model int productId; 购买的商品Id(即生产商Id)
    //@ public instance model int money; 商品的购买价格

    //@ public invariant socialValue == productName * 2;

    //@ ensures \result == money;
    public /*@ pure @*/ int getMoney();
    
    //@ ensures \result == productName;
    public /*@ pure @*/ int getProductId();
    
    //@ ensures \result == advertiserName;
    public /*@ pure @*/ int getAdvertiserId();
}

5.3 JML规格撰写

  1. 发送广告消息:sendAdvertisementMessage(int id)

    	/*@ public normal_behavior
          @ requires containsAdvertisementMessage(id) && getMessage(id).getType() == 0 &&
          @          getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
          @          getMessage(id).getPerson1() != getMessage(id).getPerson2() &&
          @          getMessage(id).getPerson1().getMoney() < getMessage(id).getMoney() &&
          @          contains(productId);
          @ assignable messages, advertisementMessages;
          @ assignable getMessage(id).getPerson1().socialValue;
          @ assignable getMessage(id).getPerson2().messages, getMessage(id).getPerson2().socialValue;
          @ assignable getMessage(id).getPerson1().money;
          @ assignable getMessage(id).getPerson2().preferenceId;
          @ 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 !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 !containsAdvertisementMessage(id) && advertisementMessages.length == 
          @ 		\old(advertisementMessages.length) - 1 &&
          @         (\forall int i; 0 <= i && i < \old(advertisementMessages.length) && 
          @ 		\old(advertisementMessages[i].getId()) != id;
          @         (\exists int j; 0 <= j && j < advertisementMessages.length; 
          @ 		advertisementMessages[j].equals(\old(advertisementMessages[i]))));
          @ 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) == \old(getMessage(id));
          @ ensures \old(getMessage(id)).getPerson2().getMessages().size() == 
          @ 		\old(getMessage(id).getPerson2().getMessages().size()) + 1;
          @ ensures \old(getMessage(id)).getPerson2().getMoney() == 
          @ 		\old(getMessage(id).getPerson2().getMoney()) - \old(getMessage(id)).getMoney;
          @ ensures getMessage(id).getPerson2().preferenceId.length == 
          @ 		\old(getMessage(id).getPerson2().preferenceId.length) + 1;
          @ ensures (\forall int i; 0 <= i && i < \old(getMessage(id).getPerson2().preferenceId.length);
          @          (\exists int j; 0 <= j && j < getMessage(id).getPerson2().preferenceId.length; 
          @ 		getMessage(id).getPerson2().preferenceId[j] == (\old(people[i]))));
          @ ensures (\exists int i; 0 <= i && i < getMessage(id).getPerson2().preferenceId.length; people[i] 
          @ 		== getMessage(id).getProductId());
          @ also
          @ public exceptional_behavior
          @ signals (MessageIdNotFoundException e) !containsAdvertisementMessage(id);
          @ signals (RelationNotFoundException e) containsMessage(id) && getMessage(id).getType() == 0 &&
          @          !(getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()));
          @ signals (NoMoneyException e) getMessage(id).getPerson1().getMoney() < getMessage(id).getMoney();
          @ signals (ProductIdNotFoundException e) !contains(productId);
          @*/
        public void sendAdvertisementMessage(int id) throws
                RelationNotFoundException, MessageIdNotFoundException, 
    			NoMoneyException,ProductIdNotFoundException;
    
  2. 发送购买消息:sendBuyProductMessage(int id)

    	/*@ public normal_behavior
          @ requires containsBuyProductMessage(id) && getMessage(id).getType() == 0 &&
          @          getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
          @          getMessage(id).getPerson1() != getMessage(id).getPerson2();
          @          getMessage(id).getPerson1().getMoney() < getMessage(id).getMoney() &&
          @          contains(productId) &&
          @          !(\forall int i; 0 <= i && i < getMessage(id).getPerson2().preferenceId.length; 
          @ 			getMessage(id).getPerson2().preferenceId[i] != getMessage(id).getProductId());
          @ assignable messages, buyProductMessages;
          @ assignable getMessage(id).getPerson1().socialValue;
          @ assignable getMessage(id).getPerson2().messages, getMessage(id).getPerson2().socialValue;
          @ assignable getMessage(id).getPerson1().money, getMessage(id).getPerson2().money;
          @ assignable advertisers[*].money;
          @ assignable getMessage(id).getPerson2().ownProductId;
          @ assignable getMessage(id).getPerson1().productNum;
          @ 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 !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 !containsBuyProductMessage(id) && buyProductMessages.length == 
          @ 		\old(buyProductMessages.length) - 1 &&
          @         (\forall int i; 0 <= i && i < \old(buyProductMessages.length) && 
          @ 		\old(buyProductMessages[i].getId()) != id;
          @         (\exists int j; 0 <= j && j < buyProductMessages.length; 
          @ 		buyProductMessages[j].equals(\old(buyProductMessages[i]))));
          @ 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) == \old(getMessage(id));
          @ ensures \old(getMessage(id)).getPerson2().getMessages().size() == 
          @ 		\old(getMessage(id).getPerson2().getMessages().size()) + 1;
          @ ensures \old(getMessage(id)).getPerson2().getMoney() == 
          @ 		\old(getMessage(id).getPerson2().getMoney()) - \old(getMessage(id)).getMoney;
          @ ensures \old(getMessage(id)).getPerson1().getMoney() == 
          @ 		\old(getMessage(id).getPerson2().getMoney()) + \old(getMessage(id)).getMoney * 0.9;
          @ ensures (\forall Person p; advertisers.hasPerson(p); p.getMoney() == \old(p.getMoney()) + 
          @ 		(\old(getMessage(id)).getMoney * 0.9) / advertisers.length));
          @ ensures getMessage(id).getPerson2().ownProductId.length == 
          @ 		\old(getMessage(id).getPerson2().ownProductId.length) + 1;
          @ ensures (\forall int i; 0 <= i && i < \old(getMessage(id).getPerson2().ownProductId.length);
          @         (\exists int j; 0 <= j && j < getMessage(id).getPerson2().ownProductId.length; 
          @ 		getMessage(id).getPerson2().ownProductId[j] == (\old(people[i]))));
          @ ensures (\exists int i; 0 <= i && i < getMessage(id).getPerson2().ownProductId.length; people[i] 
          @ 		== getMessage(id).getProductId());
          @ ensures \old(getMessage(id)).getPerson1().getProductNum() == 
          @ 		\old(getMessage(id).getPerson2().getProductNum()) - 1;
          @ also
          @ public exceptional_behavior
          @ signals (MessageIdNotFoundException e) !containsAdvertisementMessage(id);
          @ signals (RelationNotFoundException e) containsMessage(id) && getMessage(id).getType() == 0 &&
          @          !(getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()));
          @ signals (NoMoneyException e) getMessage(id).getPerson2().getMoney() < getMessage(id).getMoney();
          @ signals (ProductIdNotFoundException e) !contains(productId);
          @ signals (NotPreferenceException e) (\forall int i; 0 <= i && i < 
          @ 			getMessage(id).getPerson2().preferenceId.length; 
          @ 			getMessage(id).getPerson2().preferenceId[i] != getMessage(id).getProductId())
          @*/
        public void sendAdvertisementMessage(int id) throws
                RelationNotFoundException, MessageIdNotFoundException, 
    			NoMoneyException,ProductIdNotFoundException, NotPreferenceException;
    
  3. 查询某一消费者购买的某一种产品的数量:queryCustomerOwnProduct(int id1, int id2)

    	/*@ public normal_behavior
    	  @ requires contains(id1);
    	  @ ensures \result == (\sum int i; 0 <= i && i < getPerson(id1).ownProduct.length && 
    	  @ 		getPerson(id1).ownProduct[i] == id2);
          @ also
          @ public exceptional_behavior
          @ signals (PersonIdNotFoundException e) !contains(id1);
          @*/
        public /*@ pure @*/ int queryCustomerOwnProduct(int id1, int id2) throws
            PersonIdNotFoundException;
    

标签:OO,总结,get,int,public,Person,getMessage,id,单元
来源: https://www.cnblogs.com/Levelower/p/16345746.html