JML语言理论基础
JML理论基础
Java 建模语言(JML)将注释添加到 Java 代码中，这样我们就可以确定方法所执行的内容，而不必说明它们如何做到这一点。有了 JML，我们就可以描述方法预期的功能，无需考虑实现。通过这种方法，JML 将延迟过程设想的面向对象原则扩展到了方法设计阶段。JML 为说明性的描述行为引入了许多构造。这些构造包括模型字段、量词、断言的可见度范围、前提条件、后置条件、不变量、合同继承以及正常行为与异常行为的规范。这些构造使得 JML 的功能变得非常强大。
jml方法规格
前置条件(pre-condition)
前置条件通过requires子句来表示：requires P; 。其中requires是JML关键词，表达的意思是“要求调用者确保P为真”。注意，方法规格中可以有多个requires子句，是并列关系，即调用者必须同时满足所有的并列子句要求。如果设计者想要表达或的逻辑，则应该使用一个requires子句，在其中的谓词P中使用逻辑或操作符来表示相应的约束场景：requires P1||P2; 。
后置条件(post-condition)
后置条件通过ensures子句来表示：ensures P; 。其中ensures是JML关键词，表达的意思是“方法实现者确保方法执行返回结果一定满足谓词P的要求，即确保P为真”。同样，方法规格中可以有多个ensures子句，是并列关系，即方法实现者必须同时满足有所并列ensures子句的要求。如果设计者想要表达或的逻辑，这应该在在一个ensures子句中使用逻辑或( || )操作符来表示相应的约束场景：ensures P1||P2; 。
副作用范围限定(side-effects)
副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。从方法规格的角度，必须要明确给出副作用范围。JML提供了副作用约束子句，使用关键词assignable或者modifiable。从语法上来看，副作用约束子句共有两种形态，一种不指明具体的变量，而是用JML关键词来概括；另一种则是指明具体的变量列表。
signals子句
signals子句的结构为signals (***Exception e) b_expr，意思是当b_expr为true时，方法会抛出括号中给出的相应异常e。对于上面的例子而言，只要输入满足z<0，就一定会抛出异常IllegalArgumentException。需要注意的是，所抛出的既可以是Java预先定义的异常类型，也可以是用户自定义的异常类型。此外，还有一个注意事项，如果一个方法在运行时会抛出异常，一定要在方法声明中明确指出（使用Java的throws表达式），且必须确保 signals子句中给出的异常类型一定等同于方法声明中给出的异常类型，或者是后者的子类型。
jml工具链
JML的功能十分强大，可以实现多种需求。JML可以利用JMLUnitNG 生成 TestNG 测试样例，也可以利用OpenJML进行规格正确性检查。
OpenJML
OpenJML可以实现对JML注释正确性的检查，可以用来验证编程人员写出的JML注释。（界面版的OpenJML我弄了几个小时始终没弄好，就只能用命令行版的来将就一下了）
-
运行时检查：在运行和单元测试时会发挥作用。
java -jar openjml.jar -rac test.java -
JML语法静态检查：仅检查JML是否具有语法错误。
java -jar openjml.jar -check test.java -
程序代码静态检查：仅检查代码是否有错误。
java -jar openjml.jar -esc test.java
JMLUNitNG
JMLUnitNG可以根据规格的实现自动生成TestNG测试样例。
-
基于JML生成测试文件：
java -jar jmlunitng.jar test.java -
使用OpenJML进行运行时检查
java -jar openjml.jar -rac test.java -
使用TestNG针对性测试
java -cp jmlunitng.jar:bin test_JML_Test
最后生成的测试样例
测试样例的运行结果
三次作业分析
第一次作业
第一次作业较简单，所涉及到的jml规格也比较简单。值得一提的便是为了避免超时，在数据结构的选择上要小心。我用了两个hashmap还处理pathId与path对应的关系。同时维护一个节点集合set，储存所有的不同节点。
第二次作业
第二次作业个人感觉还是比第一次难度上有一点提升。第一次和第二次相比，最关键的实现表示寻找任意两点之间的最短路。为了避免超时一直在最短路算法上纠结。但实际上因为图修改指令只占很少一部分，所以只要自己的架构方法没问题，图算法其实是次要到的。我选择的是Floyd算法。处理任意两点之间的距离加上缓存每次的结果，已经很够用了。同时第二次在第一次基础上的改动也很少，基本上就是在第一次的基础上进行添加而已。
第三次作业
UML类图
基于度量的复杂度分析
方法复杂度分析
类复杂度分析
显然，第三次作业的架构做得很差，其中一个类有将近500行代码。时间不足可能是原因之一，因为除了oo还得忙着做os，其它课程也有作业。第三次突然加入了三四个带权无向图的计算，还有时间上的限制，一开始想了很多种算法来解决，但都没有想出一种感觉合适的。大概想了一天，一行代码没打。后来还是在讨论区找到了方法。就是把每一个path中的任意两点算作是直接相连的。边权为实际边权加上换乘一次的花费。最后再用F静态数组和loyd来跑。方法比较直接，而且可以计算部分完全和第二次相同。所以有了思路之后写了大概两个多小时，而且也没发现bug。但是由于没有考虑太多架构的问题，导致写出来像用C语言在写面向过程的大作业。
三次作业bug分析
第二次公测出现了一个bug导致强测只有了65分。因为把所有节点映射到1-250，而且用一个Treeset来储存1-250个整数中已经被映射的整数，这样在每次Floyd是可以得到已经映射点的最大值，从而来限制Floyd循环计算时的最大值。原本想这样来做一些Floyd的优化，却导致在图中没有点时调用图更新算法会抛出异常。我的输出就比标准输出少了十几行。虽然我也和同学用随机数据对过拍，但是很遗憾，随机数据里没有包含图中没有节点还进行图更新算法的情况出现。互测中我也是用随机数据拿别人的代码来对拍，也只在第二次互测中测出来别人超时的bug。
心得体会
JML给人的感觉就是很高大上。就像上学期计组提到的形式验证一样。规格使得程序设计要求变得明确没有二义性，在动手写代码之前做好了规格设计的话，在动起手来写代码就会变得很简单而且直接。感觉就是水到渠成的事。不仅可以提高代码开发的效率，还可以
尽可能地保证程序的正确性。何乐而不为呢？
架构！架构！感觉自己作业架构方面做得还很不够，每每都是为了正确性而不管不顾程序的架构，当成了C语言来写。可能课下还得自己多看看别人优秀的代码，学习之后之后试着把之前的作业再重新架构一遍（至少在纸上大致写出来程序的大题思路）。否则感觉自己收获的东西真的不多了。