BUAA_OO_第三单元总结

2024-03-29 11:15:34

一、实现规格所采取的设计策略

在本单元的代码实现过程中，由于已经用JML为我们定义了方法的规格，所以只需要将JML翻译成代码语言即可。在翻译的过程中需要确保实现的逻辑严谨以及严格符合JML的规格。

在具体的实现过程中，我的设计策略是首先实现异常类，然后分别实现不同的类。从类的包含关系来看，首先实现较为简单的Person类和Mesage类（第二次作业），接着实现包含这两个类的Gruop类（第二次作业），最后实现较为复杂的Network类。

在实现每个类的方法之前，我会首先通读这个类的JML规格，首先设计出数据的组织形式以及方法的基本实现，比如说使用哪一种容器来组织对应数据，以及是维护一个查询结果还是在每次查询的时候重新进行计算。在完成这些设计之后，再针对具体的JML进行代码语言的实现。

在实现具体方法的时候，我认为有一个小技巧是可以采取的，那就是可以先实现那些异常的行为，最后再实现正常的行为，这样会让代码逻辑更加清晰。然后针对复杂的方法，我认为可以将JML描述拆成很多小部分来阅读，首先弄清楚了每一个小部分实现了什么功能再实现，会更加简单一些（可能吧）。

二、基于JML规格的测试方法和策略

基于JML规格测试方法的正确性

采用Junit单元测试来根据JML测试方法的正确性，可以分为以下三种方法。

  • 具有分支的方法

    对于这种方法需要测试所有的逻辑分支。比如第一次作业中的addPerson方法。

    /*@ public normal_behavior
          @ requires !(\exists int i; 0 <= i && i < people.length; people[i].equals(person));
          @ assignable people;
          @ ensures people.length == \old(people.length) + 1;
          @ ensures (\forall int i; 0 <= i && i < \old(people.length);
          @          (\exists int j; 0 <= j && j < people.length; people[j] == (\old(people[i]))));
          @ ensures (\exists int i; 0 <= i && i < people.length; people[i] == person);
          @ also
          @ public exceptional_behavior
          @ signals (EqualPersonIdException e) (\exists int i; 0 <= i && i < people.length;
          @                                     people[i].equals(person));
          @*/
        public void addPerson(Person person) throws EqualPersonIdException;

    编写测试如下：

    @Test
    public void testAddPerson() throws Exception {
        Mynetwork mynetwork = new Mynetwork();
        Myperson myperson1 = new Myperson(1,"a",10);
        mynetwork.addPerson(myperson1);
        Assert.assertEquals(mynetwork.contains(1),true);
        Assert.assertEquals(mynetwork.contains(2),false);
        Assert.assertEquals(mynetwork.getPerson(1),myperson1);
        Assert.assertEquals(mynetwork.getPerson(2),null);
    }

  • 会抛出异常的方法

    需要测试该抛出异常的时候是否抛出预期的异常。同样以第一次作业的addPerson为例。

    编写异常测试如下：

    @Test(expected = EqualPersonIdException.class)
    public void testAddPersonepi() throws EqualPersonIdException {
    //TODO: Test goes here...
        Mynetwork mynetwork = new Mynetwork();
        Myperson myperson1 = new Myperson(1,"a",10);
        mynetwork.addPerson(myperson1);
        mynetwork.addPerson(myperson1);
    }

  • 维护了中间变量的方法。

    需要测试中间变量可能发生改变的时候是否按照预期完成了改变。比如第二次作业的getValueSum方法。

    /*@ public normal_behavior
          @ requires (\exists int i; 0 <= i && i < groups.length; groups[i].getId() == id);
          @ ensures \result == getGroup(id).getValueSum();
          @ also
          @ public exceptional_behavior
          @ signals (GroupIdNotFoundException e) !(\exists int i; 0 <= i && i < groups.length; 
          @          groups[i].getId() == id);
          @*/
        public /*@pure@*/ int queryGroupValueSum(int id) throws GroupIdNotFoundException;
    ​

    编写测试如下：

    @Test
    public void testSum() throws Exception {
        Mynetwork mynetwork = new Mynetwork();
        Mygroup mygroup = new Mygroup(10);
        mynetwork.addGroup(mygroup);
        Myperson myperson = new Myperson(1,"a",6);
        mynetwork.addPerson(myperson);
        mynetwork.addPerson(new Myperson(2,"b",12));
        mynetwork.addPerson(new Myperson(3,"c",18));
        mynetwork.addPerson(new Myperson(4,"d",24));
        mynetwork.addPerson(new Myperson(5,"e",30));
        mynetwork.addRelation(1,2,40);
        mynetwork.addToGroup(1,10);
        mynetwork.addToGroup(2,10);
        mynetwork.addToGroup(3,10);
        mynetwork.addToGroup(4,10);
        mynetwork.addToGroup(5,10);
        Assert.assertEquals(mynetwork.queryGroupAgeMean(10),18);
        Assert.assertEquals(mynetwork.queryGroupAgeVar(10),72);
        Assert.assertEquals(mynetwork.queryGroupValueSum(10),80);
        mynetwork.addRelation(1,3,50);
        Assert.assertEquals(mynetwork.queryGroupValueSum(10),180);
        mynetwork.delFromGroup(1,10);
        Assert.assertEquals(mynetwork.queryGroupValueSum(10),0);
        Assert.assertEquals(mynetwork.queryGroupAgeMean(10),21);
        Assert.assertEquals(mynetwork.queryGroupAgeVar(10),45);
        Assert.assertEquals(mynetwork.queryGroupPeopleSum(10),4);
    }

