JML——BUAA_OO 第三单元总结

JML语言基础

JML简介

JML (Java Modeling Language) 是一种行为接口规范语言，可用于指定Java模块的行为(如契约式设计)。它有多种工具来进行断言检查、文档生成、单元测试、静态检查和验证等。

JML优点

能更加精确地描述代码所完成的任务
能有效地发现和纠正错误
能减少随着应用程序的进展而引入错误的机会
能产生始终与应用程序代码保持同步的精确文档

JML语法

原子表达式

esult: 表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
old(expr): 表示一个表达式expr在相应方法执行前的取值，该表达式涉及到评估expr中的对象是否发生变化。
如果是引用（如hashmap)，对象没改变，但进行了插入或删除操作。v和odd(v)也有相同的取值。
not_assigned(x,y,...): 用来表示括号中的变量是否在方法执行过程中被赋值。如果没有被赋值，返回为true ，否则返回 false 。用于后置条件的约束，限制一个方法的实现不能对列表中的变量进行赋值。

量化表达式

forall: 全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
exists: 存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
sum: 返回给定范围内的表达式的和。
product: 返回给定范围内的表达式的连乘结果。
min: 返回给定范围内的表达式的最小值。
max: 返回给定范围内的表达式的最大值。

方法规格

requires: 前置条件，要求调用者确保其后的条件为真
ensures：后置条件，对方法执行结果的限制，如果执行结果满足后置条件，则表示方法执行正确，否则执行错误。
assignable：副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。

类型规格

invariant: 不变式，要求在所有可见状态下都必须满足的特性。

其他

/*@pure@*/: 指不会对对象的状态进行任何改变，也不需要提供输入参数，这样的方法无需描述前置条件，也不会有任何副作用，且执行一定会正常结束。有些前置条件可以引用pure方法的返回结果。
public normal_behavior: 正常行为。
public exception_behavior: 异常行为。如果一个方法没有异常处理行为，则也不必区分正常行为。
signals (Exception e) b_expr: 强调满足某个条件抛出相应异常。当 b_expr 为 true 时，方法会抛出括号中给出的相应异常e。

JML应用工具链

部署SMT Solver

OpenJML

OpenJML下载地址：http://www.openjml.org/
下载完成后即可在IDEA中部署OpenJML，File->Settings->External Tools->+
相应参数如下

其中参数Name和Description任意填写，参数Program填java即可，参数Wording directory会自动生成不用理会,参数Arguments填写如下

其中-jar后面为openjml.jar的路径，-exec后面为z3-4.7.1.exe的路径

使用OpenJML验证
在命令行中输入java -jar C:Users20816Desktopopenjmlopenjml.jar -esc -prover cvc4 -exec C:Users20816DesktopopenjmlSolvers-windowscvc4-1.6.exe C:Users20816IdeaProjectsdemosrcMainClass.java

我们可以看到OpenJML给出了相关信息，给出了很多的溢出警告，可以帮助我们在书写JML或者实现规格的时候提供些许帮助。

部署JMLUnitNG

JMLUnitNG

下载地址http://insttech.secretninjaformalmethods.org/software/jmlunitng/
将jmlunitng.jar导入IDEA中
使用JMLUnitNG进行验证
请将所有java文件中的中文注释清除，将所有的ArrayList和HashMap等数据结构中的<>里的内容补全
在命令行中输入java -jar PATHjmlunitng-1_4.jar javaMyGraph.java javacomoocoursespecs2models*.java
成功之后我们可以得到一大堆的java测试文件，选择类名_JML_Test文件运行，在这里我们选择运行MyGroup_JML_Test，效果如下

我们可以看到JMLUnitNG为我们自动生成了测试样例并且进行了测试，测试结果可以给我们带来一些帮助。但是测试数据仅限于特殊、边缘数据，不具有代表性，想要进行全面的测试可能需要手动测试。

架构设计

作业1

整体框架大部分都已经由课程组构建好了，我们主要按照相应的JML规格实现NetWork和Person

UML类图：

复杂度分析：

从UML类图来分析，整体构造比较清晰简单，只需实现MyPerson和MyNetwork两个类。
从复杂度来分析，MyNetwork类复杂度明显较高，原因之一是功能比较多，导致相关函数比较多；另一个原因是有的函数比较复杂，其中最复杂的是isCircle，其功能就是判断两个节点是否连通（无向图），使用BFS或者DFS都可以实现，若想要进一步提升性能，可使用并查集来实现。整体来说，这次作业比较简单，目的是让我们对JML的语法和内容等有一个大概理解。

作业2

在作业1的基础上增加了Group接口，并扩充了原有功能

UML类图：

复杂度分析：

从UML类图来看，相较于第一次作业，虽然增加了一个接口，但是整体构造依旧很清晰，我们只需要实现Group接口，并且扩充原有功能。
从复杂度来分析，Runner和MyNetwork两个类的复杂度明显升高，其中Runner类为官方实现，所以不分析；MyNetwork类复杂度升高的原因是增加了与Group有关的功能。
值得注意的是，这次的作业对某些功能的性能有一定的要求，否则将会造成CPU超时。例如对于getAgeVar()函数，我们可以通过公式方差 = （年龄平方的和 - 2 * 平均年龄 * 年龄和 + n * 平均年龄的平方）/ n来实现，O(n)维护，O(1)查询，可避免CPU超时。

