JML单元作业博客

17373492

作业详情：

1.1 梳理JML语言的理论基础

在JML的学习中我主要通过指导书和第一次作业中助教提供的链接学习，经过整理如下：

0. 前言

What JML?

JML语言本身多用在严谨的软件工程领域内，达到需求与规格描述的准确的目的。
JML引入了大量用于描述行为的结构，比如有 模型域、量词、断言可视范围、预处理、后处理、条件继承以及正常行为（与异常行为相对）规范等等。

Why JML?

使用JML来声明性地描述一个方法或类的预期行为可以显著提高整体的开发进程。把建模标记加入到你的Java程序代码中有以下好处：

1. 能够更为精确地描述这些代码是做什么的
2. 能够高效地发现和修正程序中的bug
3. 可以在应用程序升级时降低引入bug的机会
4. 可以提早发现客户代码对类的错误使用
5. 可以提供与应用程序代码完全一致的JML格式的文档

JML和Junit、JMLUintNG等测试模块有着密切的联系，这里引用zsa学长的讲解是：

JML的一大意义在于为Junit提供设计(，从而可以起到分离功能开发人员与测试人员的效果，估计表现在工程开发的顺序上)：

1. 充分完善需求
2. 根据需求产出设计规格(利用JML语言或自然语言等)
3. 工程实现阶段
   3.1. 功能模块的编写
   3.2. 测试模块的编写
4. 测试

从中我们可以清晰地看出JML语言在实际开发中的优势，因为在实际开发的过程中为了保证开发程序与功能的完备性与正确性，我们需要对工程进行充分地测试，而JML语言等规格描述语言就使得编写人员与测试人员能够分离地同步进行，一来效率上升，二来相互不影响。

此外，JML语言等规格设计语言对于程序的编写人员来说也是一大福音，因为规格描述可以讲工作任务甚至是责任划分到每个人的头上，不会出现因为甲乙双方的描述不清或语义模糊等人为情况导致最后功能上的缺陷，使得责任分担更加明确。

how JML?

• 思维上的转变：在JML的学习中，我们不是被压迫剥削的码农！而是咸鱼翻身的 产品经理，我们只管提要求，我需要你怎么做，做出来要怎么样！比如我需要你使用 高端大气上档次的PS，而不是 lowB的photoshop，最后给我做出一个 五彩斑斓的黑。因为我是产品经理，所以我其实什么都不会，所以我对中间怎么实现的过程完全不 care，我给你原来的模板，你给我修改后的产品就ok。
• 忘掉你的方法：比如电梯载人的问题，产品经理并不知道什么是容器，并不知道请求是如何被放进容器的，他只知道载人=请求被放在容器里面，所以我们在使用 JML 语言的时候，使用的应该是 pure 的方法，描述的结果是不对任何东西进行改动，比如有的人在描述中直接写了 HandleList.add(req) 这种语句，而这个语句是实现层面的语句，他不是 pure 的，这个语句如果被执行的话 HandleList 会发生改变，会增加一个元素，这不是我们希望的描述。正确的描述应该是这样的：

/*@
@......
@ensures (HandleList.size() == \old(HandleList.size()));
@ensures (HandleList.contains(req));

即载人后容纳的人数应该比原来多1，且新的请求在队列中。

1. 形式

JML存在于 Java 文档的注释中，所以完全不会对代码的编译和运行造成影响，具体表现形式主要是在注释中每行以 @ 开头的 JML 语法，如：

/* @
@ public normal_behavior
@ requires ! isEmpty();
@*/
Object pop() throws NoSuchElementException;

多行注释时用 /**/ 的形式，单行注释可以使用 //@ 的形式。

进行描述的都是表达式，即返回值是布尔型的值，一个很容易犯的错误是：将相等写成 = ，因为 JML 在运行前不进行语法检查，所以有时候比较难发现。

2. 作用域

JML 和 Java 一样有 private-、 protected-、 以及 package- 级别的作用域，作用与 Java 相同。通常我们使用的都是 public-。