基于JML规格测试方法的性能

可以对JML描述中出现了多重循环的方法做针对性的测试，在指令的限制范围内，尽可能多的调用该种方法，测试自己的程序是否超时。

三、容器的选择和使用经验

  • 将Hashmap作为组织Person和对应id，以及id和对应根节点id的方式。之所以选择Hashmap是由于查询方法很多，如果使用Arraylist作为数据组织结构的话可能每次查询的时候都需要遍历一次，但是Hashmap本身能够提供o(1)的查询，所以选择使用Hashmap。

  • 使用Hashset存储不需要查询id的Person，由于Hashset提供了o(1)的查询，在不使用id而是直接使用Person进行查询的时候使用Hashset较为方便。

四、性能问题的分析

第一次作业

重点可以关注的是在JML规格描述中，出现了两重循环的方法，对于这类方法，我们是不能够直接按照JML实现的，需要自己采用其他的方式进行优化。

  • isCircle(int id1, int id2)方法：

    JML描述这个方法的结果是查询的两个id之间是否联通。如果直接按照JML的描述对id1的熟人进行bfs搜索，虽然不会超时，但是性能可能不够好。更好的策略是采用并查集维护每个id及其对应的根节点，在isCircle的判断时，只需要判断根节点是否相同即可。注意需要在addPerson和addRelation方法中对并查集进行维护，同时还需要进行路径压缩。

  • queryBlockSum方法：

    如果直接按照JML描述实现，同样时o(n^2)级别的复杂度，会直接CPU超时。所以我采取了维护连通块数目的方法，可以实现o(1)维护，o(1)查询，只需要在addPerson和addRelation时对连通块数目维护即可。

第二次作业

和之前一样，可能出现性能问题的方法，是按照JML规格直接写会出现o(n^2)复杂度的方法，在本次作业中采用了维护查询值的方法进行优化。

  • getValueSum方法

    JML描述如下：

    /*@ ensures \result == (\sum int i; 0 <= i && i < people.length; 
      @          (\sum int j; 0 <= j && j < people.length && 
      @           people[i].isLinked(people[j]); people[i].queryValue(people[j])));
      @*/
    public /*@pure@*/ int getValueSum();

    直接按照JML描述来写的话会出现两重循环，所以我们维护一个叫做valuesum的查询值，在Group中的addPerson方法和delPerson方法以及Network的addRelation方法中对valuesum进行维护，可以做到o(n)维护，o(1)查询。

第三次作业

在第三次作业中，可能出现性能问题的只有sendIndirectMessage方法，其余方法都可以直接按照JML规格来写。

  • sendIndirectMessage方法：

    按照JML的描述，在这个方法中我们需要求出id对应的人之间的最短路。我用了dijkstra算法，并进行了堆优化，不然可能会超时。由于Java本身提供了优先队列，所以堆优化是很方便的。

五、架构设计

第一次作业

