OO第三单元总结

Posted 2021-02-18 xcw011010

OO第三单元总结

一、JML理论基础与工具链

1.JML简介

JML，即Java Modeling Language，是一种对Java程序进行规格化设计的表示语言。其用处主要有：1.开发时做出规格化设计，以便代码编写者实现；2.方便根据规格化描述开展对应的测试；3.针对已经实现的代码，编写对应规格以提高代码可维护性。

2.JML语法介绍

JML主要以javadoc的方式来表示规格，每行以@起头，分为行注释//@xxxxx和块注释/*@ xxxxx @*/两种。

• 原子表达式
  • esult:表示一个非void的方法执行后的返回值。
  • old(expr):表示一个表达式expr在执行相应方法前的取值
  • ot_assigned(x, y, ...):表示括号内的变量在方法执行过程中是否被赋值。没有被赋值则返回true；否则返回false
  • ot_modified(x, y, ...):类似not_assigned，区别是表示变量取值是否变化
  • ype(type):返回类型type对应的Class
• 量化表达式
  • forall:全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应约束
  • exists:存在量词修饰的表达式，表达对于给定范围内的元素，存在某个元素满足相应的约束
  • sum:返回给定范围内的表达式的和
  • max和min:分别返回给定范围内表达式的最大和最小值
• 操作符
  • E1 <: E2:子类型关系操作符，如果类型E1是类型E2的子类型或同类型(sub type)，则该表达式的结果为真，否则为假
  • b_expr1<==>b_expr2:等价关系操作符
  • b_expr1==>b_expr2:推理操作符
  • 变量引用操作符： othing指示一个空集；everything指示一个全集
• 方法规格
  • 前置条件：前置条件通过requires子句来表示：requires P，即要求确保条件P为真
  • 后置条件：后置条件通过ensures子句来表示：ensures P，即要求确保方法执行返回结果一定满足谓词P
  • 副作用限定：通过assignable和modifiable，分别表示可赋值、可修改
• 类型规格
  • 不变式invariant：是要求在所有可见状态下都必须满足的特性，invariant P
  • 状态变化约束constraint：对前序可见状态和当前可见状态的关系进行约束

3.JML相关工具链

• OpenJML：对JML进行语法检查、代码检查等功能
• JMLUnitNG：根据JML自动生成测试文件

具体部署过程见下

二、OpenJML和JMLUnitNG部署和使用

1.OpenJML

OpenJML主要是用于对JML进行检查的。这一工具的使用参考了一位学长的博客(十分感激这位学长，看了博客以后省去了不少时间)。下载了OpenJML工具后，编写一个脚本，添加到环境变量里就可以直接使用命令行操作。先随便写一个有语法错误的JML规格来进行检测：

public class test {
	/*@
	  @ requires a >= 0 && b >= 0 2333;
	  @ ensures 
esult == (a + b);
	  @*/
	public int add(int a, int b) {
		return a + b;
	}
	public static void main(String[] args) {
		add(2333, 23333);
	}
}

结果如下：

可以看出，JML中的错误和调用非静态方法的错误都检查了出来，改正之后则不会出现这些。下面对第三次作业中的Group和Person方法进行检验，结果如下：

其他地方倒没什么错误，除了三目运算符...想起之前checkstyle的时候三目运算符也不给过，百度一番也没找到结果。可能OpenJML只是单纯不支持这个。

2.JMLUnitNG

JMLUnitNG是一种针对类自动生成测试文件的工具。听起来很方便，很自动化，但部署过程实在一言难尽...耗时又耗力，其中总是报各种错误，好在最后还是能勉强使用了

• 从官网上下载jmlnitng的jar包
• 创建文件夹test，将待检测的java文件放在test文件夹下，以一个简单的比较函数为例：

package test;

public class Test {
    /*@ public normal_behaviour
    @ ensures 
esult == num1 - num2;
    */

    public static int compare(int num1, int num2) {
        return num1 - num2;
    }
 
    public static void main(String[] args) {
        compare(233333, 2333);
    }   
}

• java -jar jmlunitng.jar test/Test.java：生成测试文件，这一步之后文件夹中会生成如下文件：

• javac -cp jmlunitng.jar test/Test_JML_Test.java：编译测试文件，这一步后文件夹变成下面的样子：

• javac -cp jmlunitng.jar test/Test.java：编译源文件

• java -cp jmlunitng.jar test/Test_JML_Test：进行测试，结果如下：

一些使用注意事项：

• 需要用jdk8，否则各种报错
• 注意java文件中包名

