OO第三单元——很缺钱的社交网络

一、JML理论基础和工具链

基于规格的设计可以使开发人员能高效准确地完成开发，也能够使代码测试变得十分的轻松。

1.1 原子表达式

• esult：方法的返回值
• old(expr)：expr在方法执行前的取值
• ot_assigned(x,y,...)：当括号中所有变量均没有被赋值，返回true，否则返回false
• ot_modified(x,y,...)：当括号中所有变量取值均没有变化，返回true，否则返回false
• onnullelements(container)：容器中不含有null元素
• ype(x)：返回x的类型(Class)
• ypeof(expr)：返回表达式对应的准确类型

1.2 量化表达式

• forall：全称量词。用法为(forall Type x,y,...; P(x,y,...); Q(x,y,...))意思为对于任意的x，y，...，如果满足P(x,y,...)，则Q(x,y,...)为真。
• exists：存在量词。用法与forall类似。
• sum：求和。用法为(sum Type x,y,...; P(x,y,...); Q(x,y,...))，返回所有满足P(x,y,...)的x，y，...代入Q(x,y,...)计算得到的值的总和。
• product：求积。用法与sum类似，只不过求的是连乘的结果。
• max：求最大值。用法为(max Type x,y,...; P(x,y,...); Q(x,y,...))，返回所有满足P(x,y,...)的x，y，...代入Q(x,y,...)计算得到的值中最大的值。
• min：求最小值。用法与max类似。
• um_of：求满足条件的次数。用法为(max Type x,y,...; P(x,y,...); Q(x,y,...))，返回所有满足P(x,y,...)的x，y，...代入Q(x,y,...)也满足的次数。相当于(sum Type x,y,...; P(x,y,...) && Q(x,y,...); 1)。

1.3 集合表达式

一般形式为new ST {T x|R(x)&&P(x)}，其中的R(x)对应集合中x的范围，P(x)对应x取值的约束。

1.4 操作符

• 子类型关系操作符<:：如果A是B的子类型，则A<:B结果为true，否则为false
• 等价关系操作符<==>：说明两边的布尔表达式结果相同。否定为<=!=>。
• 推理操作符==>/<==：如果箭尾的表达式成立，则箭头的表达式一定成立。
• 变量引用操作符： othing表示空集，everything表示全集。

1.5 方法的规格

方法的规格有三种

• 前置条件：表示方法执行前需要满足的条件，由requires子句表示。
• 副作用：表示方法执行后会对对象造成哪些方面的改变，由assignable子句表示。如果不会对成员变量造成任何改变，则可用assignable othing表示，此时该方法可以标记为pure，后续规格中可以直接使用该方法。
• 后置条件：表示方法执行完之后需要满足的条件，比如返回值的限定，类成员变量要满足的关系等，由ensure子句表示。

方法的行为可以分为两种

• 正常行为：public normal_behavior，指在正常情况下的行为，最终完全执行整个方法并返回。
• 异常行为：public exceptional_behavior ，指遇到异常情况下，方法无法正常执行并向外抛出异常的行为。

如果一个方法中有多种行为，可以用also来连接。子类重写的方法的规格也可以用also来连接。

抛出异常的方法

• signals子句：用来抛出异常。用法为signals (xxxException e) b_expr;
• signals_only子句：只要满足前置条件就抛出相应异常。用法为signals_only xxxException;，等价于signals (xxxException e) true;

1.6 类型规格

• 不变式invariant：在所有可见状态下都必须满足的特性。
• 状态变化约束constraint：在变化前后要满足的约束。

1.7 jml工具链

关于下文的openjml和JMLUnitNG这两个工具我均没有在代码作业中使用。我也没有用过其他的jml工具链。

二、SMT Solver验证

费尽九牛二虎之力终于配置好openjml，然后对Person.java魔改一番，测试结果如下。

D:openjml>openjml Person.java
请按任意键继续. . .

D:openjml>openjml -esc -prove Person.java
Person.java:7: 警告: The prover cannot establish an assertion (NullField) in method Person
      @ public instance model non_null String name;
                                              ^