3. 前置条件 (requires)

前置条件表示调用一个 方法前 必须满足的一些要求，即该 代码运行前 必须是符合要求的，合法的。如要在栈中要调用出栈函数，前提条件是 栈中有数 ，所以这里我们的前置条件是：requires !stack.isempty()。

4. 后置条件 (ensures)

后置条件表示调用一个 方法后 必须满足的一些要求，即代码运行后必须是符合我们所 期望的。比如在栈中要调用出栈函数，后置条件是 取得的数是原来的栈的最顶端的数 且 栈存储的数比原来少1 ，所以我们这里的后置条件是：

/*@
@......
@ensures \result == \old(stack.get(stack.size()-1));
@ensures stack.size() == \old(stack.size()-1);

5. 模型域 (model)

模型域类似于 行为规范中的成员变量，如：

//@ public model instance JMLObjectBag elementsInQueue;

创立了一个公开的类型为 JMLObjectBag 的，名称为 elementsInQueue 的模型实例。
三个需要注意的地方：

• instance 关键字告诉我们了：虽然这个模型是在接口中被定义出来的，但是 每个实现接口的类 都可以有一个 单独的、非静态的 模型域。
• 因为这个模型域也是 JML 中的用法，同样在注释中声明，所以还是和 Java 代码是无关的，即 真实运行的代码中不存在这个模型域，不能引用。
• 单独构建一个包在每次操作时进行检查会让人觉得效率低下，但是因为行为规范中 不涉及代码实现 ，所以行为规范只是在描述行为接口，规定使用接口的客户代码所能依赖的外部行为。而在代码实现部分可以使用任意 满足行为规范的 高效的数据结构。
• (续上条)虽然在定义行为规范的时候我们不考虑效率问题，但是如果开启 JML 中的断言选项的时候是要考虑的，所以开启断言检查会增加程序运行的压力。

样例：

/*@
@ public normal_behavior
@ requires ! isEmpty();
@ ensures
@ elementsInQueue.equals(((JMLObjectBag)
@ /old(elementsInQueue))
@ .remove(/result)) &&
@ /result.equals(/old(peek()));
@*/
Object pop() throws NoSuchElementException;

注：这里其实和我们前文所说的使用 pure 的方法并不那么矛盾，因为我们并没有对真正代码实现做任何非 pure 的改动，相反地，我们在行为规范中新建了模型来指导具体的代码实现

模型域的取值 (represents)

模型域毕竟是和真正的实现域(Java代码)是严格分开的，而JML中的前置条件、后置条件和不变量都是没有副作用的，所以当我们在模型域中需要用到判定什么变量的时候，可以采取 represents 语句来沟通模型域和实现域。
如： //@ private represents isMinimumHeap <- m_isMinHeap;
就是将实现域中的 m_isMinHeap 传递给了模型域中的 isMinHeap，这样一来，当我们每次需要在模型域中用到 isMinHeap 这个变量的时候，我们都会从实现域中的 m_isMinHeap 同步一下，获得真正的当前的变量然后再进行判断之类的操作。
再如：

/*@ private represents elementsInQueue
@ <- JMLObjectBag.convertFrom(
@ Arrays.asList(m_elements)
@ .subList(1, m_size + 1));
@*/

就是将模型域中的 elementsInQueue 和实现域中的 m_elements[1,m_size] 联系了起来，每当模型域中要用到 elementsInQueue 就会和 m_elements 同步。 JMLObjectBag.convertFrom 是转换类型的静态函数，他将传入的数组转换为 elementsInQueue 所需要的 JMLObjectBag。

6. 不变量 (invariant)

不变量是要求表达式在 可见状态下 表达式为真。可见状态描述的是 完整可见的状态，考虑他的对立面比较方便，不可见有点像 在变化中，不稳定 的意思，我们在对象变化的时候所捕捉的状态都是不稳定的，即这里的不可见的，现在我们再来理解就简单一些，下面的都是 可见状态：

