前言
第三单元的三次作业围绕JML语言展开，和前两个单元一样是难度递进的模式，下一次作业都是上一次作业的扩展和丰富，但是因为有了JML语言的支撑，我对规格化思想和契约式设计有了更深的感受。在理论课上听老师讲JML规格的第一反应就是照着注释写代码，应该难度不大，但是三次作业下来，发现自己了解到的实在浅薄，从JML>>code也并不轻松，借此次博客从以下几个方面对第三单元的作业进行总结与反思。
一、JML理论基础及工具链梳理
关于JML
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言 （Behavior Interface Specification Language，BISL），基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。JML引入了大量用于描述行为的结构，比如有模型域、量词、断言可视范围、预处理、后处理、条件继承以及正常行为（与异常行为相对）规范等等，这些结构使得JML非常强大。
一般而言，JML有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
Level 0语言特征
1、注释结构
每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式为 //@annotation ，块注释的方式为 /* @ annotation @*/ .
2.JML常用表达式
esult：表示一个非void类型的方法执行所获得的结果，即方法执行后的返回值。 esult表达式的类型就是方法声明中定义的返回值的类型。
old(expr)：表示表达式expr在相应方法执行前的取值。注意，如果v是一个对象，old(v)表示在方法执行前v的引用地址，并不包括v本身的内容。
forall：全称量词，可理解为“任意”，表示对于给定范围内的元素，每个元素都满足相应的约束。
exists：存在量词，表示对于给定范围内的元素，存在一个元素满足相应的约束。
othing：表示一个空集，常常在副作用中使用，assignable othing表示这个方法没有副作用。
3. 方法规格
前置条件(pre-condition) 前置条件是对方法输入参数的限制，如果不满足前置条件，方法执行结果不可预测(requires .....)
后置条件(post-condition) 后置条件是对方法执行结果的限制，如果执行结果满足后置条件，则表示方法执行正确，否则执行错误(ensures .....)
副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。从方法规格的角度，必须要明确给出副作用范围。JML提供了副作用约束子句，使用关键词 assignable 或者modifiable
signals子句的结构为 signals (Exception e) b_expr ，意思是当 b_expr 为 true 时，方法会抛出括号中给出的相应异常e
4.类型规格
不变式约束 invariant
状态变化约束 constraint
JML工具链
JML提供了许多工具，可以用于检验JML规格书写的正确性，也可以根据JML规格自动生成测试用例，工具大概有：
1. 使用OpenJML检查JML规格的正确性，提供对程序的静态和动态检查。
2. 使用SMT Solver验证代码与规格等价性。
3. 使用JMLUnitNG自动生成测试数据验证代码的正确性。
二、部署JMLUnitNG/JMLUnit
首先是Openjml 安装
- OpenJML 可以在 OpenJML 官方 github 仓库获取（官方网站的下载下来一直解压失败，最终采取github版）
- 解压后将.jar文件和Solover-Windows(在Windows系统下)放在同一文件夹内
- 在该文件夹下使用命令：
$ java -jar openjml.jar "$@"完成安装
安装JMLUnitNG，下载jar包后放在之前建立的文件夹中，调用命令$ java -jar jmlunitng.jar "$@"完成安装
将待测试的源程序放入上述文件夹（采用以下简单的测试程序来体验JMLUnitNG）
public class Test {
/*@ public normal_behaviour
@ ensures
esult >= num1;
@ ensures
esult >= num2;
@ ensures
esult >= num3;
*/
public static int compare(int num1, int num2, int num3) {
int max;
if (num1 > num2) {
max = num1;
}
else {
max = num2;
}
if (max < num3) {
max = num3;
}
return max;
}
public static void main(String[] args) {
compare(347276,6234646, 2656435);
}
}
然后执行
1）$ java -jar jmlunitng.jar test/Test.java
2）$ javac -cp jmlunitng.jar test/*.java
3）$ java -jar openjml.jar -rac test/Test.java
4）$ java -cp jmlunitng.jar test.Test_JML_Test
此时文件为：
运行结果为：
从运行结果可以看出，JMLUnitNG自动生成的测试用例主要测试一些极端情况，比如0，最大值，最小值，这样可以确定测试文件在边缘情况的安全性。总的来说，JMLUnitNG还是比较可靠的自动化测试工具，可以帮助我们提高程序的准确性，但是我感觉JMLUnitNG的使用并不特别方便，都是命令行操作，在测试的过程中很容易报错，或许掌握熟悉了还是很值得利用的工具。
三、作业回顾
第一次作业
第一次作业是
第一次作业总的来说比较简单，基本上是按照规格来实现代码，只是在第一次实现时，我采用的是Arraylist来存储数据，后来改成了两个Hashmap实现id和path的对应，并将复杂度分摊到了add和remove方法，从复杂度分析也可看出MyPathContainer2要优于MyPathContainer1。第一次作业让我对java数据结构中的容器有了更深的理解，比如hashcode和equal的重写以及各类容器增删查改的复杂度，虽然难度不大，但是收获还是挺多的。
公测及互测bug分析
第一次作业比较友好，主要是为之后的作业铺垫，在公测及互测中未发现bug。
第二次作业
第二次作业
度量分析
第二次作业延续了第一次作业的设计，在图的实现里用的是邻接表（从度量分析可以看出算法复杂度比较高），计算最短距离的时候采用了dijkstra算法(第二次作业让我有一点数据结构还债的感觉，去年的图学得不好，借这个机会也再学习了一波)。
公测及互测bug分析
第二次作业在强测和互测中出现了TLE（cputime 和 realtime），看代码感觉原因有两个，一个是dij算法写得复杂了，第二个是add和remove中都有遍历pathcontainer来确定是否加减边的循环，后来尝试了广度优先算法（果然比dij快）。
第三次作业
第三次作业需要完成的任务是实现容器类Path，地铁系统类RailwaySystem，学习目标为JML规格进阶级的理解和代码实现、设计模式和单元测试的进阶级实战。
度量分析
第三次作业相较第二次作业增加了创造图的过程，在讨论区同学的指导下把计算最低票价，最少换乘次数，最少不满意度，最短路径都转换成了求最短路径问题，Graphmake里面计算并存储了四个权值不同的图（采用邻接矩阵），并且将计算的部分全部放在add和remove，当需要查找值的时候仅需要通过邻接矩阵获取值。在写的过程中需要注意的是对每条path也需要求一次最短路径，再进行整个图的计算。
公测及互测bug分析
在公测和互测中未发现bug，但是代码写得实在不好看，还有很大改进的地方（感谢大佬的评测机！！）。
四、心得体会
通过一个单元JML的练习，能明显的感受到代码在往严谨可读可交流的方向发展，模块化的思想也体现地越来越清晰。如果直接让我实现地图系统，我可能就不会有从path到pathcontainer到graph到railwaysystem的一层层分割功能的意识。JML描述的规格，对方法、类等程序单元进行了严格的约束，这些细致的规格，相较于自然语言，能更加规范地描述需求，减少歧义，保证开发的速度与质量，这种高效的约定对于大型工程的协同开发有很多好处，而且通过JML规格可以采用相关的工具来自动生成测试用例也是很有保障的。
这三次作业给我更深的感受是在实现基本功能之后，必须要考虑的事情是如何优化，功利一点地说，是要保障稳过强测，长远一点说，是要为以后的工程开发打好基础。JML规格并没有限制对象内部的结构，只是限定了必须满足的条件和结果，应该在满足规格的条件下尽可能用高效的数据结构和算法来实现需求。（此处应该感谢讨论区中热情分享的同学！！！）
这一单元主要训练了根据规格实现代码的能力，实验课上根据代码写规格感觉也不轻松，有很多拿不准的描述，更不要说根据需求撰写规格了，在这个方面还有很大很大的不足。
道阻且长。