OO第三单元（JML）总结

Posted 2021-05-30 daydayup_2021

第三单元（JML）总结

一、JML学习小结

      JML是一种面向JAVA的行为接口规格语言 。它用逻辑严格描述规格，使设计更为规范，并且更利于测试与维护。

规格的总体结构
      对于JAVA的类的规格，一般包含了数据（类型）规格和方法规格。

• 类型规格
  • 不变式invariant：所有可见状态下都必须满足的特性
  • 状态变化约束 constraint：对状态变化前后的关系进行约束
• 方法规格
  • 核心内容
    • 前置条件requires：调用前提
    • 副作用assignable：方法执行过程中的副作用，通常为会修改的数据
    • 后置条件ensures：执行结果约束
  • 方法的多种行为
    • 使用 public normal_behavior 、public exceptional_behavior来分别定义方法的正常与异常行为。可以依据前置条件的不同，定义多个正常行为或异常行为，用also连接。
    • 抛出异常可使用signals或signals_only

常用的表达式

• 原子表达式

表达式	含义
\\result	方法执行返回值
\\old(expr)	expr这一表达式在方法执行前的取值或引用
\\not_assigned(x)	表示在方法执行过程中x是否被赋值

• 量词表达式

表达式	含义
\\forall	全称量词，要求范围内所有元素满足约束
\\exists	存在量词，存在范围内某个元素满足约束
\\sum	在给定范围内求和

二、基于规格的实现策略与性能考虑

      本单元作业最终目的是完成模拟社交网络（Network），实现人（Person）与人（或分组Group）之间的信息（Message）传递功能，并提供对个人、分组及社交网络的度量。由于是基于规格设计，框架上并没有太多需要自己设计的地方，更多在于具体的实现。因此接下来将首先分析三次作业的功能实现与性能考虑。

第一次作业

规格的实现策略

      第一次作业仅需实现Person和Network，也就是图中节点和边信息的维护，以及图的一些特征的查询。由于初次接触规格，基本上完全按照规格来设计类的属性以及方法。其中类的属性（也就是数据）使用了容器HashMap来实现，提高查找效率。类的方法就直接按照规格的各种行为（含异常）实现即可，需要注意的就是认真阅读规格、把所有情况都考虑到。

性能考虑

      这次比较复杂的是Network里的isCircle和queryBlockSum方法，也就是判断图中两点的连通性、计算连通块数量。在本次作业中采用的dfs算法，在强测和互测中也没有出现问题。后来在第二次作业中为了进一步提高性能，使用了并查集算法，用一个Hashmap容器实现father，以记录每个连通块的源头（压缩路径）。

第二次作业

实现规格的设计策略

      第二次作业增加了分组Group和信息类Message。前者是主要是提供对特定子图的信息查询，属性上主要是存储分组中含有的节点（人），采用了HashMap实现。后者的类规格很简单，直接实现即可。由于Message的加入，Network需要实现发送信息的功能，由具体方法实现，并增加了对信息的存储（容器依然使用HashMap）。相关方法的规格也并不复杂，保证准确完成每一个ensures。

性能考虑

      这一次比较复杂的是Group里的getValueSum和getAgeVar方法。对此我采用的策略都是使用冗余数据缓存，这意味着需要时刻进行维护。

      对于age，冗余存储了其和与平方和，这只需要在组里增加或删除人的时候相应地加减进行维护。这里更需要注意的是精度问题（因为这里的计算是int的除法）。比如计算agevar即方差，根据规格是agevar \\(= \\frac{\\sum_n{(x_i - \\bar{x})}^2}{n} = \\frac{\\sum_n{x_i^2} - 2\\bar{x}\\sum_n{x_i} + n(\\bar x)^2}{n}\\)，这是完全按照规格展开的，没有精度差异。但实际上，它可以近一步化简成\\(\\frac{\\sum_n{x_i^2} - 2\\bar{x}\\sum_n{x_i}}{n} + (\\bar x)^2\\)甚至是\\(\\frac{\\sum_n{x_i^2}}{n} - (\\bar x)^2\\)，不过经测试这会有精度问题。
      对于valuesum即边的权重之和（每边计算两次），除了在增加或删除人的时候需要维护之外，在Network中增加边的时候也需要维护。这里我采用的方法是在Person当中增加groupid记录，即使用ArrayList存储该节点加入的组的编号。增加边的时候会检查两个节点中的公共组，直接进行valuesum的增加。（由于组数量至多为10，可以直接循环遍历groupid）

第三次作业

实现规格的设计策略

      第三次作业增加了Message的三个子类，也就是更丰富的信息类型，对应的也需要增加并维护Person的更多属性，以及实现Network中传递各类信息所要实现的功能。其中还增加了表情类Emoji，需要存储并记录其热度，对此也是直接使用HashMap实现。在数据规格上，与之前不同的是三个信息子类增加了不变式的约束，实现也十分简单。方法规格上，由于数据的增多，需要更仔细阅读ensures，准确、无遗漏地理解其要求。