1. 对象的有状态构造方法（用来初始化对象成员变量初值）的执行结束时刻
2. 在调用一个对象回收方法(finalize方法)来释放相关资源开始的时刻
3. 在调用对象o的非静态、有状态方法(non-helper)的开始和结束时刻
4. 在调用对象o对应的类或父类的静态、有状态方法的开始和结束时刻
5. 在未处于对象o的构造方法、回收方法、非静态方法被调用过程中的任意时刻
6. 在未处于对象o对应类或者父类的静态方法被调用过程中的任意时刻

样例：

//@ public instance invariant elementsInQueue != null;

这里表示我们生成的实例 elementsInQueue 在 可见状态下 不为null，其中最直接的影响就是上面可见状态的第一条：对象的有状态构造方法（用来初始化对象成员变量初值）的执行结束时刻不为null，所以构造的时候就要初始化为有意义的值。

7. 约束 (constrain)

主要用于描述delta，变化量的约束，如增删操作 Math.abs(a.length - \old(a.length)) <= 1

8. 运行时检查 (repOK)

上面所说的不变量和约束都是静态的限制，当我们自己在编写程序的时候我们就应该实现这种检查，具体来说就是使用 无参数的返回值为布尔类型的 repOk() 方法。
repOk 就是实现不变量的 JML 规格的方法，在每次执行函数前后调用，如果返回值为假的时候 要么抛出自定义的异常，要么返回错误的返回值给方法的调用者，告知这里的不变式约束出现了错误。

9. 量词 (Quantification)

这里量词的意思与逻辑学上的量词意思相近，而不是普通意义上理解的量词。如离散数学中的蕴含式 "==>" 是 JML 的一个量词，只有前件为真，后件为假的时候整个表达式才是假，其余都为真。
样例：

/* @
@ also
@ public normal_behavior
@ requires ! isEmpty();
@ ensures
@ (isMinimumHeap ==>
@ (/forall Object obj;
@ elementsInQueue.has(obj);
@ compareObjects(/result, obj)
@ <= 0)) &&
@ ((! isMinimumHeap) ==>
@ (/forall Object obj;
@ elementsInQueue.has(obj);
@ compareObjects(/result, obj)
@ >= 0));
@*/
public Object peek() throws NoSuchElementException

这是一个选取大顶堆或者小顶堆中优先级最高的数的方法，在

10. 副作用 (assignable)

在 assignable 后加变量表示这个函数的 副作用 ，即会对什么造成改变。
assignable 中持有两个关键字：/nothing & /everything，其中 /nothing 表示不会对任何进行修改，即纯方法，等同于在方法的可见范围后面加上 /*@ pure @*/；而 /everything 就表示可以修改一切内容。

纯方法

纯方法指不会改变任何变量的方法，所用的方法都是无副作用的 —— assignable \nothing

JML只对纯方法支持断言确认

为什么：因为如果对非纯方法支持了断言确认，非纯方法可能(一定)会导致内部发生变化，在某种特殊情况下，如果我们开启断言的时候方法能够正常运行，但是关闭断言之后方法不能按照期望输出，这是我们需要避免的，如很特殊的，我们在断言中读取一个数， assert((currentNumber = iterator.next())!=null) 然后再进行操作，我们关闭断言之后，实际上我们就没有进行读取 iterator.next() 的操作，可能 currentNumber 就一直是 null —— 则我们的断言改变了代码运行的状态，这是不可取的。

简化我们的后置语句

当我们害怕因为某些操作而导致一些特殊的变量发生改变，如在大顶堆的删除操作中无意间将大顶堆转换成了小顶堆：isMinHeap = !isMinHeap ，这会导致我们以后的操作出现问题，所以我们可能需要在后置条件中加上一句：isMinHeap = \old(isMinHeap)。要是一两个方法且少量的变量还好说，但是若方法增多，变量增多的时候，每个方法的后置语句都要加上长长的一串 variable = \old(variable) 吗？显然不太现实，所以我们要用到 assignable 语句，只标出需要修改的变量，因为通常在一个方法里，修改的变量比不修改的变量要少得多。
举个例子：

