OO第三单元总结——JML

一、梳理JML语言的理论基础、应用工具链情况

理论基础：

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。

1.注释结构

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

2.JML表达式

2.1 原子表达式

esult表达式：表示一个非void 类型的方法执行所获得的结果，即方法执行后的返回值。 esult表达式的类型就是方法声明中定义的返回值类型。

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

ot_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。

ot_modified(x,y,...)表达式：与上面的 ot_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取值未发生变化。

onnullelements( container )表达式：表示container 对象中存储的对象不会有null。

ype(type)表达式：返回类型type对应的类型(Class)。

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

2.2 量化表达式

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

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

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

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

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

min表达式：返回给定范围内的表达式的最小值。

um_of表达式：返回指定变量中满足相应条件的取值个数。

2.3 集合表达式

集合构造表达式：可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素。集合构造表达式的一般形式为：new ST {T x|R(x)&&P(x)}，其中的R(x)对应集合中x的范围，通常是来自于某个既有集合中的元素，如s.has(x)，P(x)对应x取值的约束。

2.4 操作符

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

(2) 等价关系操作符： b_expr1<==>b_expr2 或者b_expr1<=!=>b_expr2 ，其中b_expr1和b_expr2都是布尔表达式，这两个表达式的意思是b_expr1==b_expr2 或者b_expr1!=b_expr2 。

(3) 推理操作符： b_expr1==>b_expr2 或者b_expr2<==b_expr1 。对于表达式b_expr1==>b_expr2 而言，当b_expr1==false ，或者b_expr1==true 且b_expr2==true 时，整个表达式的值为true 。

(4) 变量引用操作符：除了可以直接引用Java代码或者JML规格中定义的变量外，JML还提供了几个概括性的关键词来引用相关的变量。 othing指示一个空集；everything指示一个全集，即包括当前作用域下能够访问到的所有变量。

3. 方法规格

前置条件(pre-condition)

前置条件通过requires子句来表示： requires P; 。其中requires是JML关键词，表达的意思是“要求调用者确保P为真”。注意，方法规格中可以有多个requires子句，是并列关系，即调用者必须同时满足所有的并列子句要求。

后置条件(post-condition)

后置条件通过ensures子句来表示： ensures P; 。其中ensures是JML关键词，表达的意思是“方法实现者确保方法执行返回结果一定满足谓词P的要求，即确保P为真”。同样，方法规格中可以有多个ensures子句，是并列关系，即方法实现者必须同时满足有所并列ensures子句的要求。

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

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

正常功能行为和异常行为

public normal_behavior：正常行为功能

public exceptional_behavior：异常行为功能

signals子句

signals子句的结构为signals (***Exception e) b_expr ，意思是当b_expr 为true 时，方法会抛出括号中给出的相应异常e。

4. 类型规格

类型规格指针对Java程序中定义的数据类型所设计的限制规则，一般而言，就是指针对类或接口所设计的约束规则。

不变式invariant

不变式（invariant）是要求在所有可见状态下都必须满足的特性，语法上定义invariant P ，其中invariant 为关
键词， P 为谓词。凡是会修改成员变量（包括静态成员变量和非静态成员变量）的方法执行期间，对象的状态都不是可见状态。类型规格强调在任意可见状态下都要满足不变式。

状态变化约束constraint

对象的状态在变化时往往也许满足一些约束，这种约束本质上也是一种不变式。JML为了简化使用规则，规定
invariant只针对可见状态(即当下可见状态)的取值进行约束，而是用constraint来对前序可见状态和当前可见状态的
关系进行约束。

应用工具：

openJML：可以对代码进行JML规格的语法的静态检查，还支持使用SMT Solver动态地检查代码对JML规格满足的情况。

JMLUnitNG/JMLUnit：根据JML描述自动生成与之符合的测试样例，重点会检测边界条件。

二、JMLUnitNG使用

先编写测试类

// demo/Demo.java
package demo;

public class Demo {
    /*@ public normal_behaviour
      @ ensures 
esult == (a>b);
    */
    public static boolean compare(int a, int b) {
        return a>b;
    }

    public static void main(String[] args) {
        compare(111,222);
    }
}

安装好openjml和jmlunitng

执行命令 jmlunitng demo/Demo.java 生成相应测试文件