Person.java:8: 警告: The prover cannot establish an assertion (NullField) in method Person
      @ public instance model non_null BigInteger character;
                                                  ^
Person.java:10: 警告: The prover cannot establish an assertion (NullField) in method Person
      @ public instance model non_null Person[] acquaintance;
                                                ^
Person.java:11: 警告: The prover cannot establish an assertion (NullField) in method Person
      @ public instance model non_null int[] value;
                                             ^
Person.java:103: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: Person.java:99: 注: ) in method compareTo
        return this.getName().compareTo(p2.getName());
                           ^
Person.java:99: 警告: Associated declaration: Person.java:103: 注:
      @ public normal_behavior
               ^
Person.java:103: 警告: The prover cannot establish an assertion (Postcondition: Person.java:100: 注: ) in method compareTo
        return this.getName().compareTo(p2.getName());
        ^
Person.java:100: 警告: Associated declaration: Person.java:103: 注:
      @ ensures 
esult == name.compareTo(p2.getName());
        ^
Person.java:63: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: Person.java:52: 注: ) in method equals
        return obj instanceof Person && this.getId() == ((Person) obj).getId();
                                                                            ^
Person.java:52: 警告: Associated declaration: Person.java:63: 注:
      @ public normal_behavior
               ^
Person.java:63: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: D:openjmlopenjml.jar(specs/java/lang/Object.jml):76: 注: ) in method equals
        return obj instanceof Person && this.getId() == ((Person) obj).getId();
                                                                            ^
D:openjmlopenjml.jar(specs/java/lang/Object.jml):76: 警告: Associated declaration: Person.java:63: 注:
      @   public normal_behavior
                 ^
Person.java:111: 警告: The prover cannot establish an assertion (Postcondition: Person.java:110: 注: ) in method getAcquaintance
        return null;//pvalue;
        ^
