标签：参考 提高 针对 不能 values 总结 返回 重点 副作用
JML，即Java Modeling Language，是一种对Java程序进行规格化设计的表示语言。其用处主要有：1.开发时做出规格化设计，以便代码编写者实现；2.方便根据规格化描述开展对应的测试；3.针对已经实现的代码，编写对应规格以提高代码可维护性。
JML主要以javadoc的方式来表示规格，每行以@起头，分为行注释//@xxxxx和块注释/*@ xxxxx @*/两种。
\result:表示一个非void的方法执行后的返回值。\old(expr):表示一个表达式expr在执行相应方法前的取值\not_assigned(x, y, ...):表示括号内的变量在方法执行过程中是否被赋值。没有被赋值则返回true；否则返回false\not_modified(x, y, ...):类似not_assigned，区别是表示变量取值是否变化\type(type):返回类型type对应的Class\forall:全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应约束\exists:存在量词修饰的表达式，表达对于给定范围内的元素，存在某个元素满足相应的约束\sum:返回给定范围内的表达式的和\max和min:分别返回给定范围内表达式的最大和最小值E1 <: E2:子类型关系操作符，如果类型E1是类型E2的子类型或同类型(sub type)，则该表达式的结果为真，否则为假b_expr1<==>b_expr2:等价关系操作符b_expr1==>b_expr2:推理操作符\nothing指示一个空集；\everything指示一个全集requires P，即要求确保条件P为真ensures P，即要求确保方法执行返回结果一定满足谓词Passignable和modifiable，分别表示可赋值、可修改invariant P具体部署过程见下
OpenJML主要是用于对JML进行检查的。这一工具的使用参考了一位学长的博客(十分感激这位学长，看了博客以后省去了不少时间)。下载了OpenJML工具后，编写一个脚本，添加到环境变量里就可以直接使用命令行操作。先随便写一个有语法错误的JML规格来进行检测：
public class test {
/*@
@ requires a >= 0 && b >= 0 2333;
@ ensures \result == (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只是单纯不支持这个。
JMLUnitNG是一种针对类自动生成测试文件的工具。听起来很方便，很自动化，但部署过程实在一言难尽...耗时又耗力，其中总是报各种错误，好在最后还是能勉强使用了
package test;
public class Test {
/*@ public normal_behaviour
@ ensures \result == 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：进行测试，结果如下：
一些使用注意事项：
由上述结果可以看出，JMLUnitNG主要是通过构造一些边界数据，比如0、+-231-1和null这种数据，来检验方法是否正确。不可否认的是对于一些简易的数值处理类方法，JMLUnitNG可以在短时间内对于边界情况进行排查检验，但说实话，这个工具用起来还是有些鸡肋(也有一部分原因可能是自己没钻研透)，就本次作业而言，数据大都是限定在一定范围内，检查边界数据可能用处不是特别明显，而且面对一些复杂的方法使用起来可能不是那么便利。除此之外，部署麻烦也从第一步开始就劝退了不少人使用。不过本人目前对这个工具也只是一知半解，如果日后还能接触JML的话还是有继续学习使用它的必要(下次一定)
第一次作业是对JML规格的一个入门，目标为实现一个社交关系模拟系统。需要实现的是Person和Network两个类，根据JML实现相应的方法。
ArrayListisCircle通过BFS实现，从id1开始，搜索到id2立即返回true类图：
整体结构并不复杂，三个类即可实现
第二次作业增加了一个Group类，同时Network增加了几个与group交互的方法。
getRealationSum、getValueSum，设置缓存，每次向group中添加人或者添加关系时更新这些缓存，调用时直接返回类图：
总体来说比上一次内容多了一点，但实现并不困难。在做第二次作业的过程中发现方法的具体实现不能过于依赖JML的描述，否则有超时的风险，只要保证JML的前置、后置条件和相关的约束，实现方式与JML描述不同也可以。
第三次作业增加了求最短路径、连通分量个数以及其他一些方法，最大的不同在于与离散数学知识联系了起来，对于算法的要求提高了不少
queryMinPath方法，采用堆优化的dijkstra算法。为此新创建了一个edge类，重写了compareTo方法，存入优先队列保证队首是最短的边queryStrongLinked，方法很暴力，使用dfs，第一次dfs找出所有路径，记录路径上的所有点；第二次枚举这些点，检验将其删去是否影响连通性。虽然实现容易，但最终效率也不高queryBlockSum，采取dfs，标记在同一连通子图中的点类图：
本单元第一、二次作业平安度过，但第三次作业中由于几个方法算法过于暴力、复杂度较高，导致强测和互测爆炸。
对于这种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，也明白了离散数学和算法对于编写程序的重要意义，日后的学习中会更加重视基础，脚踏实地。
标签：参考 提高 针对 不能 values 总结 返回 重点 副作用
原文地址：https://www.cnblogs.com/xcw011010/p/12919627.html
