一、JML语言理论基础、应用工具链
1.理论基础
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。BISL提供了对该法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。JML主要由Leavens教授在Larch上的工作，并融入了BetrandMeyer， John Guttag等人关于Design by Contract的研究成果。近年来，JML持续受到关注，为严格的程序设计提供了一套行之有效的方法。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具静态方式来检查代码实现对规格的满足情况。
一般而言，JML有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
2.表达式
1）原子表达式
\result表达式：表示一个非 void 类型的方法执行所获得的结果。\result表达式的类型就是方法声明中定义的返回值类型。
\old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。针对一个对象引用而言，只能判断引用本身是否发生变化，而不能判断引用所指向的对象实体内容是否发生变化。
\not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。如果没有被赋值，返回为true ，否则返回 false 。
\not_modified(x,y,...)表达式：限制括号中的变量在方法执行期间的取值未发生变化。
\nonnullelements( container )表达式：表示 container 对象中存储的对象不会有 null 。
2）量化表达式
\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
\sum表达式：返回给定范围内的表达式的和。
\max表达式：返回给定范围内的表达式的最大值。
\num_of表达式：返回指定变量中满足相应条件的取值个数。
3）集合表达式
集合构造表达式：可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素，一般形式为：new ST {T x|R(x)&&P(x)}，其中的R(x)对应集合中x的范围，P(x)对应x取值的约束。
4）操作符
子类型关系操作符： E1<:E2 ，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。
等价关系操作符： b_expr1<==>b_expr2 或者 b_expr1<=!=>b_expr2 。 <==> 比 == 的优先级要低。
推理操作符： b_expr1==>b_expr2 或者 b_expr2<==b_expr1 。对于表达式b_expr1==>b_expr2 而言，当b_expr1==false ，或者 b_expr1==true 且 b_expr2==true 时，整个表达式的值为 true 。
变量引用操作符：\nothing指示一个空集；\everything指示一个全集。
5）方法规格
前置条件(pre-condition)，前置条件通过requires子句来表示： requires P; 。要求调用者确保P为真。
后置条件(post-condition)，后置条件通过ensures子句来表示： ensures P; 。方法实现者确保方法执行返回结果一定满足谓词P的要求，即确保P为真。
副作用范围限定(side-effects)，副作用约束子句，使用关键词 assignable 或者 modifiable 。副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。
signals子句，signals子句的结构为 signals (***Exception e) b_expr ，意思是当 b_expr 为 true 时，方法会抛出括号中给出的相应异常e。还有一个简化的signals子句，即signals_only子句，后面跟着一个异常类型，调满足前置条件时抛出相应的异常。
6）类型规格
不变式（invariant）是要求在所有可见状态下都必须满足的特性，语法上定义invariant P，其中invariant 为关键词，P为谓词。
状态变化约束constraint对前序可见状态和当前可见状态的关系进行约束。
2.应用工具链
OPENJML用以检查JML的规范性。现在IDEA官方更新支持到18.2版本，更高的18.3和19.1是不支持的。因而引入该工具时需要从OpenJML官网下载并作为外置插件引入。JMLUnit/JMLUnitNG可以自动生成测试代码。
二、部署JML UnitNG
为了测试我们部署的JML UnitNG，我们选择了最简单的代码
然后使用以下指令即可生成测试文件以及对测试文件进行编译：
java -jar jmlunitng.jar Main.java
javac -cp jmlunit.jar *.java
openjml -rac Main.java
最后我们使用如下指令进行测试：
java -cp jmlunitng.jar: Main_JML_Test
能得到以下的结果，能看到自动生成的指令都以边界数据为主：
三、代码架构分析
1、第一次作业：总体而言很简单，唯一需要注意的就是复杂度的处理，笔者在写第一次的时候照着规格写了最简单的暴力轮询算法结果时间复杂度超了
2、第二次作业：第二次作业我是使用弗洛伊德算法将所有数据都存储了起来，每一次更新图便重新计算所有的图数据，查询操作可以O(1)时间完成
3、第三次作业：第三次作业延续了上一次的思路，使用拆点的方式然后使用佛洛依德算法，但这一次时间复杂度超了，考虑到可能是拆点后点过多每次弗洛伊德算法是n^3的时间复杂度，导致最终速度很慢，可以考虑不使用拆点的算法。