性能考虑

      这次比较复杂的是求最短路径，采用了堆优化的dijsktra算法。算法中使用Pair类型打包节点id和距离distance，并使用了PriorityQueue实现小顶堆，优化对当前最短距离的查询。在算法当中本来是需要修改distance的值的，但是由于PriorityQueue不方便进行修改操作，采用的策略是直接存入一个新值。对同一个节点id而言，distance较小的总会先取出；为避免冗余的distance的影响，只需要每次取出是判断该节点是否已是最短路径即可（Hashset存储已完成的节点id）。

private int dijsktra(int start, int target) {
        PriorityQueue<Pair<Integer, Integer>> distance =
            new PriorityQueue<>(Comparator.comparingInt(Pair::getValue));//id--distance between start and id
        HashSet<Integer> flag = new HashSet<>();//id of those has found min distance
        distance.add(new Pair<Integer, Integer>(start, 0));

        Pair<Integer, Integer> head;
        while (true) {
            //get minfistance
            do {
                head = distance.poll();
            } while (flag.contains(head.getKey()));
            //judge finish
            if (head.getKey() == target) {
                return head.getValue();
            }
            //update
            for (Person person :
                    ((MyPerson) this.getPerson(head.getKey())).getAcquaintance().values()) {
                if (!flag.contains(person.getId())) {
                    distance.add(new Pair<>(person.getId(),
                            head.getValue() + person.queryValue(this.getPerson(head.getKey()))));
                }
            }
            //flag: this id finish
            flag.add(head.getKey());
        }
    }

三、基于JML规格的测试方法与策略

Junit

      通过在Junit中生成实例并输入数据测试，并利用断言实现与期望结果的比对。对于void类型的方法，需要调用其他方法来验证其准确性。这种测试方法的优势在于可以独立地进行模块测试，并且给不同人员（特别是非开发人员）测试提供了一个统一接口。不过实际上我并没有太多使用，因为感觉测试效率比较低。

评测机与对拍

      本单元的测试主要依靠测评机完成。在正确性测试上，可以基于规格的理解手动构造边界数据进行测试。大规模随机测试是由评测机进行，并重点测试上述提到的复杂方法。实际上由于本单元的要素不断变得复杂，对拍的效率更高。不过考虑到本单元涉及图的算法，可以使用python的networkx库进行无向图的建模，利用现成的函数获得连通性、最短路径、子图属性等。但其余功能的实现（比如信息传递等）很大程度上相当于再写一次作业。

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

HashMap

      本单元使用最多的容器就是HashMap，因为它拥有很高的查找效率。对于HashMap中的元素，主要需要实现（key的）hashcode和equals方法。HashMap中的value的修改比较简单，因为put方法中若对应的key中已有value，会直接覆盖。对于键值对的删除，推荐使用removeIf方法：

hashmap.entrySet().removeIf( Entry -> condition)

condition是要删除的键值对的条件，其实整体就是一个lambda表达式。当然也可以使用迭代器。

PriorityQueue

      优先队列PriorityQueue是一颗完全二叉树，在本单元中主要用于实现小顶堆。因为存在顺序先后的比较，因此一般需要自定义comparator接口中的compare方法：

PriorityQueue<Class> queue = new PriorityQueue<Class>(new Comparator<Class>(){
	@Override
	public int compare(Class o1, Class o2){
        //return > 0  o1优先级更高
        //return 0    优先级一样
        //return < 0  o2优先级更高
	}
})

也可以使用lambda表达式优化：

PriorityQueue<Class> queue = new PriorityQueue<Class>((Class o1, Class o2) -> o1.compareTo(o2))

      在写compare方法的时候，更建议返回1，0，-1，避免作差结果超过int的范围而产生bug。

      优先队列较常用的是poll，取出（获取并删除）第一个元素。

      当然本次作业还使用了ArrayList，主要实现的是顺序存储。由于使用频率较高，就不赘述了。

五、作业架构设计

      本单元作业的架构基本上是按照规格设计的，自己并没有过多额外设计。UML类图如下：

      本单元的模拟社交系统本质上是一个无向图模型，其中Person是节点，Network就是图。因此从图的建模来看，图的边信息是通过邻接表的形式存储的（即Person中的acquaintance属性），同时节点中还保存了许多如age、name、socialvalue等特征信息。由于社交系统还有发送信息、分组等功能，而这些事件会改变图的结构（比如socialvalue等），因此需要维护。本次作业中图的维护基本上都是事件响应机制，即调用Network的一些方法的时候，对节点信息进行维护。此外还有一些事件涉及图的度量信息，比如连通块、子图的特征（如agevar）等，这需要维护数据缓存（如并查集维护、Group里valuesum缓存）。

六、心得体会

      本单元主要提高了JML的阅读理解、并根据规格实现的能力。个人感觉JML确实很大程度上给予类型、方法更严格的描述，而在具体实现上又不作限制、十分自由。而基于JML的静态代码检查也一定程度上有助于保障代码的正确性。当然JML有时也没有自然语言描述直观，而且基于JML的自动化测试也有待发展。但是我认为这一单元的学习，让我们对如何严格描述代码功能、如何让别人快速理解我们的代码、如何证明程序的正确性有了更多的思考。