Person.java:110: 警告: Associated declaration: Person.java:111: 注:
    public HashMap<Person, Integer> getAcquaintance() {
                                    ^
Person.java:95: 警告: The prover cannot establish an assertion (Postcondition: Person.java:92: 注: ) in method getAcquaintanceSum
        return pacquaintance.length;
        ^
Person.java:92: 警告: Associated declaration: Person.java:95: 注:
    //@ ensures 
esult == acquaintance.length;
        ^
Person.java:48: 警告: The prover cannot establish an assertion (Postcondition: Person.java:46: 注: ) in method getAge
        return page;
        ^
Person.java:46: 警告: Associated declaration: Person.java:48: 注:
    //@ ensures 
esult == age;
        ^
Person.java:43: 警告: The prover cannot establish an assertion (Postcondition: Person.java:41: 注: ) in method getCharacter
        return pcharacter;
        ^
Person.java:41: 警告: Associated declaration: Person.java:43: 注:
    //@ ensures 
esult.equals(character);
        ^
Person.java:33: 警告: The prover cannot establish an assertion (Postcondition: Person.java:31: 注: ) in method getId
        return this.pid;
        ^
Person.java:31: 警告: Associated declaration: Person.java:33: 注:
    //@ ensures 
esult == id;
        ^
Person.java:38: 警告: The prover cannot establish an assertion (Postcondition: Person.java:36: 注: ) in method getName
        return pname;
        ^
Person.java:36: 警告: Associated declaration: Person.java:38: 注:
    //@ ensures 
esult.equals(name);
        ^
Person.java:72: 警告: The prover cannot establish an assertion (Postcondition: Person.java:68: 注: ) in method isLinked
        return person.getId() == this.getId();// || pvalue.containsKey(person);
        ^
Person.java:68: 警告: Associated declaration: Person.java:72: 注:
      @ ensures 
esult == (exists int i; 0 <= i && i < acquaintance.length;
        ^
Person.java:72: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: Person.java:66: 注: ) in method isLinked
        return person.getId() == this.getId();// || pvalue.containsKey(person);
                                           ^
Person.java:66: 警告: Associated declaration: Person.java:72: 注:
    /*@ public normal_behavior
               ^
Person.java:89: 警告: The prover cannot establish an assertion (Postcondition: Person.java:79: 注: ) in method queryValue
        return 0;
        ^
Person.java:79: 警告: Associated declaration: Person.java:89: 注:
      @ ensures (exists int i; 0 <= i && i < acquaintance.length;
        ^
30 个警告

弹出来一堆莫名的警告。似乎openjml支持能测的范围很小啊。

三、JMLUnitNG自动生成测试样例

这个工具也把我整的够呛。网上相关的教程也不多。搞了很久Group没有跑通，只跑通了阉割版Person。

[TestNG] Running:
  Command line suite

Passed: racEnabled()
Failed: constructor Person(-2147483648, null, null, -2147483648)
Failed: constructor Person(0, null, null, -2147483648)
Failed: constructor Person(2147483647, null, null, -2147483648)
Failed: constructor Person(-2147483648, , null, -2147483648)
Failed: constructor Person(0, , null, -2147483648)
Failed: constructor Person(2147483647, , null, -2147483648)
Failed: constructor Person(-2147483648, null, null, 0)
Failed: constructor Person(0, null, null, 0)
Failed: constructor Person(2147483647, null, null, 0)
Failed: constructor Person(-2147483648, , null, 0)
Failed: constructor Person(0, , null, 0)
Failed: constructor Person(2147483647, , null, 0)
Failed: constructor Person(-2147483648, null, null, 2147483647)
Failed: constructor Person(0, null, null, 2147483647)
Failed: constructor Person(2147483647, null, null, 2147483647)
Failed: constructor Person(-2147483648, , null, 2147483647)
Failed: constructor Person(0, , null, 2147483647)
Failed: constructor Person(2147483647, , null, 2147483647)
Skipped: <<null>>.addAcquaintance(null, -2147483648)
Skipped: <<null>>.addAcquaintance(null, 0)
Skipped: <<null>>.addAcquaintance(null, 2147483647)
Skipped: <<null>>.compareTo(null)
Skipped: <<null>>.equals(null)
Skipped: <<null>>.equals(java.lang.Object@4fccd51b)
Skipped: <<null>>.getAcquaintanceSum()
Skipped: <<null>>.getAcquaintance()
Skipped: <<null>>.getAge()
Skipped: <<null>>.getCharacter()
Skipped: <<null>>.getId()
Skipped: <<null>>.getName()
Skipped: <<null>>.hashCode()
Skipped: <<null>>.isLinked(null)
Skipped: <<null>>.queryValue(null)
test
Passed: static main(null)
test
Passed: static main({})

===============================================
Command line suite
Total tests run: 36, Failures: 18, Skips: 15
===============================================

从测试数据上看，似乎只会使用一些极端数据来进行测试。跟我想象中的测试用例差远了。而且并没有常规情况下的测试样例。

四、架构设计梳理

三次作业整体的架构没有变，都是直接照搬接口，而且每个方法实现起来也比较简单，所以也就只有那三个类了。最后一次作业因为tarjan实现起来相对复杂一些，而且需要额外的临时空间，所以多了一个Tarjan类来处理。后来反思一下，觉得我应该也为并查集和最短路这些图的算法抽出一个类，这样的话可以对具体算法解耦合，Network的功能也更加专一。

第九次作业

• 类图

  

  这次作业架构也比较简单。让我难受的是找不到比较好的办法来让MyNetwork和SocialPerson脱耦。

• 方法复杂度

  Method	ev(G)	iv(G)	LOC
  MyNetwork.addRelation(int,int,int)	4	3	22
  MyNetwork.queryNameRank(int)	2	2	13
  MyNetwork.queryValue(int,int)	3	1	13

  两个类也就只有三个方法超过了10行，说明没有十分累赘的方法。

• 类复杂度

  Class	CSA	CSO	LOC	OCavg	WMC
  MyNetwork	2	38	121	2.14	30
  SocialPerson	5	34	61	1	12

  从这次作业也看不出来哪里存在较大问题。

• 实现细节

  这次虽然规格用的是数组表示，但是我还是用的是HashMap，因为里面涉及到大量的查找工作，使用HashMap比使用ArrayList性能要好很多。

  对于isCircle方法，我一下子就想到用并查集。并查集不仅性能比较高，而且还比bfs和dfs更好写，为什么不用呢？不过并查集在出现绝交(delRelation)的情况就要出问题了。所以我做好了只用一次的心理准备。没想到三次都能用

  还有一个queryName方法，逐个遍历给了我一个很低效的印象（虽然我之后也是这么做的）。有种想用TreeMap来存的冲动。

第十次作业

• 类图

  

  这次MyNetwork不仅跟SocialPerson耦合了，还跟MyGroup耦合了。我更难受了。

• 方法复杂度

  Method	ev(G)	iv(G)	LOC	v(G)
  MyNetwork.addRelation(int,int,int)	4	5	29	8
  MyNetwork.addtoGroup(int,int)	4	1	19	4
  MyNetwork.getRoot(Person)	2	4	19	5
  MyGroup.toString()	1	5	17	5
  MyGroup.addPerson(Person)	1	3	15	3
  MyNetwork.queryNameRank(int)	2	2	13	4
  MyNetwork.queryValue(int,int)	3	1	13	4

  前两个方法ev(G)达到4是因为异常情况太多了。

  getRoot超过了10行是因为实现了非递归式。

  toString用于debug。

  总的来说，方法的复杂度还能接受。

• 类复杂度

  Class	CSA	CSO	LOC	OCavg	WMC
  MyNetwork	5	59	213	2	50
  MyGroup	7	33	93	1.67	20
  SocialPerson	5	34	61	1	12

  从表中可以看出来，MyNetwork已经变得很臃肿了，应该对其进行拆解。

• 具体实现

  这次作业增加了组的要求，但是实现起来都比较简单。

  关于组的一些查询，我采用了冗余存储的办法，每次组内发生改变的时候，更新这些量。这样可以做到单次查询的时间复杂度为O(1)。这一过程是必要的，不这样做的话会导致TLE。

  这次幸好queryName限制了次数，否则这个O(n)的方法也要改造一下了。

  在MyNetwork中存储组的时候，为了降低耦合，我又存储了每个组的大小，在询问组大小的时候就不用依赖于组了。

  这次我还记录了每个人所在的组别，在加关系的时候能够方便地对相应组别进行更新。

第十一次作业

• 类图

  

  从类图中可以看出来，我分离出来一个Tarjan类，实际上还应该分离出来更多的类，让MyNetwork不再臃肿。

• 方法复杂度

  Method	ev(G)	iv(G)	LOC	v(G)
  Tarjan.dfs(SocialPerson,SocialPerson)	9	8	42	12
  MyNetwork.addRelation(int,int,int)	4	6	34	9
  MyNetwork.getDistance(Person,Person)	6	3	24	6
  MyGroup.toString()	1	6	22	6
  MyNetwork.getRoot(Person)	2	3	19	4
  MyGroup.delPerson(Person)	2	3	18	4
  MyNetwork.addtoGroup(int,int)	3	1	16	3
  MyGroup.addPerson(Person)	1	3	15	3
  MyNetworkTest.setUp()	1	2	14	2
  MyNetwork.delFromGroup(int,int)	2	1	13	2
  MyNetwork.queryNameRank(int)	2	2	13	4
  MyNetwork.borrowFrom(int,int,int)	3	2	12	4
  MyNetwork.queryAgeSum(int,int)	1	2	12	4
  MyNetwork.queryStrongLinked(int,int)	3	1	12	3
  MyNetwork.addPerson(Person)	2	1	10	2
  MyNetwork.queryValue(int,int)	2	1	10	2

  dfs需要40+行，这个没有办法。

  addRelation要维护的东西越来越多了。

  getBistance实际上就是Dijkstar算法，所以也有一定的篇幅。

  剩下的都还能接受。

• 类复杂度

  Class	CSA	CSO	OCavg	LOC	WMC
  MyNetwork	7	76	2.03	316	71
  MyGroup	7	35	1.92	116	25
  SocialPerson	5	36	1.07	67	15
  Tarjan	6	14	6.5	59	13

  MyNetwork的臃肿不想再说了。应该把一些图论相关的抽离出来。估计如果Tarjan不抽离的话会更加难受。

• 具体实现

  在了解了HashMap的各种遍历方法之后，我将所有keySet换成了entrySet，遍历性能应该有很好的提升。

  幸好这次删除的是组里的人，并查集保住了。

  钱的存储我放在了Network里面，因为我没有在Person里面找到跟钱有关的方法，所以只能这样解耦了。

  关于查询块数量，得益于之前实现的并查集。只需要维护一个新的变量，每次加点的时候相当于块数量加一，加关系的时候判断是否合并了两个连通块，是的话块数量减一就行了。

  关于最短路，用了堆优化 dijkstra 算法。单次询问O(nlogn)妥妥的。

  关于询问是否存在两条不相交路径，用了奇怪的Tarjan算法。别人存的是边，我存的是点。我以第一个点为dfs树的根，检查到第二个点出栈的时候，只需要判断当前遍历到的点是不是根即可。这样就可以不用遍历所有的结点了。当然，首先还是判断两个点是否可达，不可达后面就不用dfs了。

  关于年龄区间人数询问，第一反应是树状数组，不过因为实现相对复杂，遂放弃。

五、Bug与测试

三次作业强测均是满分，互测安全通过。说明充分的测试才能有好的结果。

跟前两个单元的作业不同，本单元作业的输出与输入一一对应，所以测试使用的是对拍器。

Junit如果使用得很好，确实能够保证很高的覆盖度。但是Junit宛如自己出题给自己做然后自己改，这样的话万一自己的想法本来就有偏差就测不出来了。而且Junit需要人去写测试样例，还有考虑指令的各种组合，很容易就漏掉情况。另外，由于本次作业结构简单，而且每次询问只会调用一个主要方法，得到的结果立刻转化为输出，所以对拍器就相当于单元测试了。大数据量覆盖面是有保证的，可以帮你找到绝大多数的bug。(当然tle是找不出来的)

在互测中，

第九次作业未能找到他人的bug。(断刀了)

第十次作业发现3人有bug。

• 没有冗余存储，每次询问使用二层循环求关系和关系值的和，于是造了两个数据hack他，让他tle。

• queryCircle过于暴力，于是也hack了一个tle。

• 认为一个人只能在一个组。这个错误我也犯过，不过在测试当中找出来了。

第十一次作业仅发现1人的bug，就是没有判断除0。错过了两个人的bug，都是算法过于暴力导致。原因是这一次互测我没有好好地读代码，写极端数据，以为不会有tle的情况。看来每次的极端数据制造都不能少。

六、心得与体会

这个单元的作业相对之前的作业来说简单了很多，不需要自己设计架构，只需要自己填空就行了。也就只有一些算法比较难一点。听说不少的人翻了车，我认为还是测试没有做到位。俗话说：浅水浸死人。即使简单，也要进行充分的测试，才能有无惧翻车的底气。

这个单元学习了JML。个人认为JML虽然确实能够很清晰地描述行为，但是对于一些方法有篇幅过长的情况，表达效果甚至不如自然语言。而且，设计JML也是一个痛苦的过程。所以，形式化还有很长一段路要走。

关于JML工具链，感觉相当鸡肋啊。openjml配置了相当长的时间，终于跑通了，但是只能测一些最简单直接的方法，而且还经常报错。JMLUnitNG只能生成一些边界数据，而且很多情况下这些边界数据都不会出现。对于组合出现的bug则无法测试。总的来说，体验极差而且没有什么用。JML工具链还需要慢慢发展才行啊。

虽然说这个单元成绩不错，但是我对JML没有太多的好感，而且没有很好地引导我们用合理的架构。希望下一个单元有更好的游戏体验。