zoukankan      html  css  js  c++  java
  • BUAA_OO_2020_第三单元总结

    BUAA_OO_2020_第三单元总结 

    JML理论基础

    简介

    JML(Java Modeling Language)是一种用于对JAVA程序进行规格化设计的语言,其通过定义接口所包含方法的行为,来约束实现接口的类的行为。本章作业就是实现课程组提供的用规格定义好的接口,来学习如何根据规格写方法。

    JML表达式

    原子表达式

    关键字含义示例
    esult 定义返回值 esult == getPerson(id1).getAge()
    old(expr) expr在执行方法前的取值 groups.length == old(groups.length) + 1;
    ot_assigned(x) 括号中的变量是否倍赋值 forall int i; 0 <= i < groups.length; ot_assigned(groups[i])

    其中有一点容易混淆。old(group.length)代表的是group在执行方法前的长度。而old(group).length == group.length,指的是方法执行后的长度。这是由于在方法执行过程中,并没有改变group指向的对象,只是改变了其指向对象的值。

    量化表达式

    表达式含义示例
    forall 对于范围内的每个元素遍历 (forall int i; 0 <= i < groups.length; ot_assigned(groups[i]));
    exists 范围内存在一个元素满足后续条件 (exists int i; 0 <= i && i < groups.length; groups[i].getId() == id)
    sum 范围内满足条件的表达式的和 (sum int i; 0 <= i < people.length && people[i].getAge() >= l && people[i].getAge() <= r; 1)

    方法规格

    在此,以作业提供的接口方法规格为例,依次分析方法规格的组成部分。

    1 /*
    2  @ public normal_behavior
    3  @ requires contains(id);            //前置条件
    4  @ assignable 
    othing;              //副作用限定
    5  @ ensures (exists int i; 0 <= i && i < people.length && people[i].getId() ==    @id;money[i] == 
    esult);           //后置条件
    6  @ also  
    7  @ public exceptional_behavior       //异常行为
    8  @ signals (PersonIdNotFoundException e) !contains(id);
    9  @*/
    • 前置条件

      通过requires子句表示,要求确保其表达式为真才可进行正常行为操作。

    • 后置条件

      通过ensures子句表示,要求确保方法执行后其表达式为真

    • 副作用限定

      通过assignablemodifiable表示,限定方法能够修改的对象

    • 异常行为

      通过signals (ExceptionType e)为了提高程序鲁棒性,在不满足requires表达式时,需要进行其他异常行为操作(比如抛异常)。

    一般通过public normal_behaviorpublic exceptional_behavior来区分正常行为和异常行为,但是对于正常行为设计多种条件分支(if-else语句)时,也可以把每个正常/异常分支使用public xxx_behavior区分开,以提高可读性。(在本次作业提供的规格中多是这样,所以阅读规格时按照其分开,就可理清各种个各种if-else情况,方便输写)

    类型规格

    类型含义示例
    invariant 不变式,在可见状态下必须满足的条件 invariant seq_nodes != null
    constraint 状态变化约束,前序和当前状态之间关系的约束 constraint counter == old(counter)+1;

    工具链

    OpenJML

    检查JML语法。不支持高版本java,环境很难配。

    JMLUnitNG

    根据规格自动生成测试。环境很难配。

    Junit

    单元测试。根据规格自行构造测试,可以检查覆盖率,尽量保证覆盖率高(但不是全部覆盖就没bug)。

    由于OpenJML和JMLUnitNG功能有限,所以本单元中主要还是采用单元测试的方法。

    OpenJML验证

    整个src的检测结果:

    结果非常申必。

    调整后:

    发现以上的bug。

    有时候会冒出上百个warning。为了美观就不放了。

    JMLUnitNG测试

    以上为使用JMLUnitNG进行UserGroup类的测试。

    可以看到,其主要对于边界情况进行简单测试。

    我的架构设计

    第一次作业

    容器选择

    第一次作业要求比较简单,实现了官方提供的三个接口。为了使得访问更加方便,多使用HashMap作为容器。例如:在User类(实现Person接口)中,使用HashMap<id, value>来存储熟人和value值。

    并查集

    另外,针对isCircle方法,为了降低复杂度,选择并查集。在Network中,实现HashMap<id,father_id>存储每个用户和其祖先的id。在addPerson方法中,新增id对应的键值对,将father_id设为自己。在addRelation方法中,合并两个人的father_id。另实现find方法,路径压缩+返回祖先。在isCircle方法中,对两个id分别find出祖先,以判断二人是否连通。

    find方法进行路径压缩时,需要注意先将find其父节点的返回值保存,再替换和返回,及采用如下写法:

     
    1 private int find(int id) {
    2      if (father.get(id) == id) {
    3          return id;
    4      }
    5      int ans = find(father.get(id));
    6      father.replace(id, ans);
    7      return ans;
    8  }

    若使用如下的简写方法,会在成链情况&人多的时候出现栈溢出:

    1  private int find(int id) {
    2      if (father.get(id) == id) {
    3          return id;
    4      }
    5      father.replace(id, find(father.get(id)));
    6      return father.get(id);
    7  }

    第二次作业

    本次作业新增Group接口,在设计过程中需要注意其中方法的性能。如果直接找着JML写,会出现O(n^2)复杂度,而出现CTLE错误。因此,采用在向Group中加人的时候预处理relationSumvalueSumconflictSumageSumageVar(由于向Group中加人有指令条数限制)。预处理方法如下:

     
     1 public void addPerson(Person person) {
     2      // renew people
     3      people.put(person.getId(), person);
     4      // renew conflictSum
     5      conflictSum = conflictSum.xor(person.getCharacter());
     6      // renew ageSum
     7      ageSum = ageSum + person.getAge();
     8      int meanAge = getAgeMean();
     9      ageVar = 0;
    10      // renew relationSum
    11      // renew valueSum
    12      // renew ageVar
    13      for (Integer next : people.keySet()) {
    14          ageVar = ageVar +
    15              (people.get(next).getAge() - meanAge) * (people.get(next).getAge() - meanAge);
    16          if (people.get(next).isLinked(person)) {
    17              relationSum = relationSum + 2;
    18              valueSum = valueSum + (people.get(next).queryValue(person)) * 2;
    19          }
    20      }
    21      ageVar = ageVar / people.size();
    22      relationSum = relationSum - 1;
    23  }

    采用这种方法不要忘记,在addrelation的时候可能会造成relationSum、valueSum的变化,因此还需要新建方法如下:

    1  public void updateRelation(int value) {
    2       relationSum = relationSum + 2;
    3       valueSum = valueSum + 2 * value;
    4   }

    第三次作业

    本次作业难点在于最短路算法和点双连通分量算法。

    最短路

    最短路采用堆优化迪杰斯特拉算法,如果不堆优化可能会被卡。具体实现方法为,新建Pair类,包含属性id和dis(表示到起点的距离),并继承comparable接口,重写compareTo方法。

    1  @Override
    2  public int compareTo(Pair o) {
    3      if (dis > o.getDis()) {
    4          return 1;
    5      } else if (dis < o.getDis()) {
    6          return -1;
    7      }
    8      return 0;
    }

    点双连通分量

    由于对tarjan不熟悉,怕写bug,再加上时间足够,因此采用暴力方法。

    • 首先如果people.size == 2,一定不满足条件,直接return false。

    • 如果!isCircle(id1,id2),一定不满足条件,直接return false。

    • isLinked(id1, id2),则将两人分别从acquaitance中移除,及删掉两人之间的边,再dfs。若两人依然连通,则return true。否则return false。

    • !isLinked(id1, id2)针对所有出了起点、重点的人,将他们从图中删除(具体实现方法为,设置lock=id),然后dfs判断id1和id2的连通性。若一直连通,则return true。否则return false。

    还有一种常数优化,就是再遍历所有点的时候,如果该点和id1不isCircle,可以直接continue,不进行dfs,因为去掉其一定不会影响两点之间本来的连通性。

     

    关于测试和bug

    第一次

    第一次作业比较简单,在自己写代码的时候发现的bug就是find()方法栈溢出问题,已在架构设计中详述。

    互测和公测都没有出现bug,屋里十分安静。

    第二次

    第二次作业在自己测试中,一开始没有考虑到addRelation对Group类的relationSum、valueSum的影响,通过Junit单元测试发现。

    从本次作业开始采用对拍,不验证输出的正确性,而是横向比较多人的输出,若出现不同则有人有bug。

    在公测和互测中没有被发现bug。

    互测中,共hack到两个bug:

    • 一位同学在使用O(1)求ageVar的时候,采用如下写法:

      (ageSquaredSum - 2 * mean * ageSum) / people.size() + mean * mean;

      这种写法的错误在于,第一个因子的分子部分可以是负数,而java整除对于负数向上取整。用如下数据就可以hack:

       ag 1
       ap 1 1 1 4
       ap 2 1 1 5
       ap 3 1 1 6
       atg 1 1
       atg 2 1
       atg 3 1
       qgav 1
    • 一位同学由于时间复杂度高导致CTLE

    第三次作业

    第三次作业的易错点比较多,依然采用对拍,不验证输出的正确性,而是横向比较多人的输出,若出现不同则有人有bug。在本地测试时发现了一下易错问题:

    1. 针对qsl,只有两人的情况可能需要特判。

    1. 使用优先队列时,必须调用add方法才会更新排序,直接修改queue中元素时不会触发重新排序的。

    1. Group类中的ageVar会溢出int范围(但是由于java不是到什么神奇的机制,并不会出现错误),但是需要注意,如果多项式中某一项转long而某一项没转,可能会出问题。

    1. delPerson的时候可能需要考虑除0问题。

    在公测和互测中没有被发现bug。

    在互测中,发现了一下5个bug。

    1. delPerson的时候没有考虑除0。

    2. 采用静态数组,出现越界问题。

    3. 在delPerson的时候没有更新relationSum,valueSum

    4. 暴力求qsl写的有点过于暴力,导致CTLE

    5. qmp不完备,由对拍发现bug,由于可读性不太好,没有深究是什么问题。

    测试

    1. Junit单元测试,用于输写一些数据量较小的边界情况,尽量覆盖所有情况,测试基本功能。在此举例:

       1 @Test
       2  public void testQueryStrongLinked() throws Exception {
       3      //TODO: Test goes here...
       4      net.addPerson(new User(0, "a", new BigInteger("63"), 22));
       5      net.addPerson(new User(1, "a", new BigInteger("1"), 21));
       6      assertEquals(false,net.queryStrongLinked(0,1));
       7      net.addPerson(new User(2, "a", new BigInteger("1"), 21));
       8      // only two + not linked
       9      assertEquals(false,net.queryStrongLinked(0,1));
      10      net.addRelation(0,1,5);
      11      // only two + linked
      12      assertEquals(false,net.queryStrongLinked(0,1));
      13      net.addRelation(0,2,5);
      14      assertEquals(false,net.queryStrongLinked(0,1));
      15      // triangle
      16      net.addRelation(1,2,5);
      17      assertEquals(true,net.queryStrongLinked(0,1));
      18      net.addPerson(new User(3, "a", new BigInteger("63"), 22));
      19      net.addPerson(new User(4, "a", new BigInteger("1"), 21));
      20      net.addRelation(2,3,5);
      21      net.addRelation(3,4,5);
      22      net.addRelation(4,2,5);
      23      // eight
      24      assertEquals(false,net.queryStrongLinked(0,3));
      25      assertEquals(true,net.queryStrongLinked(3,4));
      26  }
      View Code
    2. 对拍。在提交之前,邀请一些好友参加对拍,自动生成数据,横向比对输出结果和运行时间。第二次作业帮助多人共de出2-3个bug,第三次帮助多人共de出>5个bug,效率还是蛮高的。但是,由于对拍数据量较小,对于一些小数据边界情况(比如qsl的仅两人)可能不太友好,所以充足的本地单元测试是必要的。

    感想

    由于本单元没有动手写JML规格,所以对于其输写过程还是比较陌生。

    在根据JML输写代码时,看懂JML和按照其写出满足要求的方法不难,但是很多时候需要意会其中的深意,并且考虑性能上的优化。例如,queryblocksum方法是在求连通分量的数量,如果分析出这点,通过动态维护blocksum或者根据并查集求都是很简便的,但如果完全仿照JML的写法,双重循环,会使得性能上有很大的损失。

    本单元印象最深的就是在理论课上老师提到,如果规格不够全面,没有考虑一些异常情况,一定要在实现时体现出来抛出的异常是由于规格,而不是自身实现的问题,不能把锅扣到自己头上,我觉得很有道理。

  • 相关阅读:
    JDK中Unsafe类详解
    JAVA并发理论与实践
    关于FastJSON
    指数退避算法
    MySQL多表关联查询效率高点还是多次单表查询效率高,为什么?
    App开放接口api安全性—Token签名sign的设计与实现
    使用Jmeter进行http接口性能测试
    短信验证登录实现流程
    使用 Postman 取得 Token 打另一隻 API
    SpringMVC拦截器HandlerInterceptor使用
  • 原文地址:https://www.cnblogs.com/CindyZhou/p/12917486.html
Copyright © 2011-2022 走看看