用后置语句
ensures
elementsInQueue.equals(((JMLObjectBag)
/old(elementsInQueue))
.remove(/result)) &&
/result.equals(/old(peek())) &&
isMinimumHeap == /old(isMinimumHeap) &&
comparator == /old(comparator);

用assignable语句
assignable elementsInQueue;
ensures
elementsInQueue.equals(((JMLObjectBag)
/old(elementsInQueue))
.remove(/result)) &&
/result.equals(/old(peek()));

修改规则

严谨来说，并不是只有在 assignable 中列出才可以修改，一个变量能被修改，至少满足下列五个条件之一：

• assignable 语句中显式列出这个变量。
• assignable 语句中列出的变量依赖于这个变量。
• 举刚才的模型域的例子，模型域的 isMinHeap 依赖于 m_isMinHeap，所以我们如果在 assignable 中列出了 isMinHeap ，那就隐式的表面了我们也可以修改 m_isMinHeap ，反过来想：否则 isMinHeap 如何被修改？
• 方法开始执行时这个变量尚没有分配。
• 这个变量是方法的局部变量。
• 这个变量是方法的形式参数。
• 传参进来的参数是形式参数，并不是实际参数，当然如果传的是引用就另当别论。修改形式参数不会对调用者的参数造成任何影响，所以是安全的。
• 但是有个例外，这里说的是改变方法的形式参数本身，而不能是改变 形式参数的内部成员变量，因为对内部的成员变量修改是对调用者有效的，会导致调用者的成员变量不安全，所以如果要修改参数的成员变量，务必要在 assignable 中明确指出，如：foo(Bar obj) 中 obj 的成员变量 x 要被修改，则 assignable obj.x

11. 异常行为 (exceptional_behavior)

上面我们讲的都是正常情况下对变量进行增删改查等操作，但是我们程序有时候会出现异常情况，甚至可能会抛出异常，这个时候我们就要区别于正常情况来定义我们的操作。
正常情况我们称之为：normal_behavior，通常写在方法的JML的第一句，与其可见范围写在一起，如 public normal_behavior。
如果我们有异常的行为，我们就要在正常行为讨论完之后另起炉灶，用一个 also 来引出更多的行为，而且每种新增的行为我们都要用一个 also 在前面修饰，表示更多的情况：

public normal_behavior
assignable balabala
requires balabala
ensures balabala
......also
public exceptional_behavior
balabala

异常行为的内容和正常的行为大致一致，都可以有 assignable ensures 之类的，但是异常行为当然还具有抛异常的功能，请看以下：

• signals (Exception e) (Expression)
• signals_only (Exception e)
  上面是两种JML中抛出异常的表示方法，其中第一种是当抛出的异常是 Exception 类型的时候，后面的表达式 Expression 要为真，即 (e instanceof Exception) -> (expr == true)；第二种是无条件抛出异常，没有前置条件，等价于 signals (Exception e) true

以上就是JML中的语法的大致内容。

1.2 梳理JML语言的应用工具链

在本单元中我们主要接触到了以下几个JML相关的工具：

1. OpenJML (对代码结合JML语言进行检查：包括JML语法静态检查，代码静态检查，运行时检查。)
2. JUnit4 (Java语言的单元测试框架，在极限编程和重构被极力推荐使用)
3. JMLUnitNG (以JML语言规格描述作为指导的自动生成单元测试工具)
   
4. SMT Solver (Satisfiability Modulo Theories)
   SMT是一款基于数理逻辑的用于自动化验证函数正确性的工具，其支持多平台的SMT解释器(SMT-Solver)，其中应用最广泛的平台之一是微软所研发的 z3，我们在实验中也使用的是 z3。
   