由上述结果可以看出，JMLUnitNG主要是通过构造一些边界数据，比如0、+-2³¹-1和null这种数据，来检验方法是否正确。不可否认的是对于一些简易的数值处理类方法，JMLUnitNG可以在短时间内对于边界情况进行排查检验，但说实话，这个工具用起来还是有些鸡肋(也有一部分原因可能是自己没钻研透)，就本次作业而言，数据大都是限定在一定范围内，检查边界数据可能用处不是特别明显，而且面对一些复杂的方法使用起来可能不是那么便利。除此之外，部署麻烦也从第一步开始就劝退了不少人使用。不过本人目前对这个工具也只是一知半解，如果日后还能接触JML的话还是有继续学习使用它的必要(下次一定)

三、三次作业构架设计

1、第一次作业

第一次作业是对JML规格的一个入门，目标为实现一个社交关系模拟系统。需要实现的是Person和Network两个类，根据JML实现相应的方法。

• 由于第一次接触JML，看到规格变量中使用静态数组实现，不太敢使用map之类的容器，最终使用了最简单朴素的ArrayList
• 添加关系存放acquaintance和value时成对存放，保证同一索引对应的人和value数值是一对的
• 一些查询类的方法实现基本依照JML来写，即从头遍历
• 稍微复杂点的函数isCircle通过BFS实现，从id1开始，搜索到id2立即返回true

类图：

整体结构并不复杂，三个类即可实现

2、第二次作业

第二次作业增加了一个Group类，同时Network增加了几个与group交互的方法。

• 为了防止TLE，废弃了之前ArrayList，改用HashMap，存放id-xxxxx键值对，可以省去不少遍历开销
• 对于一些JML规格描述中需要双层遍历的方法，如getRealationSum、getValueSum，设置缓存，每次向group中添加人或者添加关系时更新这些缓存，调用时直接返回

类图：

总体来说比上一次内容多了一点，但实现并不困难。在做第二次作业的过程中发现方法的具体实现不能过于依赖JML的描述，否则有超时的风险，只要保证JML的前置、后置条件和相关的约束，实现方式与JML描述不同也可以。

3、第三次作业

第三次作业增加了求最短路径、连通分量个数以及其他一些方法，最大的不同在于与离散数学知识联系了起来，对于算法的要求提高了不少

• 对于queryMinPath方法，采用堆优化的dijkstra算法。为此新创建了一个edge类，重写了compareTo方法，存入优先队列保证队首是最短的边
• 对于queryStrongLinked，方法很暴力，使用dfs，第一次dfs找出所有路径，记录路径上的所有点；第二次枚举这些点，检验将其删去是否影响连通性。虽然实现容易，但最终效率也不高
• 对于queryBlockSum，采取dfs，标记在同一连通子图中的点

类图：

四、Bug及其修复

本单元第一、二次作业平安度过，但第三次作业中由于几个方法算法过于暴力、复杂度较高，导致强测和互测爆炸。
对于这种tle类型的错误，修复起来感觉尤其棘手，因为优化算法绝对不是5行代码能解决的事，不知道大规模改动审核会不会通过。针对超时的问题，目前打算从两方面优化：1.queryMinPath：原本的方法中是找到了所有的距离后才结束，实际上dijkstra算法某一点出列后算出的距离就是最短路径，也就是说找到目标点后即可退出；2.queryStrongLinked：这个方法原本写得我自己都有些看不下去，修复bug使用tarjan是一个方向。

五、心得体会

????本单元我个人对JML的理解是不断变化的。第一次作业的JML规格很容易理解，实际上即使不细想规格的内容照着描述也能写出函数，颇有一种os看着注释补函数的感觉，那时我以为JML就是对java实现过程的一个规格化，即将实现过程用一个标准的语言描述出来，有了JML就能照着写出程序。后来的作业中发现，其实JML对于具体的实现方法限制很小，具体编写主要看自己，这时JML给我编写程序(具体实现过程)的帮助就不那么大了，甚至直接照着JML写有超时风险。感觉它更多的是一种限制作用，即要求编写出来的程序应该满足什么前提、过程和结果满足什么条件等等。这样的话理解JML就十分重要。有了JML的话对于程序的测试也可以依照规格进行，检验执行方法后是否满足各种条件。
????除此之外，感觉最深的就是体验到了真正的离散和数据结构课程。不过还是想吐槽一句作业的重点是不是偏离了。因为即使是后两次作业中，要想理解JML的意图还是较容易的，大家几乎都能理解方法作用和满足条件，倒是在算法方面讨论比较激烈，个人感觉这对于JML的学习帮助不是很明显。感觉作业可以从一些比较复杂的JML规格入手，或者是进行JML规格编写的作业练习(在书写这方面确实感觉还有不足之处)。不过依然要感谢课程组，这单元个人收获还是很大的，不仅学到了JML，也明白了离散数学和算法对于编写程序的重要意义，日后的学习中会更加重视基础，脚踏实地。