JML语言梳理

JML理论基础

JML是一种契约式设计，一种形式化java建模语言。契约式设计的核心是将代码实现和设计本身分离。设计者只考虑设计层面的问题。

注释结构

• 行注释  //@ annotation

• 块注释 /*@ annotation*/

JML表达式

原子表达式

• \result 表示非void类型的方法执行结果

• \old（expr） 表示表达式expr在相应方法执行前的取值

• \not_assigned(x,y,...) 表示括号内变量是否被赋值

• \not_modified(x,y,...) 表示括号内变量是否被修改

• nonnullelements(container) 表示container对象存储对象不会有null

• type(type) 表示type对应的类型

• typeof（expr） 返回expr对应的准确类型

量化表达式

• \forall 全称量词

• \exists 存在量词

• \sum 返回给定表达式的和

• \protect 返回给定表达式的连乘

• \max 返回给定表达式的最大值

• \min 返回给定表达式的最小值

• \num_of 返回给定变量满足条件的个数

集合表达式

• 集合构造表达式 new JMLObjectSet {Integer i | s.contains(i) && 0 < i.intValue() }

操作符

• 子类型关系操作符 E1<:E2

• 等价关系操作符 b_expr1<==>b_expr2

• 推理操作符 b_expr1==>b_expr2

• 变量引用操作符 \nothing,\everything

方法规格

• pre-condition( requires P )

• post-condition( ensures P )

• side-effects( assignable,modifiable )

• pure 关键字

• singals 子句

类型规格

• 不变式invariant

• 状态变化约束constraint

工具链

• jml-launcher (the launcher   for the graphical user interface tools).

• jml and jml-gui (the checker).

• jmlc and jmlc-gui (compile for runtime assertion checking).

• jmldoc and jmldoc-gui   (a version of javadoc that includes JML specification information).

• jmle    (compile for executing or prototyping specifications).

• jmlrac (a version of java, the VM, that   includes the bin/jmlruntime.jar file in the CLASSPATH, for   running files compiled with jmlc).

• jmlre (a version of java, the VM,   that includes the runtime support needed for executing   specifications, for running files compiled with    jmle).

• jmlspec and jmlspec-gui   (generate skeleton specification files from Java source files).

• jmlunit and jmlunit-gui   (produce unit testing code stubs for use with    JUnit).

• jtest   (combines the work of jmlc and    jmlunit)

