BUAAOO 第三单元总结

 

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

 

1.通读JML

 

三次作业下来，我都是采取先通读一遍JML规格，大致理解整体的架构，这么做的主要目的就是分析采取的数据结构，以免后面写着写着发现有更高效的数据结构。这里需要做的主要是分析JML规格中对数组的操作，比如第一次作业中Network中有根据id获得Person的操作，我最终就决定了采取Hashmap，又如

 

/*@ public instance model non_null Person[] acquaintance;
  @ public instance model non_null int[] value;
  @*/

 

通过后面的分析就可以知道这两个实际上是一一对应的，这样就完全没必要设置两个数组了，于是我就用了Hashmap

 

private final HashMap<Person, Integer> acquaintance;

 

这显然极大地方便了操作。第三次作业中的

 

/*@ public instance model non_null int[] emojiIdList;
  @ public instance model non_null int[] emojiHeatList;
  @*/

 

也是同理，用一个Hashmap就可以了。

 

我认为，JML只是告诉了我们一条绝对正确的道路（只要经过形式化验证），但是完全没有顾及到性能，所以我们照着JML写代码的时候，千万记得分析他的时间复杂度，而时间复杂度最容易出问题的地方就是数据结构，所以在我们动手写代码之前，要仔细分析项目中数据结构的作用，选择合适的容器，在满足规格描述的同时尽可能地降低时间复杂度。另外一点和前面地数据结构略有不同，就是看着很简单的代码，实际上因为反复的操作而增加运行时间，最明显的就是第二次作业中的getValueSum、getAgeMean和getAgeVar，这个时候就需要思考架构了，将指令实现的步骤分摊开来，减少重复操作即可。总而言之，刚开始需要通读JML了解整体架构，针对时间复杂度采取相应的架构。

 

2.代码实现

 

有JML的第三单元代码明显就比前两个单元好些多了，因为根本不需要思考太多，整体的架构都已经搭好了，并不会出现边写边怀疑整体架构的问题，这就造成了这个单元第一次作业是最轻松的一次，而前两个可以说是最难的一次。

 

照着JML写代码无非就是读懂前置条件以及后置条件，然后相应地加上if-else即可。看JML最烦的一点就是得一条一条看过去，尤其是那些维护数组原先成员的规格描述，这是最浪费时间的，不过也是最能让我们感受到JML强大的地方。然后最困难的就是几个语句嵌套在一起，这使得我们必须断好句，否则可能出现理解的偏差，而理解的偏差是注定导致程序的错误的。

 

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

 

这次的测试基本上只需要看看实现的函数是否严格按照JML的要求来写即可，所以我在测试的时候尽可能将JML所描述的几个分支都测了一遍，当然主要是看看边界条件。

 

符合JML的描述只是满足了程序的正确性，我将重心放在了后面测试性能的方面，JML的描述中高时间复杂度的地方我构造了一些测试数据，也就是卡TLE，比如第二次作业getValueSum、getAgeMean和getAgeVar就是我重点针对的内容，直接不加思考按照规格来写肯定不行，所以专门测试（主要是互测）这些地方就很有必要了，又比如最后一次作业的sendIndirectMessage显然是最容易测出代码时间复杂度的地方。

 

专门卡TLE的测试数据实际上就非常好构造了，只需要根据指令条数算出时间最大值，再用程序生成指令即可。

 

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

 

第一次作业

 

// Person类
/*@ public instance model non_null Person[] acquaintance;
  @ public instance model non_null int[] value;
  @*/
private HashMap<Person, Integer> acquaintance; //<=我使用的，因为上述两个数组实际就是一一对应的
// Network类
/*@ public instance model non_null Person[] people;
  @*/
private HashMap<Integer, Person> personMap; //<=我使用的，便于利用id获得person

 

第二次作业

 

// Person类
/*@ public instance model non_null Message[] messages;
  @*/
private final ArrayList<Message> messages; //<=我使用的，因为考虑到后面的数组顺序问题
// Network类
/*@ public instance model non_null Group[] groups;
  @ public instance model non_null Message[] messages;
  @*/
private HashMap<Integer, Group> groupMap; 
private HashMap<Integer, Message> messageMap; //<=我使用的，因为都和id有关，所以比较方便
// Group类
/*@ public instance model non_null Person[] people;
  @*/
private final HashMap<Integer, Person> personMap; //<=我使用的，和Network类中同理

 

第三次作业

 

// Network类
/*@ public instance model non_null int[] emojiIdList;
  @ public instance model non_null int[] emojiHeatList;
  @*/
private HashMap<Integer, Integer> emojiMap; //<=我使用的，也因为他们是一一对应的

 

显而易见，Hashmap是真的适合这个单元，当然可能还会有更好的容器，但我没有去深入了解，第一反应就是显然是用Hashmap啊，这也反映出Hashmap适用的场景，尤其是通过某个索引值（比如id）获得某个对象的时候。

 

