JML语言的理论基础、应用工具链
前言
JML是用于对java程序进行规格化设计的一种表示语言。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，而且能够以静态方式来检查代码实现对规格的满足情况。
理论基础
注释结构
通过使用javadoc注释的形式表示规格，每行以@起头，包括行注释和块注释两种表示方式。
JML表达式
JML表达式是对java表达式的扩展，新增了一些操作符和原子表达式，但同样有优先级顺序的规定。
原子表达式
esult表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。
ot_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。
ot_modified(x,y,...)表达式：与上面的 ot_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取值未发生变化。
onnullelements( container )表达式：表示 container 对象中存储的对象不会有 null 。
ype(type)表达式：返回类型type对应的类型(Class)，如type( boolean )为Boolean.TYPE。
ypeof(expr)表达式：该表达式返回expr对应的准确类型。
量化表达式
forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
sum表达式：返回给定范围内的表达式的和。
product表达式：返回给定范围内的表达式的连乘结果。
max表达式：返回给定范围内的表达式的最大值。
min表达式：返回给定范围内的表达式的最小值。
um_of表达式：返回指定变量中满足相应条件的取值个数。
操作符
子类型关系操作符： E1<:E2 ，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。如 果E1和E2是相同的类型，该表达式的结果也为真，如 Integer.TYPE<:Integer.TYPE 为真；但 Integer.TYPE<:ArrayList.TYPE 为假。需要指出的是，任意一个类X，都必然满足 X.TYPE<:Object.TYPE 。
等价关系操作符： b_expr1<==>b_expr2 或者 b_expr1<=!=>b_expr2 ，其中b_expr1和b_expr2都是布尔表达 式，这两个表达式的意思是 b_expr1==b_expr2 或者 b_expr1!=b_expr2 。可以看出，这两个操作符和Java中的 == 和 != 具有相同的效果，按照JML语言定义， <==> 比 == 的优先级要低，同样 <=!=> 比 != 的优先级低。
推理操作符： b_expr1==>b_expr2 或者 b_expr2<==b_expr1 。对于表达式 b_expr1==>b_expr2 而言，当 b_expr1==false ，或者 b_expr1==true 且 b_expr2==true 时，整个表达式的值为 true 。
变量引用操作符：除了可以直接引用Java代码或者JML规格中定义的变量外，JML还提供了几个概括性的关键词来 引用相关的变量。
othing指示一个空集；everything指示一个全集，即包括当前作用域下能够访问到的所有变 量。变量引用操作符经常在assignable句子中使用，如 assignable
othing 表示当前作用域下每个变量都不可以 在方法执行过程中被赋值。
方法规格
前置条件
前置条件通过requires语句表示，要求调用者确保被调用条件为真。
后置条件
后置条件通过ensures语句表示，要求方法实现者确保返回结果满足所定义条件的要求。
副作用范围限定
通过使用assignable或者modifiable关键词定义副作用约束语句，限定次方法执行对后续方法执行产生的影响范围。
类型规格
类型规格指针对Java程序中定义的数据类型所设计的限制规则，一般而言，就是指针对类或接口所设计的约束规则。 从面向对象角度来看，类或接口包含数据成员和方法成员的声明及或实现。
应用工具链
OpenJML：可用于检查规格设计的规范性。
JMLUnit：可用于进行单元测试，检查代码实现的正确性。
部署JMLUnit测试
关于这一部分，在部署测试时，由于我的jdk版本是1.9，无法运行openjml，所以我先转换到了jdk8.
之后在运行时，又因为文件路径有中文和jar包保存在package目录下而产生了很多编译错误的bug。
我这次的测试是用的讨论区大佬，大概弄清楚了JMLUnit测试的步骤。
测试源码：
运行结果：
架构梳理
第九次作业
第九次作业的主要目标是实现两个容器类Path和PathContainer，这次作业的难度较低，作为规格实现的第一次作业比较合适。
总的来说没什么困难，主要就是要读懂规格要求，确保程序与规格要求没有冲突就可以了。
第十次作业
第十次作业的要求是实现两个容器类Path和Graph，其中Path类与第九次作业的要求相同，Graph类是继承了第九次作业中的PathContainer接口。
在完成这次作业时，可以在第九次作业的成果上进行迭代，这样可以节省很多时间。其中的Path类可以照搬上次的，而Graph类既可以在继承PathContainer类的基础上完成，也可以直接修改PathContainer类。但在继承PathContainer类时，由于变量保护的原因，无法直接调用PathContainer类中的数据变量，为图方便，我直接修改了PathContainer类，在其中增加新的需求内容。本次作业的主要难点在于两结点间最短路径的计算，为了解决这个问题，我使用了floyd算法。
第十一次作业
第十一次作业的要求是完成两个容器类Path和RailwaySystem。
关于这次作业，我在前一次作业的Path类中新增了一个函数，使其满足规格要求；而对于RailwaySystem，我魔改了第十次作业的Graph类，并新增了三个类Leastprice，LeastTransfer和LeastUnpleasant，分别用来计算最低票价、最少换乘和最低不满意度。而算法方面，我使用了依旧是floyd算法，具体实现思路参考了讨论区大佬的方法，主要原理是将计算信息转换为边的权值，利用folyd算法求两结点间的最短路得到结果。
bug和修复情况
第九次作业
第九次作业中未发现bug。
第十次作业
本次作业中bug的主要来源是使用floyd算法时出现的错误，由于循环变量的设置问题（即i，j，k三重循环作为二维数组下标的使用顺序），我的程序在处理某些数据时，会产生十分奇怪的输出。究其原因，是我在写代码时不够认真所导致的。
第十一次作业
我在本次作业中出现的bug是判断同节点间路径存在性问题的错误输出。由于我的程序中判断路径是否存在的依据是两结点间最短路径是否为一，而我在执行floyd算法计算最短路径时，将每个结点到自身的距离直接设置为零，从而使得对每个结点到自身的路径是否存在无法正确判断。
心得体会
还是认真阅读规格要求，做好单元测试吧。除此以外没有什么办法能够解决程序中出现的bug。