作业3

在作业2的基础上虽未增加新的接口，但是增加了很多的新功能

UML类图:

复杂度分析：

从类图来看，增加了一个Edge类，目的是实现Dijkstra算法，整体上看结构比较清晰。
从复杂度来看（不分析Runner，原因同上），MyNetwork类的复杂度相较于第二次作业翻了一番，可以说是极度臃肿了，原因是有很多复杂的图操作函数，其实我们完全可以将相关函数抽出来构成一个类，可以降低MyNetwork的复杂度，同时也可以让结构更加的清晰。

关于图操作函数的分析

queryMinPath()：这个函数的功能是若两个节点连通，则求出二者之间的最短加权路径。很明显，我们可以使用在数据结构课程中练习过的Dijkstra算法，时间复杂度为O(n*n)，大概率会被卡时间，所以需要进行堆优化，在java中PriorityQueue容器可以实现小顶堆，使用十分方便。经优化后的Dijkstra算法时间复杂度为O(nlogn)，几乎不会被卡时间。
queryBlockSum(): 这个函数的功能是求解图中连通块的数量。若按照规格中的双重遍历，一定会超时，所以需要用到并查集，维护复杂度O(n),查询复杂度O(1)，不会被卡时间。此外isCircle函数也可通过并查集来判断两个节点是否连通，大大降低了复杂度，可谓一石二鸟。
queryStronglink()：这是这次作业最复杂的函数，功能是判断两个节点之间是否有两条不同的路径，即双连通分量。实现方式主要有两种，第一种是非常NB的Tarjan算法，第二种是暴力做法，无限双重BFS。第一种实现方式网上比较多，所以这里着重介绍我所采用的第二种方法：
step1:第一重BFS
step2:若找到了两个节点间的一条路径，记录所经过结点；若未找到一条路径，则返回false
step3:去掉第一条路径所经过的点，进行第二重BFS
step4:找到了两个节点间的另外一条路径，则返回true；若未找到一条路径，则回到step1，继续搜索
这个算法复杂度和Tarjan相比肯定要大很多，但是课程组善良，不会被卡时间

Bug分析

自己的bug

本单元对时间复杂度有一定的要求，在强测和互测中我所有的bug都是由于某些函数的实现过于复杂从而出现CPU超时，例如在第三次作业中的queryMinPath()，在调用Dijkstra()前需要调用isCircle()函数，而isCircle函数使用了BFS，未采取直接查询并查集的方法，导致queryMinPath的复杂度为BFS的复杂度加上Dijkstra的复杂度，超出了限制，造成CPU超时。究其原因，首先是对算法复杂度没有一个正确的估计，总是一种差不多的感觉，然而当指令大幅度增加时，就变得差很多了；其次就是没能采取有效的手段构造与强测相似的边缘数据集，也没有计算自己的程序所花费的CPU时间，当然也就无法及时调整自己的算法，最终造成CPU超时。

他人的bug

对于他人的代码，我主要采用定点爆破加上广撒网双管齐下的方式进行hack。首先阅读他人的代码，若代码中有明显的错误或者算法复杂度过高，则直接采取定点爆破，直接构造针对性数据集进行hack；其次就是随机生成数据集进行多个程序间的对拍验证。
在互测中，我hack到的bug大部分都是CPU超时，原因自然是某些算法的复杂度过高。也有一部分的WA，例如实现queryAgeVar()时调用公式错误等。

心得体会

JML作为一种行为接口规范语言消除了自然语言的歧义，提供了一个统一的规范，对保证代码的正确性和结构的清晰性都具有强大的作用。通过书写JML时（虽然这不是考察点），我们可以描述方法预期的功能，无需考虑实现，这将延迟过程设想的面向对象原则扩展到了方法设计阶段。在阅读JML时，我们也不能为实现一个功能而只看相关的JML规格，我们应从整体来理解，眼光不能狭隘。
JML是对代码规格、行为进行了规范，但绝不是束缚住我们的手脚。不能死板地翻译JML，要从整体来理解；在满足规范的前提下，也可以对代码进行调整，例如可以增加某些类从而对代码进行解耦。
写代码无论如何是离不开算法的，在这一单元中，我们可能会用到并查集、Dijkstra、Tarjan、暴力枚举等，这无疑在学习OO时也学到了一些算法的知识。但同时我认为在第三次作业中对算法的要求有一些偏高，其实理解JML两次作业足矣。
算法的实现离不开数据结构。Java为我们提供了多种容器，HashMap、ArrayList等。对于查询操作较多的函数或者算法HashMap无疑是最好的选择,对于对象存储顺序有要求的函数或者算法ArrayList是一个很好的选择。不同的容器或者数据结构有不同的特点，如何正确使用这些容器也值得深入思考和探索。