BUAA_OO第三单元作业总结——JML

单元任务

本单元的主要内容是熟悉JML相关的理论知识，能够根据JML规格实现对应方法，通过一步步实现地铁系统来熟悉JML规格。

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

1. JML语言的理论基础

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.1 原子表达式

• \result表达式：表示一个非void 类型的方法执行所获得的结果，即方法执行后的返回值。
• \old( expr )表达式：用来表示一个表达式expr 在相应方法执行前的取值。

1.2 量化表达式

• \forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
• \exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
• \sum表达式：返回给定范围内的表达式的和。
• \max表达式：返回给定范围内的表达式的最大值。
• \min表达式：返回给定范围内的表达式的最小值。

1.3 集合表达式

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

1.4 操作符

• 子类型关系操作符：E1<:E2，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。
• 等价关系操作符：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指示一个全集，即包括当前作用域下能够访问到的所有变量。

1.5 方法规格

• 前置条件通过requires子句来表示： requires P; 。其中requires是JML关键词，表达的意思是“要求调用者确保P为真”。
• 后置条件通过ensures子句来表示： ensures P; 。其中ensures是JML关键词，表达的意思是“方法实现者确保方法执行返回结果一定满足谓词P的要求，即确保P为真”。
• 副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。使用关键词assignable或者modifiable。
• 为了有效的区分方法的正常功能行为和异常行为，public normal_behavior 表示接下来的部分对方法的正常功能给出规格，public exceptional_behavior表示对异常功能给出规格。
• signals子句的结构为signals (***Exception e) b_expr，意思是当b_expr为true时，方法会抛出括号中给出的相应异常e。

1.6 类型规格

• 不变式（invariant）是要求在所有可见状态下都必须满足的特性，语法上定义invariant P，其中invariant 为关键词，P为谓词。
• 状态变化约束constraint对前序可见状态和当前可见状态的关系进行约束。

该部分内容摘自JML Level 0手册。

2. 应用工具链

Java可以用来指定Java模块的行为（如DBC协议中的设计）。它有许多工具来进行断言检查、文档生成、单元测试、静态检查、验证等。

下面是通用JML工具版本中每个工具的Unix样式手册页。手册的每一页都有一些关于如何使用该工具的信息，并指定了它们的选项和参数。

• jml-launcher：图形用户界面工具的启动程序。
• jml和jml-gui：检查器。
• jmlc和jml-gui：编译用于运行时断言检查。
• jmldoc和jmldoc-gui：包含JML规范信息的JavaDoc版本。
• jmle：为执行或原型化规范而编译。
• jmlrac：Java版本，VM，包括类路径中的BI/JMLRunTime.JAR文件，用于运行用JMLC编译的文件。
• jmlre：Java版本，VM，包括执行规范所需的运行时支持，用于运行用JMLE编译的文件。
• jmlspec和jmlspec-gui：从Java源文件生成骨架规范文件。
• jmlunit和jmlunit gui：生成用于JUnit的单元测试代码存根。
• jtest：结合jmlc和jmlunit的工作。
• jml-junit：JUnit的Swing用户界面的一个版本，包括类路径中的bin/jmluntime.jar和bin/jmljunitruntime.jar文件，用于对用jmlc编译的文件和jmlunit生成的测试用例运行基于jml和junit的测试。

该部分内容摘自http://www.eecs.ucf.edu/~leavens/JML/documentation.shtml

二、部署SMT Solver

在部署OpenJML上花了两天时间，试了各种方法，最后也不知道自己到底是不是部署成功了，在测试的过程中出现了各种问题。

因为第二次和第三次作业中都有自己定义的类，每次检查到自己定义的类时，就会出现找不到符号的错误，因此只好测试第一次作业中的代码。

测试GjxPath中的equals()方法

推测可能是因为接口Path声明中不包含nodes，因此找不到符号。

因为GjxPath没有通过检查，所以无法进行静态分析。因此，我使用Demo1.java来尝试静态分析，该段代码来自第九次作业讨论区。

package demo;public class Demo1 {/*@@ public normal_behaviour@ requires lhs>0 && rhs<0;*/public static int compare(int lhs, int rhs) {return lhs - rhs;}public static void main(String[] args) {compare(114514, 1919810);}
}

静态分析的结果如下：

第一个警告是因为减法可能会产生越界，后面的警告还没有搞清楚。

三、部署JMLUnitNG/JMLUnit

因为三次作业的代码在openJML检查中都没有通过，因此无法实现自动生成测试用例，此处依旧是通过上文中的Demo1.java来进行尝试。

依次输入以下指令