在我们的本单元实验中，由于 OpenJML 开发时的Java版本较低，只能用于简单的JML语句处理且对于 Intellij IDEA 的支持不是很好，所以主要还是用 JUnit 对自己的程序进行简单的单元测试。

2. 部署 SMT Solver(选做)

//TO-DO 在下面贴了几个链接，供大家参考

3. 部署 JMLUnit/JMLUnitNG，针对PathContainer生成样例

很遗憾，在多次尝试失败后决定放弃对目前相对复杂的Java程序的JML分析

C:\MyCode\OOCode\JMLCollection\Graph\MyPathContainer.java:77: 错误: 找不到符号
throw new PathNotFoundException(path);
^
符号: 类 PathNotFoundException
位置: 类 MyPathContainer
C:\MyCode\OOCode\JMLCollection\Graph\MyPathContainer.java:69: 错误: 找不到符号
@ signals (PathNotFoundException e) path == null;
^
符号: 类 PathNotFoundException
位置: 类 MyPathContainer
C:\MyCode\OOCode\JMLCollection\Graph\MyPathContainer.java:70: 错误: 找不到符号
@ signals (PathNotFoundException e) !path.isValid();
^
符号: 类 PathNotFoundException
位置: 类 MyPathContainer
C:\MyCode\OOCode\JMLCollection\Graph\MyPathContainer.java:71: 错误: 找不到符号
@ signals (PathNotFoundException e) !containsPath(path);
^
符号: 类 PathNotFoundException
位置: 类 MyPathContainer
C:\MyCode\OOCode\JMLCollection\Graph\MyPathContainer.java:91: 错误: 找不到符号
MyPath myPath = (MyPath) path;
^
符号: 类 MyPath
位置: 类 MyPathContainer
C:\MyCode\OOCode\JMLCollection\Graph\MyPathContainer.java:91: 错误: 找不到符号
MyPath myPath = (MyPath) path;
^
符号: 类 MyPath
位置: 类 MyPathContainer

但还是参照lzb的帖子配置运行简单的JMLUnitNG样例生成测试
简单的可能导致溢出的相减的函数：

$ cat demo\Demo.java
// demo/Demo.java
package demo;public class Demo {
/*@ public normal_behaviour
@ ensures \result == lhs - rhs;
*/
public static int compare(int lhs, int rhs) {
return lhs - rhs;
}public static void main(String[] args) {
compare(114514,1919810);
}
}

生成的测试覆盖很广泛，具体可以从运行情况中看出：

$ java -cp jmlunitng.jar demo.Demo_JML_Test
[TestNG] Running:
Command line suitePassed: racEnabled()
Passed: constructor Demo()
Passed: static compare(-2147483648, -2147483648)
Failed: static compare(0, -2147483648)
Failed: static compare(2147483647, -2147483648)
Passed: static compare(-2147483648, 0)
Passed: static compare(0, 0)
Passed: static compare(2147483647, 0)
Failed: static compare(-2147483648, 2147483647)
Passed: static compare(0, 2147483647)
Passed: static compare(2147483647, 2147483647)
Passed: static main(null)
Passed: static main({})===============================================
Command line suite
Total tests run: 13, Failures: 3, Skips: 0
===============================================

主要是对特殊情况进行测试，int型的边界情况，包括正边界与负边界的情况，还有0的情况，还有空的无效输入等情况，果不其然在边界情况下溢出了，没有得到我们预期的结果。

由此可以看出，如果在未来能应用到我们的地铁交通线路规划这种较大的小型工程的话，对于准确性的测试是非常有益的。

4. 按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构