• jml-junit (a version of   JUnit's swing user interface that   includes the bin/jmlruntime.jar and bin/jmljunitruntime.jar files   in the CLASSPATH, for running JML   and JUnit based tests on files   compiled with jmlc and test cases   generated by jmlunit).

• openJML

参考链接：http://www.eecs.ucf.edu/~leavens/JML/documentation.shtml

JMLUnitNG/JMLUnit

在同学们的帮助之下，我也体验了一把JMLUnitNG的自动化测试。

我直接采用了讨论区中大佬的java文件进行简单的测试。

 1 // demo/Demo.java
 2 package demo;
 3 ​
 4 public class Demo {
 5     /*@ public normal_behaviour
 6       @ ensures \result == lhs - rhs;
 7     */
 8     public static int compare(int lhs, int rhs) {
 9         return lhs - rhs;
10     }
11 ​
12     public static void main(String[] args) {
13         compare(114514,1919810);
14     }
15 }

具体的过程如下

1 java -jar jmlunitng.jar demo/Demo.java
2 javac -cp jmlunitng.jar demo/*.java
3 javac -cp jmlunitng.jar demo/Demo_JML_Data/*.java
4 java -jar openjml.jar -rac demo/Demo.java
5 java -cp jmlunitng.jar demo/Demo_JML_Test

可以看到JMLUnitNG自动测试几乎选取了在临界边缘的数据，即只会选取边缘值和0。并且做一些关于null和{}的测试。上述代码出现了减法溢出的问题，所以WA了三个点。

个人认为这个JMLUnitNG如果只能这样测试，而且又对JML语法要求如此严格，那它还挺划的。也就是测试其实并不算充分。

架构设计

第一次作业

架构分析

第一次作业需求简单，算是初入JML的一点小试炼。要实现的部分不算太多，针对每个方法只要读懂JML规格，完成逻辑实现即可。

需要注意的是CPU时间，三次作业都严格要求了CPU时间，这就要求了我们将查询方法的复杂度分散均摊，同时选用更好的算法实现。此次作业还没有牵扯到算法，所以只要在图结构变更时，及时更新并保存数据，保证在查询的复杂度为O（1）。

这次作业也让我切实体会了Hash的意义。

类图及复杂度分析

作业给好了框架，只要负责填充JML规格对应的方法，因此本次类图和复杂度格外可观（

第二次作业

架构分析

这一次作业在第一次作业上新增的核心问题是最短路，是否连通其实也是最短路。所以在CPU时间的要求下，我选择了无权图的BFS算法直接得到单源点的最短路径。另外增加了类似cache机制的询问方法。若询问最短路时未命中，则进行BFS算法并存储得到的结果，且在每次进行图结构变更时，更新最短路缓存区。

另外有意思的一点是，得益于大舞台巨佬的想法——采用映射机制分配静态数组。建立了一个空闲链表管理数组的索引，数组索引与真实结点进行映射，很有OS的感觉！

然而这一次的JML好像不是自己的重点，自己思考算法和实现的时间已经不再关注JML规格。我觉得我跑偏了（

类图和复杂度分析

这一次的类图还是一样的简单，复杂度还是一样的可观。也许是我最OO的一次（预示着下一次要翻车）

第三次作业

架构分析

第三次作业还是和别的单元第三次一样，都是一堆魔鬼需求。核心问题是动态权（表现在换乘模型），而且还是各种花式带权。

针对换乘的建模，是对我最大的挑战。经过了很长时间的思虑，得到了两种算法——拆点和wjy算法。拆点算法把换乘点全部分离，这样就把动态权转化成为了静态权，然后归约到最短路径算法。但是耐不住我觉得wjy算法惊为天人，而且貌似更好实现，所以还是采用了wjy算法（wjynb！）

这个算法的最大问题在于建图，我尝试了很多方法来贪CPU时间，结果到最后都失败了。所以最终还是采取了直接Floyd全图莽的莽夫算法。每次图结构变更，就对全图进行重构，再Floyd出各种权的最短路，确保了查询的O（1）。虽然计算下来貌似我复杂度炸掉了，但是常数很小，反而跑的很快（？？？）

类图和复杂度分析

可以看到第三次作业只用了四个类，所以复杂度有点小炸，尤其是MyRailwaySystem类466行（在500行的边缘疯狂试探）。

我对于这样的规格一大起来的代码完全丧失了把控能力。可以和前两次作业做出很鲜明的对比，几乎是写了一个模块就忘记了上一个模块。能够把每个模块有效的组织起来，这也许就是OO的作用。（而我仿佛没有得到这样的灵丹妙药）

迭代中对架构的重构

三次作业下来几乎没有大型重构，只有第二次作业的BFS转换成了第三次作业的Floyd。没有重构加上我的弱鸡代码水平，最终的结果就是第三次的框架的的确确非常烂。虽然它也顺利完成了逻辑实现，但是不得不承认，我自己甚至都没有完全把控住每一个模块之间的层次关系。尤其是三种权值问题，我也没有进行抽象，只是进行了完全一致的“代码重用”。

作业中bug情况

第一次作业

强测

很不幸，虽然这一次作业真的极其简单，但是我确实在这一次作业炸掉了。这一次作业完成的过于轻松，因此几乎没有进行任何有意义的测试。最后的结果就是一个bug炸翻，强测60的美好结局（

这个bug其实是在path_add时，私心想封装一个统计结点个数的方法，结果手抖封装到了if的外面，具体代码如下。

 1 //错误示范
 2 nodeCountAdd(path);
 3 if (!containsPath(path)) {
 4     pathListInt.put(count, path);
 5     pathListPath.put(path, count);
 6     count++;
 7     return (count - 1);
 8 }
 9 //正确代码
10 if (!containsPath(path)) {
11     pathListInt.put(count, path);
12     pathListPath.put(path, count);
13     count++;
14     nodeCountAdd(path);
15     return (count - 1);
16 }

可以说一行代码，就造成了车祸级别bug，这就提醒了我

• 严格检查代码实现逻辑

• 任何情况下都不可以不做测试

互测

互测屋里估计都是一群翻车老哥，恰好碰上了五一，所以也几乎没有怎么刀人（所以我甚至没有被刀）。结果随便交个空刀却刀中了人。

具体bug都表现在compare方法上，很多同学compare会出现字典序比较错误或者溢出的问题。我认为也是测试不充分的锅。

第二次作业

强测

吃一堑长一智，老老实实测试。虽然我还是没有掌握OpenJML的使用方法（且用户体验极差）,但是和室友对拍还是简单粗暴的。果真也没有挂强测点）

且这一次本地测试也没有发现什么玄学bug，算是比较友好的一次作业。

互测

互测也没有被找出bug。

互测屋里一位同学被对拍器揪出了bug，事实上这位同学好像也被屋里的人快乐的刀了很多次。不过具体分析对拍器6000行的代码确实不好找bug。。。

第三次作业

强测

OpenJML还是没有学会，JUnit也没有用上。仍然是那个对拍器，仍然是那个室友。实名感谢一票巨佬。

这一次完成的很仓促，对拍器帮助我找到了很多bug。

• remove时没有及时更新矩阵

• 更新矩阵时遗漏了部分矩阵没有reset

• 建图时需要仅对这一部分path做Floyd再进行更新

• 缓存机制需要时刻维护信号isnew

互测

互测也没有被找出bug。

互测屋里的同学们都经受住了我对拍器的考验。但是Altergo一挑四，还是四个不同的bug，实在是tql。这也侧面说明了对拍器其实覆盖面不够。

心得体会

• JML的资料其实比较少，北航走在了时代前沿。JML是一种形式建模语言，所以追求的应该是精确的描述设计需求，杜绝自然语言的二义性问题。优秀的JML能有效将代码模块化，不会出现把控不住架构的问题。

• 写出一手优秀的JML其实比写代码还要难，而且一旦方法规模变大，JML的复杂程度甚至会超过代码本身。而且撰写JML其实对写者的挑战很大，需要有非常严密的逻辑。我认为撰写JML的核心其实是尽可能把设计思路展现出来，所以JML其实是给人看的。而不是另一种编程语言。

• JML可以给出实现设计的思路，但不是码代码指南。很多情况下，我们都不需要完全按照JML按部就班完成自己的代码。

• 这一单元的第三次作业，我对于JML就几乎没有关注，仅仅只是看了下。因为算法问题耗费了我大量的精力，虽然我确实菜，但感觉还是有些许的偏题。

• 虽然单元测试有些许麻烦，但是确实能够以覆盖面更大的形式进行测试。单纯的黑盒对拍其实完全取决于数据生成是否足够强力。

• OO方面，我还是没有很好掌握把各个模块抽象分层的能力。第三次作业，自己最直观的感受就是，所有的方法混为一谈，根本谈不上什么继承封装。我觉得自己还是不OO（，需要学习的东西太多了，实际码代码的水平也有待提高。

• 数据结构的债还是还上了。。。

• JML工具链的用户体验其实并不好，这一块由于我太菜了，所以决定自己赶快去学了。

第三单元也结束了，尽管我并不OO，但还是努力在往OO的方向追赶。

最后一单元——冲压！