第一次作业中需要自己实现四个带有计数功能的异常类以及自己的Network类和Person类。

  • 异常类：

    • 在实现计数功能的时候用了一个单独的Counter类。

    • 在Counter类中，使用static变量分别计数了每个异常出现的次数和每个id出现某种异常的次数，在记录后者的时候采用了Hashmap容器。

    • 对于异常出现的次数以及id出现特定异常的次数提供了对外的get接口。

  • Person类

    • 由于在规格中，acquaintance和value是一一对应的，所以使用Hashmap来实现在规格定义中分离的acquaintance和value

      private HashMap<Person,Integer> acqs = new HashMap<>();

  • Network类

    • 由于在对Network中的每个人进行操作的时候，绝大部分情况下都是由Person的id去操作对应的人，如果直接按照Arraylist的方式来组织Person数据，在每一次查找具体id对应的人时都需要遍历Arraylist，复杂度较高，所以采用Hashmap来存储对应的id和人。

      private HashMap<Integer, Person> pid;

    • 在isCircle()方法中，需要判断id1和id2对应的Person是否联通，为了便于查询两个人是否连通，我们采用并查集的形式，使用Hashmap来存储人的id和其对应根节点的id。

      private HashMap<Integer, Integer> father;

      在新加入人的时候，将对应的根节点的id设置为自己的id，在将调用addRelation()方法时，判断两个人的根节点是否相同，如果不相同的话将一个人的根节点设置成另外一个，在获取根节点的时候采用了路径压缩如下。

      private int finddad(int id) {
              if (father.get(id).equals(id)) {
                  return id;
              }
              int ans = finddad(father.get(id));
              father.replace(id,ans);
              return ans;
      }

    • 在queryBlockSum方法中，需要返回此时Network里所有Person的连通块数目，如果直接按照规格书写的话会导致超时，所以维护了一个blocksum变量，在加人和加关系的时候对其进行修改。

第二次作业

第二次作业是在第一次作业的基础上新增加了4个异常类，并且新增了Group类和Message类，由于异常类和Person类的实现和第一次作业没有区别，所以接下来对其他的类进行分析。

  • Message类

    基本可以按照JML来实现，没有需要自己更改的地方。

  • Network类

    新增的方法中主要涉及Group类和Message类的添加管理，以及一些查询的方法，查询的方法主要在Group类实现。在整体的架构方面除了多了两类数据（组织方式和Person类似），和第一次作业没有区别。

    • 由于新增了Group类型的数据以及Message类型的数据，并且对于这些数据的查询也主要使用id，所以又新建立了两个Hashmap如下：

      private HashMap<Integer, Group> gid;
      private HashMap<Integer, Message> mid;

  • Group类

    在Group类中涉及到的大多查询类方法都不能够直接按照JML来实现，需要维护一个查询值。

    • 在Group类中对于Person的查询主要是直接传入Person，所以使用Hashset来存储Group包含的Person，在查询的时候较为方便。

    • 关于查询方法，涉及到的又查询Group所包含的Person的Valuesum，以及所有人年龄的均值和方差。对于这些查询都维护一个查询的值：ageSum,asSquare,valueSum，在查询的时候可以直接返回结果，但是需要在添加和删除人以及添加关系的时候对这些查询值进行维护，以在组添加人为例（需要维护以上三个变量）：

      public void addPerson(Person person) {
              this.people.add(person);
              ageSum += person.getAge();
              asSquare += person.getAge() * person.getAge();
              for (Person tmp : people) {
                  if (!person.equals(tmp) && person.isLinked(tmp)) {
                      valueSum += 2 * person.queryValue(tmp);
                  }
              }
          }

第三次作业

第三次作业在第二次作业的基础上增加了2个异常类，同时增加了三个新的消息类，这一部分新增的类都可以直接按照JML规格来书写。同时Person类和Group类基本没有变化，所以只对Network类新增的方法进行架构分析。

  • Network类

    除了sendIndirectMessage方法之外其余都可以直接按照JML规格来写，在实现sendIndirectMessage是需要查找两个id对应的Person之间的最短路，在这里使用了堆优化的dijkstra算法。使用Java自带的优先队列作为堆的模型。在每一次调用sendIndirectMessage方法的时候对两个id所对应的Person之间的最短距离进行dijkstra查询。

图模型构建与维护策略

关于图模型的构建和维护，在课程组给出的设计中基本已经完成了。包括添加人，添加关系，添加组，添加消息等方法。关于自己构建的图模型只有并查集以及dijkstra，具体的构建和维护策略见上。



上一篇：BUAA OO 第二单元总结


下一篇：BUAA_OO_2021_ 第二单元 - 难度巅峰之多线程电梯