Ctrl+C Ctrl+V一时爽，一直Ctrl+C Ctrl+V火葬场
上面这句话是我本单元作业的真实写照。
在本单元的前两次作业中，由于实现的功能特别简单，所以我直接复制粘贴整个 MyPathContainer 到了 MyGraph 中，用了很短的时间就完成了作业，并进行了充分的正确性测试。但是，在第三次作业的时候，需求的突然增多让我乱了阵脚，直接复制粘贴在 MyRailWayStation 中完成所有方法导致一个类十分臃肿，甚至在 checkStyle 时违反了类大小超过500行的设定，其耦合性与冗杂程度可见一斑。
其实我在第二次作业开始的时候，也思考过通过继承的方式来使代码变得好看，但是在此单元中继承最大的硬伤是子类不能继承父类的私有变量与方法，而在checkStyle中又明确了不能将变量设置为public，这导致我无从继承；在第三次作业中也设想用接口的方式简化，但是接口中都是抽象方法，是对几个不同类之间的抽象，所以还是用了单独的类 MyRailwayStation 解决问题。

在第九次作业，即本单元第一次作业中，只需要判断各点之间的连通性，所以有很多方法，我自己实现了 bfs 和 floyd 的方法，都能成功运行并通过测试点。

在第十次作业，即本单元第二次作业中，需要计算最短单源路径，鉴于图结构的改变操作只有20次，且节点的个数限制在120个，所以我使用的是有存储记忆的 floyd 一次遍历并缓存的方式，且用静态数组的方式加速了矩阵的计算存取速度，也很简单过了第二次作业。

在第十次作业，即本单元第二次作业中，我还是使用了floyd算法，但是的但是，我是基于拆点的网络流方式计算的，并没有采用wjy的不拆点算法，这也直接导致我第三次作业的严重翻车！！！！！。在本地测试的时候，用了随机数据生成的方式，虽然确实在运行的时间上比别人慢一截，但是自己本地只能测试实际运行时间，都是绰绰有余的，没有考察到自己的CPU时间，结果交上去之后只过了前三个数据点，后面17个数据点全部CTLE。怎么说呢，很后悔，也很无奈。

强烈建议在下一届开放CPU时间测试窗口

强烈建议在下一届开放CPU时间测试窗口

强烈建议在下一届开放CPU时间测试窗口

在哪里跌倒，就要在哪里爬起来吧，看到强测爆炸之后就开始着手重构，采用 spfa 算法优化。以下是我的三次作业以及重构的UML图，可以看出明显的差别：

第一二三次作业几乎是一样的：

------

第三次重构后的作业风格有了明显的差异：

重构发生的改变主要在于以下几个方面：

1. 分离存储与查询的部分，MyRailWayStation 只作为查询，具体的点的存储都在类 Graph 中
2. 类 Graph 进行抽象，将三种图归一到一种，具体的不同只有 line_weight 和 transfer_weight 的不同
3. 类之间为了避免冗余存储采用了共有 “节点和边的管理器” 的方式，即采用 单例模式 创建了唯一的储存管理边和节点的类 nodeContainer ，类 Graph 和 类 NodeContainer 之间的交互方式模仿了 生产者消费者模式下的 —— 每个都将自己私有的 NodeContainer 与单例的 NodeContainer 共享。
4. 采用了 spfa 算法加速，而不是 floyd 算法， floyd 算法最大的缺点在于 拆点的情况下 邻接矩阵异常大，虽然只有 120 个点，但是每个点都可以出现在不同的 Path 中，所以最后拆点后节点规模可以达到 4-5k 的量级 —— 这种情况下直接导致 O(n^3) 的时间复杂度爆炸。相反地，在 spfa 算法下，我们只访问每个点的邻接边的集合，并不断地松弛达到单源最短的目的。

5. 按照作业分析代码的bug