编译 javac -cp jmlunitng.jar demo/*.java  openjml -rac demo/Demo.java 

运行测试文件 java -cp jmlunitng.jar demo.Demo_JML_Test 

可以看出，生成的测试数据都是边界数据，这也符合工程测试的要求。

三、梳理架构设计，分析迭代中对架构的重构

第一次作业

类图：

三个类，

Path类维护两个数据成员

private ArrayList<Integer> nodes;　　
private HashMap<Integer, Integer> map;

nodes用来索引，存储Path的节点序列，而map用来查看Path中是否包含某个节点以及统计Path不同节点的个数。

PathContainer类维护四个数据成员

private HashMap<Path, Integer> map1;
private HashMap<Integer, Path> map2;
private HashMap<Integer, Integer> mapnodes;
private static int pid = 0;

map1存储键值对<Path,PathId>

map2存储键值对<PathId,Path>

mapnodes存储键值对<NodeId,该Node重复的次数>

静态变量pid存当前最大PathId

containsPath(Path path),getPathId(Path path)使用成员map1查询

containsPathId(int pathId),getPathById(int pathId)使用成员map2查询

本次作业复杂度比较高且调用次数比较多的的指令是统计容器不同节点的个数，为了防止tle，因此我选择了把它分散到调用次数相对较少的方法（addPath,removePath,removePathById）中，这些方法都是改变该类成员属性的。

添加或移除路径时，需要给map1、map2、mapnodes添加或删除或更新键值对。

在调用方法int getDistinctNodeCount()时，直接返回maonodes.size()即可，这样便可极大的降低时间复杂度。

第二次作业

类图：

这次作业在之前的基础上新增了几条指令：CONTAINS_NODE（容器中是否存在某个结点），CONTAINS_EDGE（容器中是否存在某一条边），IS_NODE_CONNECTED（两个结点是否连通），SHORTEST_PATH_LENGTH（两个结点之间的最短路径）。

对于新需求要做的变化：

很显然前两条指令可以使用第一次作业的mapnodes来查询。

涉及最短路径的计算，所以需要构建一个图的数据结构，类似于邻接矩阵，我新增一个类GraphStructure

public class GraphStructure {
    private HashMap<Integer, HashMap<Integer, Integer>> edgeNum;
    private HashMap<Integer, HashMap<Integer, Integer>> minPathLength;
    private final int inf = 99999999;

    public GraphStructure() {
        edgeNum = new HashMap<>();
        minPathLength = new HashMap<>();
    }
    
    public void addVer(int nodeId) {}
    
    public void addEdge(int from, int to) {}

    public void removeEdge(int from, int to) {}

    public void removeVer(int nodeId) {}

    public boolean containsEdge(int fromNodeId, int toNodeId) {}

    public void floyd() {}

    public boolean isConnected(int fromNodeId, int toNodeId) {}

    public int getShortestPathLength(int fromNodeId, int toNodeId) {}

}

该类在MyGarph中被实例化一个对象。 

这个类维护一个图结构edgeNum，采用双层hashmap嵌套,存储键值对<顶点i，Hashmap<顶点j，顶点i、j之间的边数>>

每次添加或移除路径时，调用该类的addVer()、addEdge()、removeVer()、removeEdge()方法来更新该类的图结构，然后调用floyd（）来计算所有节点之间的最短路径，将结果存到minPathLength中。

第三次作业

类图

此次增加的指令是CONNECTED_BLOCK_COUNT（整个图中的连通块数量），LEAST_TICKET_PRICE（两个结点之间的最低票价），LEAST_TRANSFER_COUNT（两个结点之间的最少换乘次数），LEAST_UNPLEASANT_VALUE（两个结点之间的最少不满意度）。

对于新需求要做的变化：

对每个指令添加一个类来实现相应的功能。

求解连通块我采用的是并查集的方法。

剩下的三个由于涉及到换乘，因此我借鉴讨论区的方法，每种方法构造一个图(在每条path中加边，并添加能体现换乘的权重)，求此图的最短路径即可。求最短路径采用的是Dijskra算法，将获得的一部分结果缓存到hashmap中，这样带来的好处可以避免一些不必要的计算。

当添加或删除路径的时候，对这三个类直接重新new一个对象，然后根据容器类的path进行图的构建。

分析：

这三次作业的迭代，每次都会添加一些新的功能，不过我的架构基本没什么变化，都能保证原有代码不变，类之间的解耦做的很好，这样对我的代码维护起到了很大的作用。但是也有不足，就是第三次作业中类的整合做的不是很好，导致几个类有一些重复代码。

四、分析代码实现的bug和修复情况

第一次作业tle了几个点，因为对Path类重写hashcode()时过于复杂，复杂度为O（n），直接返回path.size()即可修复。

第二次作业没出现bug。

第三次作业出现大面积wa，发现原来是把Integer等同于int来对待了，直接用“==”导致只要测试点出现比较大的整数就有bug，了解到二者区别，判断Integer是否相等应该使用equals。

五、对规格撰写和理解上的心得体会

规格和代码是相互辅助的，借助规格我们可以检查代码逻辑的正确性，还可以使我们的代码更易被人理解。

规格对设计、实现、测试都是很有用的工具。学会撰写规格、利用规格来测试是很有必要的。

实现代码的时候不要被规格说明限制，例如path类中数据规格是int[]，但是实现时可以使用ArrayList、Hashmap这些数据结构来降低相应方法的时间复杂度。

总之，JML这一单元让我对面向对象有了新的思考和认识。