【老物】BUAA_OO_2020_UNIT3

一、JML初探

JML(Java Modeling Language)作为一种形式化语言,可以约束Java代码中类和方法的状态和行为形成规格,通过将一系列具体代码实现抽象成明确的行为接口,可以形成一种契约式编程模式,JML设计者无需考虑实际的数据结构与算法,可以聚焦于程序的整体逻辑,JML形式化语言的无二义性能让实现者准确理解接口功能,根据问题需要选择合适的实现方式,同时JML可以帮助实现者开展代码测试与形式化验证,当然这时就要分析出模型语言映射到具体代码的抽象函数了。

JML表达式

JML可以内嵌在.java内,很方便,以**// @行注释或/* @ ... @ */**块注释,JML表达式支持Java表达式作为基础。针对更复杂的逻辑引入了量词表达式,\forall关键字类似数学中的,用法为\forall v; P(v); Q(v),等价于∀v(P(v) → Q(v))\exists关键字类似数学中的,用法为\exists v; P(v); Q(v),等价于∃v(P(v) ^ Q(v));这是在本单元比较常用的,当然还有\max, \sum, \min等实用的关键字。

​ 还可以使用特殊操作符==> <==>表示蕴含与等价关系,使用这种操作符可以增强JML的可读性,同时还有\nothing, \everything表示当前作用域下的空集全集

方法规格

​ 本单元我们聚焦于JML中的方法规格,方法规格针对类中各种方法(构造、修改、查询、生成)的返回值与行为进行约束,方法规格的三大关键是前置条件、后置条件、副作用范围。

​ 前置条件通过对参数施加约束,从而区分不同的处理操作,大体可分为normal_behaviorexpcetional_behavior,各有各的前置条件,从而通过JML可以直观看出何时需要对异常输入处理,何时是正常输入,当然二者的条件不能有交集。若输入均不满足前置条件,我们在实现中是没有理由进行处理的,因此方法的调用者为了保证结果的可控必须了解前置条件。对于前置条件,使用requires P;要求输入满足命题P

​ 后置条件对方法调用之后的对象状态与返回值约束,规定方法行为,使用关键字ensures规定后置条件,对于查询(query)方法,特别是只关心返回值不改变数据的方法,可以在访问修饰符后加上/*@pure@*/ 标记,对于返回值(\result)的表示,一般使用ensures P(\result);

​ 当然可能在查询中可能也会修改对象,比如惰式更新,修改方法(modify)也要修改对象,为了表示出修改与其范围,我们需要调用前的状态,ensures P针对的是调用后状态,\old(obj)关键字就可以看作对象/基本类型在方法调用前的快照。比如对于涉及容器的数据管理类,经常使用增删Add, Remove方法,\old就派上用场了,可以使用P(\old(obj)) ==> Q(obj)描述新的对象状态,当然这对对象的新状态是一种弱约束,比如不能保证Add后不会加入不期望的元素,可以在另一方向再加一个条件(constains(obj) && !isforadd(obj)) ==> \old(constains(obj))进行最小化,可见利用requires, ensures已经可以基本描述方法了

​ 还有一个方面就是副作用范围(side effect)了,我们可以列出本方法中可能修改的类中(静态)属性,对调用者而言,可以轻松get到是否会修改自己关心的敏感属性,通常使用assignable(modifiable)来列出可能修改的属性表assignable v1, v2, ...;,也可以使用JML中的全集,空集

​ 上面提到的expcetional_behavior是针对Java的异常特性的,使用signals关键字规范了异常的抛出时机与类型,用法为signals (<Exception Class> e) P;,等价于当P == truethrow异常,本单元对程序鲁棒性的考量也在此体现

类型规格

​ 类型规格就是对类中属性数据的约束,类似JavaJML可在变量名前加修饰符,non_null保证容器内无null,遵从这个规约可有效避免访问空引用,也有static, instance区分静态属性,当然JML想访问类中private属性时,相关属性可加/*@spec_public@*/,但我们的实现大可不必完全按规格来,规格描述也不该关心具体实现中的数据(这一点是在实验课中体会到的),本单元JML描述中容器都用数组表示,但我们只要符合规格的约束条件,可以选择更合适的数据结构。本单元代码中未涉及不变式invariant、状态变化约束constraint,这两个是比较强的约束条件,前者规定每次属性修改后的规约,后者表示属性修改相对于修改前状态的规约

​ 总之JML对代码实现者很实用,本单元写代码时官方JML已经给出了整体的结构与逻辑,JML中还有不少很实用的用法,值得日后深入学习一哈