1. 第一次作业没有发现bug，在互测中也没有发现别人的bug，但是有的屋内的同学出现了罕见的bug —— 针对 HashCode 函数恶意哈希碰撞。如我们在映射 Path 到 PathId 的时候，很多人采用默认的 Arrays.hashCode()，而这个生成 HashCode 的方式是以 31 作为 hashSeed 迭代生成的，所以当遇到 4 0 和 3 31 的 path(es) 的时候，会产生相同的 hashCode，在 equals() 函数中没有严格的区别的情况下就会误判相同导致错误。
2. 第二次作业没有发现bug，在互测中也没有发现别人的bug，但是发现了在实现 floyd 或者 dij 的时候，邻接矩阵用 Array 的方式会导致效率急剧下跌，舍友的 cpu time 几近超时，特别危险，但是我采用的静态数组 int[][] 有着显著的优越性，cpu时间和实际时间都在10s内。
3. 第三次作业 “也没有发现bug”。为什么这样说呢，因为正确性是保证了的，通过大量的对拍和强测的数据都可以看出我的正确性，但是在效率上 略逊一筹，所以才会导致 ctle，这样看来，这一单元虽然看起来没有 性能分，但是实际上 性能分是100%。在别的屋内有现最短单源路径算法出错的，比如拆点的时候对于已经遍历过的点直接不再考虑，但是存在换乘的先后的情况，存在 之前遍历过但后续被松弛 的情况，这种情况下没有 二次松弛 导致出现错误。

6. 阐述对规格撰写和理解上的心得体会

刚接触JML语言的时候其实和大多数人一样内心是抗拒的，明明自然语言就足够能叙述清楚的事情，为什么要繁琐地重新设计一种语言去表述呢？甚至于第一次作业的时候我其实并没有细看规格，而是根据指导书的意思理解地去做，只是在处理异常的时候参考了JML语言而已。但是我还是强迫着自己去接受新的东西，去逼着自己读助教分享的四篇JML起步文章，并做笔记总结。

然而在第二次作业开始我就意识到错了。第一次作业因为内容本来就简单所以容易叙述清楚，但是第二次作业开始要判定最短路，还是在一条路径上有相同节点的最短路，甚至还会出现自环、闭环的最短路，这个时候自然语言所叙述出来的就不够严谨了，很多时候我都是对特殊情况无法理解，从而查看JML规格解释。

第三次作业，特别是重构的时候，自己已经逐渐形成了JML的这种语法习惯，我其实也特别诧异。具体表现在我之前对自己的函数做注解的时候都是英文表示，但重构时候发现通过JML的一些量词和谓词逻辑表示特别清爽简便，如下面：

//add Edge and save it in style of Pair<node1, node2>
// where node1.nodeId < node2.nodeId && node1.pathId == node2.pathId
//caution: single-direction

虽然说和真正的JML语言相比还差很多，但是已经有了思维惯性去这样表示，自己还是感到有点欣慰的。
在重构的时候，还用了老师上课推荐的对不变量和约束量的动态检查，即 repOK() 函数，搭配 assert 使用感觉确实可以对自己的每一步进行准确的保证，如下面：

private boolean repOk() {
for (int i = 0; i < startNode.size(); i++) {
if (startNode.get(i).getNodeId() != endNode.get(i).getNodeId()) {
return false;
}
}
if (!(startNode.size() == endNode.size())
&& (startNode.size() == midNode.size())) {
return false;
}
return true;
}

这个函数是用来保证我的源点和汇点在两个不同的 ArrayList<> 中 index 是始终保持一致的，这种一致性不能出错，所以是一个约束量，在每个函数的开头和返回的地方加上一句 assert repOk() ，方便简洁有力。

虽然结合 OpenJML 和 JMLUnitNG 只是简单的实现了一些功能，但是可以看出其潜在的功能之强大，若是未来能发展到支持 \exists 和 \for all 等复杂的谓词逻辑的话，相信一定对代码工程大有裨益。

Reference：

1. z3官方使用手册
2. Github JavaSMT - Unified Java API for SMT solvers.
3. 伦泽标[使用 JMLUnitNG 生成 TestNG 测试样例]
4. JMLUnitNG Offical Guide Book
5. Z3 SMTsolver 学习笔记（一） ——安装，环境配置篇
6. Z3 SMTsolver 学习笔记（二）——examples运行篇（未完成）
7. 用SMT solver验证程序等价