BUAA_OO_第三单元

1、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_behavior，expcetional_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 == true时throw异常，本单元对程序鲁棒性的考量也在此体现

类型规格

​ 类型规格就是对类中属性数据的约束，相似Java，JML可在变量名前加修饰符，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	返回变量中知足相应条件的元素个数

2、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 接口 源码生成了测试代码

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

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

其余

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

3、架构与Java性能提高

​ 本次做业要求是对社交关系网络的模拟，很显然是一种图论模型，Person接口做结点，Network做图，Group做子图，JML规格将层次描述的很清楚，强制Person管理边集，层次按图的层次就好，在hw9, 10我还专门引入了边类MyFriend，主要考虑到可能迭代会出现Person的子接口。并且针对hw10的isCircle还保留了BFS和Disjoint 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，增长结点addPerson时k++，增长边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？笔者只用过神奇的塔尖求过有向图的强连通份量啊...而后其实把求有向图的强连通份量的tarjan的DFS树的出栈条件改一下就行了：递归遍历子节点后再出栈改为每一个子节点递归后出栈。上张简单图（数字是DFS顺序，箭头是DFS大概的方向）

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

单源带权最短路-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在查询次数远大于节点数时能够二分下界查找，本次做业应该不太实用

4、Bug们和修复

JUnit单元测试

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

自测 & 公测 Bugs

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

5、规格设计心得体会

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