关键字 作用
\not_assigned(x,y,...) 变量是否在方法执行过程中未被赋值
\not_modified(x,y,...) 变量在方法执行期间的取值是否未发生变化
\type(type) 返回类型type对应的类型
\typeof(expr) 返回expr对应的准确类型
\num_of 返回变量中满足相应条件的元素个数

二、JML之工具链

IDEA貌似没有插件式的JML工具,还是挺可惜的,JML官网有相关工具的介绍

OpenJML

OpenJML可用于JML的语法检查分析,下载解压到项目文件夹下运行

java -jar openjml.jar -exec Solvers-windows\z3-4.7.1.exe -esc com\oocourse\spec3\exceptions\*.java com\oocourse\spec3\main\*.java

​ 发现提示int#INT1不同啥的,是JML中三目运算符的解析好像有点问题,把Group接口中三目修改成

    /*@ ensures (\result == 0 && (people.length == 0) || (people.length != 0) && \result ==
      @          ((\sum int i; 0 <= i && i < people.length; people[i].getAge()) / people.length));
      @*/

JMLUnitNG

JMLUnitNG可基于JML对代码实现自动生成测试代码并开展测试,使用java -jar jmlunitng.jar 接口 源码生成了测试代码

img

​ 与同学交流貌似需要在JDK 8环境下才能运行,在IDEAProject Structrue -> Project Settings -> Project language level设置成8,运行一下针对Group接口的测试代码

imgimg

​ 可见JMLUnitNG是针对极端数据的,说好也是验证了程序的基本功能,说坏数据覆盖面并不广,对本单元作业的帮助有限。

其他

  • JMLEclipse:针对EclipseJML插件
  • JMLOK:介绍是说随机数据对JML实现的测试
  • AspectJML tool, JML4c:运行时规格验证

三、架构与Java性能提升

​ 本次作业要求是对社交关系网络的模拟,很显然是一种图论模型,Person接口作结点,Network作图,Group作子图,JML规格将层次描述的很清楚,强制Person管理边集,层次按图的层次就好,在hw9, 10我还专门引入了边类MyFriend,主要考虑到可能迭代会出现Person的子接口。而且针对hw10isCircle还保留了BFSDisjoint Sets两个版本的,主要考虑到最后可能会加入删边操作,并查集的删边操作至少也得是*O(V + E)*了,然而都并没有,whatever,本单元这一点相当友好~~,笔者终于不用重构了~~

​ 选用数据结构方面,考虑到id范围,类中容器全部选择以id为键值的Hashmap<>,当然用两个Hashmap<>建立起结点输入id到数组下标index的可逆函数 + 静态数组也很不错,为了可维护性选了前者

为什么要说"Java性能"

JML设计者只关心类可见的状态,并不关心具体实现的类内部状态,这也是同学们发挥的空间,但那种直接对着规格照葫芦画瓢的代码是很危险的,笔者仍然记得hw10用互测规模数据都可以把Group.getAgeVar朴素遍历卡到1e9级复杂度(运行分钟级),震惊了。反正适合实际问题的方法才是最好的!其次,Java还有c++这种面向对象语言,但凡涉及到字符串String,容器(container)之类的,抽象层次一高,就很难针对问题进行优化,导致执行效率低,反正很慢就是了,而且根据数据本单元T的还不少,所以提高性能很关键,这一部分围绕几个图架构下的关键矛盾方法开扯

连通块-isCircle & queryBlockSum

​ 前者查询是否为同一连通块内,后者查询连通块数,最优解为并查集(Union-find Sets),具体原理老生常谈了。isCircle()两次find操作,同时在图内维护连通块数k,增加结点addPersonk++,增加边addRelation时进行merge操作,若为不同连通块合并,k--,在i条指令下复杂度为*O(E + i)*

​ 当然hw10中的并查集有很大的隐患,递归形式的find操作在退化成单链的图中递归层数为*V*,笔者通过压力测试发现四千多层就爆栈了,StackOverFlow由递归层数,JVM设置的栈大小以及函数参数,局部变量大小决定,笔者决定稳他一手,将find路径上的结点暂存一下,找到父节点后统一设置父节点,就不递归了

​ 像开头说的,并查集如果面对删边deleteRelation很棘手,由于查并集路径压缩信息丢失,不能单纯的改父节点,我们需要遍历点集找到涉及的两个连通块的点集,再遍历一遍打上标记,删边,对于有标记的点展开BFS重新记录下父节点,O(V) / O(V + E),但如果deleteRelation有条数限制,那又是另一种权衡了

记忆化-Group接口

