一、JML语言

JML是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言，基于Larch方法构建。 可以用来为严格的程序设计提供一套有效的方法。通过JML及其支持工具，不仅可以更加精确地描述代码所完成的任务，还可基于规格自动构造测试用例，有效地发现和纠正错误，还整合了SMT Solver等工具以静态的方式来检查代码实现对规格的满足情况。

 

理论基础

• 注释结构

  JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式为 //@annotation ，块注释的方式为 /* @ annotation @*/ 。

 

• JML表达式

  • 原子表达式

    \result：表示一个非void类型的方法执行所获得的结果，即方法执行后的返回值。

    \old(expr)：用来表示一个表达式expr在相应方法执行前的取值。

    \not_assigned(x,y,...)：用来表示括号中的变量是否在方法执行过程中被赋值。若没有赋值，返回true，否则返回false。

    \not_modified(x,y,...)：限制括号中的变量在方法执行期间的取值未发生变化。

    \type(type)：返回类型type对应的类型(Class)。

    \typeof(expr)：该表达式返回expr对应的准确类型。

  • 量化表达式

    \forall：全称量词修饰表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。

    \exists：存在量词修饰表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。

    \sum：返回给定范围内的表达式的和。

    \product：返回给定范围内的表达式的连乘结果。

    \max：返回给定范围内的表达式的最大值。

    \min：返回给定范围内的表达式的最小值。\num_of：返回指定变量中满足相应条件的取值个数。

  • 集合表达式

    可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素。

  • 操作符

    子类型关系操作符：E1<:E2，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。如果E1和E2是相同的类型，该表达式的结果也为真。

    等价关系操作符：b_expr1<==>b_expr2或者 b_expr1<=!=>b_expr2 ，其中b_expr1和b_expr2都是布尔表达式，这两个表达式的意思是 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指示一个全集，即包括当前作用域下能够访问到的所有变量。变量引用操作符经常在assignable句子中使用，如 assignable \nothing 表示当前作用域下每个变量都不可以在方法执行过程中被赋值。

 

• 方法规格

  • 前置条件(pre-condition)

    前置条件通过requires子句来表示： requires P; 。其中requires是JML关键词，表达的意思是“要求调用者确保P为真”。注意，方法规格中可以有多个requires子句，是并列关系，即调用者必须同时满足所有的并列子句要求。如果设计者想要表达或的逻辑，则应该使用一个requires子句，在其中的谓词P中使用逻辑或操作符来表示相应的约束场景： requires P1||P2;。

  • 后置条件(post-condition)

    后置条件通过ensures子句来表示： ensures P; 。其中ensures是JML关键词，表达的意思是“方法实现者确保方法执行返回结果一定满足谓词P的要求，即确保P为真”。同样，方法规格中可以有多个ensures子句，是并列关系，即方法实现者必须同时满足有所并列ensures子句的要求。如果设计者想要表达或的逻辑，这应该在在一个ensures子句中使用逻辑或( || )操作符来表示相应的约束场景： ensures P1||P2; 。

  • 副作用范围限定(side-effects)

    副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。从方法规格的角度，必须要明确给出副作用范围。JML提供了副作用约束子句，使用关键词 assignable 或者modifiable 。从语法上来看，副作用约束子句共有两种形态，一种不指明具体的变量，而是用JML关键词来概括；另一种则是指明具体的变量列表。

 

• 类型规格

  JML针对类型规格定义了多种限制规则，从课程的角度，我们主要涉及两类，不变式限制(invariant)和约束限制(constraints)。无论哪一种，类型规格都是针对类型中定义的数据成员所定义的限制规则，一旦违反限制规则，就称相应的状态有错。

 

应用工具链

• OpenJML：基本的功能就是对JML注释的完整性进行检查，检查包括经典的类型检查、变量可见性与可写性等, 也可以对代码进行静态和运行时检查。

• JMLUnitNG：是用于JML注释的Java代码的自动化单元测试生成工具。

 

二、部署JMLUnitNG，针对Graph接口的实现自动生成测试用例

 

 

三、程序分析

• 第一次作业（实现Path和PathContainer两个容器类）

  类图：

  

   

   

  度量分析：

  

  

   

  

   

  bug分析：

  第一次实现的Path和PathContainer两个容器的方法都不难，参考JML规格很容易实现，并且通过中测。但是也正是因为如此，没有考虑到运行时间的问题，在计算容器内不同节点数的时候，直接暴力遍历Path数组，导致强测遇到更多更大数据时会CPU超时。修复bug时，新建了一个存储容器内不同节点的数组，每次addPath和RemovePath时，更新这个数组，在计算容器内不同节点数时只需要计算这个数组大小就可以，大大降低CPU的运行时间。

   

• 第二次作业（实现Path和Graph两个容器类）

  类图：

  

   

   

  度量分析：

  

  

   

  

   

  bug分析：

  这一次的作业bug主要还是CPU超时，而这次是因为在计算最短路径时使用的dijkstra算法不优化。一开始使用的dijkstra算法，嵌套三层for循环，前两层都完全遍历了容器内所有节点一遍，显然这样的算法复杂度很高，很容易使得CPU超时。修复bug时，优化了原有的dijkstra算法，使用while语句，从要计算最短路径的开始节点开始遍历，只需要考虑与from节点相邻的节点就可以，再考虑与相邻节点相邻的节点，如此下去，直到遇到计算最短路径的结束节点即可跳出循环，大大降低复杂度，减少CPU运行时间。

   

• 第三次作业（实现Path和RailwaySystem两个容器类）

  类图：

  

  

   

  度量分析：

  

  

   

  

   

  bug分析：

  这一次作业虽然比前两次更加复杂，但是他建立在第二次作业计算两节点间最短路径基础上，只需要修改计算最短路径的算法，就可以了。由于采用了第二次作业优化的dijkstra算法，因此，终于没有遇到CPU超时问题。但是强测过程中还是遇到了一个bug，在Node类里，移除该节点的相邻节点方法，由于对hashmap的理解不够，并且没有考虑到该节点的相邻节点如果就是它本身的情况，导致有异常。

 

四、心得体会

本单元主要学习了JML规格的使用。每次作业都有给出很明确JML规格说明，大大方便了我们实现代码，可以说比起前两单元的作业，这一单元的作业并没有那么令人难受了。经过这一单元的学习，包括三次作业、几次实验，我对JML规格也有了一些理解。对于一个方法的JML，是包括这个方法的正常情况以及异常情况的，同时也包括正常情况写的各种子情况、异常情况下的各种子情况。而对于一些复杂的方法，构造中间层的JML来表述会更加简洁明了。

但是虽然在作业中给我们提供了完备的JML规格，但是我在写代码的时候，只有较为简单的方法，会参考JML写，而对于较为复杂的方法，比如计算两个节点的最短距离，并没有给我想象中那么大的帮助。

不过总体而言，JML非常严谨，可以帮助我们节省很多用于处理输入输出的精力，使我们专心于代码的实现，这一点还是很有帮助的。