java -jar jmlunitng.jar src/demo/Demo1.java
javac -cp jmlunitng.jar src/demo/Demo1_JML_Data/*.java src/demo/*.java

生成以下文件

在idea中运行Demo1_JML_Test.java文件，得到运行结果

可以看出对于整数型参数，主要是通过边界数据，如-2147483647和2147483647，以及特殊数据0，来测试程序是否正确执行。

四、架构设计

1. 第一次作业

本次作业的结构没有什么可说的，只是完成了基本要求的Path类和PathContainer类。ArrayList结构负责进行遍历，HashSet结构负责统计不同节点的个数。

需要注意的是，因为这个单元的作业都有严格限制CPU运行时间，所以像distinctNodeCount()方法，如果每次都去遍历一遍，极有可能会超时，因此通过参考讨论区大佬们的讨论，添加了HashSet结构来进行节点数量的统计，避免每次遍历，将时间复杂度分摊在构造函数和addPath()和removePath()方法中。

2. 第二次作业

本次作业在架构上与上次作业差不多，只添加了一个类便于统计边。

本次作业在上次作业的基础上添加了计算距离和连通性的功能，我的实现方法是建立邻接矩阵，通过邻接矩阵计算距离矩阵。

距离矩阵是通过可达矩阵得来的，设可达矩阵为R，邻接矩阵为A，则有

R=binary(I+A+A²+A³+…+Aⁿ)

对于矩阵A^k，A^k[i][j]表示从节点i到节点j长度为k的路径数量，因此对于距离矩阵D，当A^k[i][j]第一次出现非0元素时，D[i][j]即为该次方数k。

在代码实现的过程中，邻接矩阵和距离矩阵是通过int型二维数组存储的，每次添加和移除边的时候需要重新计算一次距离矩阵。因为没有使用HashMap结构进行映射，导致我每次都需要通过遍历来查找nodeId对应的index，造成了很多时间上的浪费。同时，因为没有进行映射，每次移除节点的时候还需要对邻接矩阵和距离矩阵进行移位。

这次作业原本应该是通过集成上次的PathContainer类来实现Graph类，但为了节省时间，选择了直接复制的方式，没有进行重构，只是添加了几个方法，重写了上一次的addPath()、removePath()和removePathById()方法。

3. 第三次作业

通过类图可以看出这次作业明显复杂了，但程序结构依旧与上两次类似。虽然在发现GjxRailwaySystem类超过500行之后，尝试使用继承的方式，但因为实现起来比较复杂，最后还是放弃了，将几个参数相对少的方法新建了一个类，以此减少GjxRailwaySystem类的行数。

因此，三次作业在架构上没有什么区别，也没有进行重构，每次只是在上一次的基础上重写和添加一些方法，以实现新的功能。

这次作业因为涉及最少票价、最少换乘次数、最少乘客不满意度，每条边上的权值都各不相同，在看过讨论区大佬们的探讨后，选择采取拆点的方法，每个点拆为起点、终点、每条边上的点，边上的点根据不同的图带有不同的权值，每条边上的点到终点的权值为0，终点找起点的权值为换乘一个的取值，起点带每条边上的点的权值为0，形成拆点之后的四张带有权值的图，通过四个矩阵进行存储。对每张图执行最短路径算法，可以求得在不同权值下的最短路径，即最少票价、最少换乘次数和最少乘客不满意度。

吸取了上次超时的教训，这次在结构上采取了HashMap的结构存储映射关系，另外创建一个ArrayList来存储可以使用的index，每次添加点的时候移除第一个，移除点的时候将index添加到ArrayList的末尾处。

在计算最小结果的时候采取的是Floyd算法（类图中的dijkstra方法是因为我后来尝试了一下dijkstra方法，但最后没有提交，提交的最终版是Floyd算法），但因为拆点导致节点数大量增加，最终CPU还是超时了。

在计算连通块个数时，选择的是并差集的方法，最初每个节点是一个集合，如果两个点连通，就将两个集合合并成一个集合，最终统计集合的个数，即为连通块的个数。

每次在有添加边和移除边的操作时，都需要重新计算连通块个数以及每张图的最短路径。

在这次和上次作业中都涉及到需要构造自己写的类的集合，因此需要重写创建的类的equals()方法。在运行之后，我发现只重写equals()方法是不够的，因为集合在判断两个元素是否相等的时候，是先判断两者的HashCode是否相等，如果HashCode相等再通过equals()方法判断，因此还需要重写hashCode()方法。

通过上网查询得到hashCode()方法可以重写为下面的形式

    public int hashCode() {int result = hashCode;if (result == 0) {result = 17;result = 31 * result + nodeId;result = 31 * result + pathId;hashCode = result;}return result;}

至于为什么最初是17，之后每次乘31，我并没有查到答案，貌似是一种规定。

五、bug分析和修复

• 第一次作业强测没有bug，也没有超时。

• 第二次作业出现了两个逻辑上的bug，主要还是因为在映射上没有使用类似HashMap的结构，导致在移除边的时候需要对矩阵进行行的移动和列的移动，在第三次作业中通过使用HashMap结构解决了这个问题。这次作业还出现了CPU运行时间过长的问题，主要原因还是因为没有使用HashMap结构来存储映射关系，导致每次都是遍历查询，浪费了许多时间，其次，因为使用的是邻接矩阵和可达矩阵的算法，每次都需要进行矩阵乘法，每次矩阵乘法都是O(n²)的时间复杂度，从时间复杂度角度上是没有Dijkstra算法快的。

• 第三次作业出现了RUNTIME_ERROR的错误，有的是因为抛出了异常，因为空指针的问题，有的完全没有返回信息，因此到现在还没搞懂是为什么。超时的问题主要还是因为拆点之后导致节点数急剧增多，每次添加和移除都需要花费大量时间，不知道讨论区的大佬究竟是怎么实现的可以把时间缩得那么短。

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

规格在工程上具有很重要的意义，因为规格规定好一个方法的输入和输出，对于方法使用者而言，不需要关心方法的具体实现，只需要按照前置条件输入参数，按照后置条件使用返回值即可。而对于方法实现者而言，不需要关心其他方法的实现，只需要实现规格中规定的功能即可。规格的存在使得团队分工合作十分便捷，统一接口，实现高内聚低耦合。

起初以为规格的撰写十分简单，就是将文字叙述转换为逻辑语言，但当真正开始读和写JML的时候才发现远没有那么简单。虽然JML和逻辑语言很像，但实际上还是比逻辑语言复杂很多，因为需要描述各个变量在方法执行完之后的结果，逻辑会变得十分复杂。同时因为规格不是程序执行过程的描述，所以在根据程序撰写规格时需要转换思维，从执行前和执行后的差别上着手。

这个单元原本以为按照规格完成代码会比较简单，但事实上难点在于图论方面知识的实现。同时，这个单元的作业都是根据规格写代码，在撰写规格方面还需要练习。