Group用于查询子图信息,为了提高效率维护内部属性,反正一堆东西在addPerson / delPerson时更新就好,平均值维护年龄和suma,方差维护年龄平方和suma^2,套公式(suma^2 + mean^2 * size - 2 * size * suma) / size特别地,子图内的增加边(ar)可以绕开Group,所以ar的时候得更新一下边的数据,没啥可操作的,但必须我们对变量的维护这个优化要符合JML(比如hw11再维护int suma^2就溢出了,一定得保证正常情况合法结果),对拍走起

点双连通分量-queryStrongLinked

​ 通读一下规格,查询两个结点是否在某个阶数大于2的环路上,在讨论区大手子指点下可以解读为两个结点是否在某个阶数大于2的点双连通分量上,学习了一下资料,点双连通分量竟然是tarjan?笔者只用过神奇的塔尖求过有向图的强连通分量啊...然后其实把求有向图的强连通分量的tarjanDFS树的出栈条件改一下就好了:递归遍历子节点后再出栈改成每个子节点递归后出栈。上张简单图(数字是DFS顺序,箭头是DFS大概的方向)

img

​ 可以看到我们2次回溯到1,根据塔尖的递归更新,2, 3 / 4,5low都会标记成1正好对应两个分量,但在求强连通分量时要等到1无子节点时再出栈;改改代码,每次回溯到根节点出栈就ok,当然注意不能出栈根节点,它可以处在多个分量中,并且注意特判阶数,O(V + E)

img

单源带权最短路-queryMinPath

​ 经典带权最短路,经典Dijkstra,堆优化后*O(Vlog(V))*

Java中想要搞一个小顶堆,PriorityQueue / TreeSet就够用,两者分别基于静态数组与红黑树,当然注意不能修改堆比较器中涉及的类属性,这将破坏堆维护的性质并导致意料之外的Bug,只能冗余加或先删除再添加,PriorityQueue就不要先删再加了,毕竟只能按引用查找遍历到下标再删,O(n),红黑树的增删都是*O(log(n))*

public boolean remove(Object o);
private int indexOf(Object o);

​ 为啥笔者还是TLE一个点,排查后原来是结点联结边集Hashmap<>(initalSize)初始化容量太大了,Hashmap迭代器遍历的核心函数为

final HashMap.Node<K, V> nextNode() {...
                if ((this.next = (this.current = e).next) == null && (t = HashMap.this.table) != null)
                    while(this.index < t.length && (this.next = t[this.index++]) == null);
...}

​ 可见要一次迭代器遍历要遍历哈希表到最后一个键值对,复杂度是容器的线性,所以说容量不能设太大,或者说这种无序型容器就不适合进行频繁的遍历操作,我们可以冗余存储一个顺序容器。当然对于qmp, qsl这种频繁访边点权的操作,建立起结点输入id到数组下标index的可逆函数 + 静态数组进行离散化就很香了,再把那个图中的边集直接一给MyNetwork管理,采用链式前向星,就纯数组,绕过低效的容器和对象,甚至可以搬自己的c代码了,起飞

次序,区间查询

queryAgeSum()单点更新,区间查询,教科书的树状数组queryNameRank在查询次数远大于节点数时可以二分下界查找,本次作业应该不太实用

四、Bug们和修复

JUnit单元测试

​ 这是一个可以快捷开展针对特定方法测试的框架,很实用,因为本单元我们要抓住关键矛盾~~,测试复杂方法就好了~~,用@Before标记可以在测试前初始化数据,用@Test开展一次测试,一般测一个函数就好了,Junit可以把不同测试的stdout分开,关于测试方式,我们往往要优化代码,所以我们可以在测试类中模拟这些方法的朴素版,比如Group的,然后随机构造数据,通过Junit的断言Assertion机制来验证一下优化版是否保证了正确性,当然可以调用c来对拍,Junit内嵌于Java相当灵活,还可以用于抛出异常的测试和运行时间的分析,是非常有用的Debug工具

自测 & 公测 Bugs

  • 首先是之前说的优先队列内元素不随意修改,笔者竟然没注意到Java只能传引用的特性;修复: 冗余加入的时候clone()一下
  • Group.getAgeVar没注意到size == 0的情况,divide by zerohw10强测翻皮水
  • 上文说了qmp在设置哈希表容量过大时不要迭代器遍历,TLE一个点

五、规格设计心得体会

JML作为一种形式化语言,表意很准确,我觉得结合接口API文档使用也就更直观了,本单元作业没有涉及不变式跟继承关系下的规格啥的。但其实主要让笔者体会到了规格设计中的契约式编程方法,设计者和实现者分离,我们在作业中扮演的实现者就是要在JML规格之下考量可维护性,执行效率,可读性,采用最合适的。这是一种高效的开发模式,对我们在团队项目、工作中很有用处