当然，当我们需要得到一个有序的数组的时候，比如有很多的查询最值的需求的时候，我们可能就需要Treemap之类的了，这样能够提升程序的性能。

 

四、性能分析

 

这个单元我并没有在性能方面丢分（这里吐槽一点：第一次作业我因为部分异常处理的时候开头多加了个空格，直接给我强测30分，这种BUG中测测不出来不就是搞心态吗？？？去掉空格就A了，这是真的离谱，强烈要求这里有所改进！），下面根据三次作业逐一分析。

 

第一次作业

 

public boolean isCircle(int id1, int id2) throws PersonIdNotFoundException;
public int queryBlockSum();

 

毫无疑问这里是卡时间复杂度的地方，这里我使用了并查集

 

// Network类
private HashMap<Integer, Integer> fatherMap; //记录父亲（祖先）节点
private int fatherNum; //记录祖先的数量，即有几个连通块，在queryBlockSum直接输出即可
public int fd(int x) { //查询祖先节点，这样在isCircle中只需要比较两个节点的祖先节点是否相同即可
        if (fatherMap.get(x) == x) {
            return x;
        } else {
            int father = fd(fatherMap.get(x));
            fatherMap.replace(x, father);
            return father;
        }
    }

 

第二次作业

 

这次作业中最容易TLE的是getValueSum、getAgeMean和getAgeVar这三个函数，主要是每次查询都真的进行遍历会造成很多的重复操作，因此我设置了这三个变量用以保存需要的量

 

private int valueSum; //value和
private int ageSum; //age和
private int ageSquareSum; //age平方和

 

在查询指令来的时候只需要直接返回这些值，或者花一两步计算一下即可，这样就将查询时的遍历工作分配到了更新维护上面，然后我们只需要在会涉及更改这些量的地方进行更新就行，这里最需要注意的就是

 

public void delFromGroup(int id1, int id2)
            throws GroupIdNotFoundException, PersonIdNotFoundException, EqualPersonIdException; //删人引起value值的变化

 

我是再进行了一次遍历，算出id1相关的value，实际上这是比较冒险的，可以从这里卡一波时间，但是按理论课老师讲的，实际程序中读操作会远多于写操作，所以这里还是无伤大雅的。

 

第三次作业

 

public int sendIndirectMessage(int id) throws MessageIdNotFoundException;

 

最短路径查询，这里我采用的是最常用的堆优化的dijistra算法，核心算法如下

 

public int djs(int id1, int id2) {
    HashSet<Integer> visSet = new HashSet<>(); //标记访问过的节点
    HashMap<Integer, Integer> disMap = new HashMap<>(); //记录节点的路径长度

    Queue<Edge> queue = new PriorityQueue<>(); //堆优化
    queue.add(new Edge(id1, 0));

    disMap.put(id1, 0);
    while (!queue.isEmpty()) {
        Edge now = queue.poll();
        int u = now.getTo();
        int disToU;
        disToU = disMap.getOrDefault(u, 2147483647);
        if (disToU < now.getCost()) {
            continue;
        }
        if (visSet.contains(u)) {
            continue;
        }
        visSet.add(u);
        Person personNow = getPerson(u);
        for (Person person : ((MyPerson) personNow).getAcquaintance().keySet()) {
            int next = person.getId();
            int cost = personNow.queryValue(person);
            int costByU = disMap.get(u) + cost;
            int disToNext;
            disToNext = disMap.getOrDefault(next, 2147483647);
            if (!visSet.contains(next) && (costByU < disToNext)) {
                disMap.put(next, costByU);
                queue.add(new Edge(next, costByU));
            }
        }
    }
    return disMap.get(id2);
}

 

五、架构设计

 

第一次作业

 

第一次作业自己设计的主要就是并查集相关的架构

 

// Network类
private HashMap<Integer, Integer> fatherMap; //用于记录节点的父亲（祖先）节点
private int fatherNum; //用于记录连通块个数
// public void addPerson(Person person) throws EqualPersonIdException;
// public void addRelation(int id1, int id2, int value) throws PersonIdNotFoundException, EqualRelationException; 在这两个函数中对上述两个数据进行更新

 

第二次作业

 

第二次作业自己设计的主要是几个预存的量

 

private int valueSum; //value和
private int ageSum; //age和
private int ageSquareSum; //age平方和

 

然后就是在相关函数中对这些值的更新，这里就不赘述了

 

第三次作业

 

第三次作业自己设计的主要是最短路径算法，上文已经分析过了

 

实际正如第一部分所说，主要就是设计JML中时间复杂度高的地方，三次作业中我自己设计的地方都是为了解决JML不能解决的时间复杂度问题，所以开始时的通读一遍还是很有必要的。