JML语言概述（Level 0）
概念定义
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。
由上述定义可知，JML诞生的初衷就是对代码进行形式化描述，试图在用自然语言表达的需求与用代码语言表达的实现之间构建一座桥梁，一方面可以消除自然语言可能存在的歧义与模糊，另一方面也可以屏蔽具体的代码实现，实现另一种形式的抽象。
JML基本语法
| 含义 | |
|---|---|
| \result | 方法的返回值（非void类型） |
\old(expr) |
表达式expr在方法执行前的取值 |
| \not_assigned(x, y, ...) | 括号中的变量是否在方法执行过程中未被赋值 |
| \not_modified(x, y, ...) | 限制括号中的变量在方法执行期间的取值未发生变化 |
| (\forall T x; R(x); P(x)) | 全称量词 |
| (\exists T x; R(x); P(x)) | 存在量词 |
(\sum T x; R(x); expr) |
返回给定范围内的表达式的和 |
(\max T x; R(x); expr) |
返回给定范围内的表达式的最大值 |
(\min T x; R(x); expr) |
返回给定范围内的表达式的最小值 |
| <==> | 等价操作符 |
| ==> | 蕴含操作符 |
| \nothing |
| 含义 | |
|---|---|
| requires | 前置条件，表达的意思是“要求调用者确保P为真”。 |
| ensures | 后置条件，表达的意思是“方法实现者确保方法执行返回结果一定满足谓词P的要求，即确保P为真”。 |
| assignable | 副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。 |
| public normal_behavior | 正常功能，一般指输入或方法关联this对象的状态在正常范围内时所指向的功能。 |
| public exceptional_behavior | 异常功能，与正常功能相对 |
| signals | 结构为signals (***Exception e) b_expr; |
| 含义 | |
|---|---|
| invariant | 不变式（invariant）是要求在所有可见状态下都必须满足的特性 |
| constraint |
JML工具链
通过上文，我们已经看到，JML在形式化描述上就语言规范来说已经非常完善了，可以说是把谓词逻辑的那一套完完整整地搬了过来，很好地保证了严谨性，也相对代码要更加易读一些。
但是！！！这里面有两个问题。
首先，JML并不对方法的复杂度有任何限制。于是我们可以看到，在某些方法里，比如addRelation()，方法本身复杂度并不高，但JML却特别长，让人看得很不耐烦，还不如直接看代码来得简洁明了；而对另一些场景，比如返回的对象比较复杂不是一个简单基本类型的话，就会出现关键字嵌套的情况，这就使得单条JML语句的复杂度也会很高，还不如拆成多行的代码看的清楚。特别地，我尤其对于如何用JML来写递归感到好奇，毕竟我依稀记得一阶逻辑似乎是不完备的哦？
所以这时候可能就有人会说，JML不是写给程序员看的，程序员看代码就好了。那么问题又来了，JML的理想服务对象是谁呢？是掌握谓词逻辑的产品经理？不过，如果真是这样，那我也可以接受。但似乎，JML工具链却为我们指出了另一个潜在服务对象：机器。
简单来说，JML工具链似乎就是为了能够让机器基于规格以形式化验证的方式来代替人类对方法进行完备的测试而诞生的。怎么说呢，光是看这句话就挺心疼人家机器的——这要求也忒高了吧。别说AI了，就是人，你能保证他做到绝对完备吗？他能考虑到一个顾客进来问现在几点了这种操作吗？
为什么说让机器来代替人类进行测试是不现实的呢？很简单，因为机器也是人造的，要想实现基于形式化语言的可泛化测试，而不基于具体的需求本身，就意味着你必须要仅仅凭借上面的那些关键字，就能枚举出它们所有潜在可能组合，而且这个组合中的每一种情况所包含的测试样例还必须是有穷，有阶梯性的。你觉得，如果我随手写一行一阶谓词逻辑，你有信心告诉我这玩意的所有边界情况吗？更何况，你知道的只是一个谓词集合呢？
或许，可能开发者的初衷是只要我把每个前置条件与后置条件还有副作用写清楚，机器针对不同的behavior生成不同的测试样例这样。但是，需要特别指出的是，同一个requires语句下的不同的边界数据才是构造测试的关键，特别是面对非欧拓扑模型（很不巧，我们的Unit3就长这样）。
所以啊，别难为人家开发者和机器了。指望靠JML工具实现自动测试还是等到强AI出来并且还没来得及毁灭人类的时候吧。
吐槽到此结束，对于JML工具链的具体介绍，请参见这个传送门。下文仅涉及openjml与JMLUnitNG的极少数方法。
OpenJML形式化验证
openjml是目前相对较为完备的一套形式化验证Kit，但是遗憾的是它在jdk1.8之后就停止更新了，于是对于我这个一开始用jdk12.0的人就很不友好（上来就把人劝退的那种）。
下面我们以task2中的实例化类RealNetwork为例，演示该工具的使用与其相应结果。假设IDEA项目所在目录为$PATH。
Parsing and Type checking
运行命令：
java -jar openjml.jar -check $PATH\src\network\RealNetwork.java -sourcepath $PATH\src -encoding utf-8
程序正常返回，无任何报错信息。
Extended Static Checking
运行命令：
java -jar openjml.jar -prover z3_4_7 -exec .\Solvers-windows\z3-4.7.1.exe -esc $PATH\src\network\RealNetwork.java -sourcepath $PATH\src -encoding utf-8
其中，-prover参数用于指定Solver类型，-exec参数用于指定Solver可执行程序，-esc参数指定检查类型为Extended Static Checking。
注: Not implemented for static checking: ensures clause containing \not_assigned
错误: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can. Reason: Internal exception: class java.lang.NullPointerException
警告: The prover cannot establish an assertion (ExceptionalPostcondition:
警告: Associated declaration:
警告: The prover cannot establish an assertion (UndefinedCalledMethodPrecondition:
警告: Precondition conjunct is false:
错误: ESC could not be attempted because of a failure in typechecking or AST transformation: queryNameRank
至于为什么只找到2个错误，我也不知道
总之，给人一种不明觉厉的感觉吧。（输出信息有近450行，我就不放了）
Runtime Assertion Checking
运行命令：
java -jar openjml.jar -rac $PATH\src\network\RealNetwork.java -sourcepath $PATH\src -encoding utf-8
其中，-rac参数指定检查类型为Runtime Assertion Checking。
运行结果如下：
1 The operation symbol ++ for type java.lang.Object could not be resolved 2 org.jmlspecs.openjml.JmlInternalError: The operation symbol ++ for type java.lang.Object could not be resolved 3 at org.jmlspecs.openjml.JmlTreeUtils.findOpSymbol(JmlTreeUtils.java:291) 4 at org.jmlspecs.openjml.JmlTreeUtils.findOpSymbol(JmlTreeUtils.java:282) 5 at org.jmlspecs.openjml.JmlTreeUtils.makeUnary(JmlTreeUtils.java:739) 6 at com.sun.tools.javac.comp.JmlAttr.createRacExpr(JmlAttr.java:4465) 7 at org.jmlspecs.openjml.ext.QuantifiedExpressions$QuantifiedExpression.typecheck(QuantifiedExpressions.java:214) 8 at com.sun.tools.javac.comp.JmlAttr.visitJmlQuantifiedExpr(JmlAttr.java:4070) 9 at org.jmlspecs.openjml.JmlTree$JmlQuantifiedExpr.accept(JmlTree.java:2685) 10 at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:577) 11 at com.sun.tools.javac.comp.Attr.visitParens(Attr.java:2995) 12 at com.sun.tools.javac.tree.JCTree$JCParens.accept(JCTree.java:1661) 13 at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:577) 14 at com.sun.tools.javac.comp.Attr.attribExpr(Attr.java:619) 15 at com.sun.tools.javac.comp.JmlAttr.attribExpr(JmlAttr.java:6209) 16 at com.sun.tools.javac.comp.JmlAttr.visitJmlMethodClauseExpr(JmlAttr.java:3117) 17 at org.jmlspecs.openjml.JmlTree$JmlMethodClauseExpr.accept(JmlTree.java:2332) 18 at com.sun.tools.javac.comp.JmlAttr.visitJmlSpecificationCase(JmlAttr.java:3361) 19 at org.jmlspecs.openjml.JmlTree$JmlSpecificationCase.accept(JmlTree.java:2837) 20 at com.sun.tools.javac.comp.JmlAttr.visitJmlMethodSpecs(JmlAttr.java:3423) 21 at org.jmlspecs.openjml.JmlTree$JmlMethodSpecs.accept(JmlTree.java:2539) 22 at com.sun.tools.javac.comp.JmlAttr.checkMethodSpecsDirectly(JmlAttr.java:1560) 23 at com.sun.tools.javac.comp.JmlAttr.visitMethodDef(JmlAttr.java:1121) 24 at com.sun.tools.javac.comp.JmlAttr.visitJmlMethodDecl(JmlAttr.java:6053) 25 at org.jmlspecs.openjml.JmlTree$JmlMethodDecl.accept(JmlTree.java:1261) 26 at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:577) 27 at com.sun.tools.javac.comp.Attr.attribStat(Attr.java:646) 28 at com.sun.tools.javac.comp.JmlAttr.attribStat(JmlAttr.java:558) 29 at com.sun.tools.javac.comp.Attr.attribClassBody(Attr.java:4378) 30 at com.sun.tools.javac.comp.JmlAttr.attribClassBody(JmlAttr.java:536) 31 at com.sun.tools.javac.comp.Attr.attribClass(Attr.java:4286) 32 at com.sun.tools.javac.comp.JmlAttr.attribClass(JmlAttr.java:414) 33 at com.sun.tools.javac.comp.JmlAttr.completeTodo(JmlAttr.java:492) 34 at com.sun.tools.javac.comp.JmlAttr.attribClass(JmlAttr.java:458) 35 at com.sun.tools.javac.comp.Attr.attribClass(Attr.java:4215) 36 at com.sun.tools.javac.comp.Attr.attrib(Attr.java:4190) 37 at com.sun.tools.javac.main.JavaCompiler.attribute(JavaCompiler.java:1258) 38 at com.sun.tools.javac.main.JmlCompiler.attribute(JmlCompiler.java:479) 39 at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:898) 40 at com.sun.tools.javac.main.JmlCompiler.compile2(JmlCompiler.java:712) 41 at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:867) 42 at com.sun.tools.javac.main.Main.compile(Main.java:553) 43 at com.sun.tools.javac.main.Main.compile(Main.java:410) 44 at org.jmlspecs.openjml.Main.compile(Main.java:581) 45 at com.sun.tools.javac.main.Main.compile(Main.java:399) 46 at com.sun.tools.javac.main.Main.compile(Main.java:390) 47 at org.jmlspecs.openjml.Main.execute(Main.java:417) 48 at org.jmlspecs.openjml.Main.execute(Main.java:375) 49 at org.jmlspecs.openjml.Main.execute(Main.java:362) 50 at org.jmlspecs.openjml.Main.main(Main.java:334) 51 错误: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can. 52 Reason: com.sun.tools.javac.code.Type$BottomType cannot be cast to com.sun.tools.javac.code.Type$ArrayType 53 java.lang.ClassCastException: com.sun.tools.javac.code.Type$BottomType cannot be cast to com.sun.tools.javac.code.Type$ArrayType 54 at org.jmlspecs.openjml.JmlTreeUtils.copyArray(JmlTreeUtils.java:1546) 55 at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitJmlMethodInvocation(JmlAssertionAdder.java:15456) 56 at org.jmlspecs.openjml.JmlTree$JmlMethodInvocation.accept(JmlTree.java:2229) 57 at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49) 58 at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67) 59 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504) 60 at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitParens(JmlAssertionAdder.java:10686) 61 at com.sun.tools.javac.tree.JCTree$JCParens.accept(JCTree.java:1661) 62 at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49) 63 at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67) 64 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504) 65 at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitBinary(JmlAssertionAdder.java:11862) 66 at com.sun.tools.javac.tree.JCTree$JCBinary.accept(JCTree.java:1785) 67 at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49) 68 at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67) 69 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504) 70 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertJML(JmlAssertionAdder.java:1647) 71 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertJML(JmlAssertionAdder.java:1664) 72 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertNoSplit(JmlAssertionAdder.java:1685) 73 at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitJmlQuantifiedExpr(JmlAssertionAdder.java:16233) 74 at org.jmlspecs.openjml.JmlTree$JmlQuantifiedExpr.accept(JmlTree.java:2685) 75 at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49) 76 at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67) 77 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504) 78 at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitParens(JmlAssertionAdder.java:10686) 79 at com.sun.tools.javac.tree.JCTree$JCParens.accept(JCTree.java:1661) 80 at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49) 81 at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67) 82 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504) 83 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertJML(JmlAssertionAdder.java:1647) 84 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertJML(JmlAssertionAdder.java:1664) 85 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertNoSplit(JmlAssertionAdder.java:1685) 86 at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitJmlQuantifiedExpr(JmlAssertionAdder.java:16233) 87 at org.jmlspecs.openjml.JmlTree$JmlQuantifiedExpr.accept(JmlTree.java:2685) 88 at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49) 89 at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67) 90 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504) 91 at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitParens(JmlAssertionAdder.java:10686) 92 at com.sun.tools.javac.tree.JCTree$JCParens.accept(JCTree.java:1661) 93 at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49) 94 at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67) 95 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504) 96 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertJML(JmlAssertionAdder.java:1647) 97 at org.jmlspecs.openjml.esc.JmlAssertionAdder.addPostConditions(JmlAssertionAdder.java:4758) 98 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertMethodBodyNoInit(JmlAssertionAdder.java:1195) 99 at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitJmlMethodDecl(JmlAssertionAdder.java:15127) 100 at org.jmlspecs.openjml.JmlTree$JmlMethodDecl.accept(JmlTree.java:1261) 101 at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49) 102 at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67) 103 at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitJmlClassDecl(JmlAssertionAdder.java:13784) 104 at org.jmlspecs.openjml.JmlTree$JmlClassDecl.accept(JmlTree.java:1174) 105 at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49) 106 at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67) 107 at org.jmlspecs.openjml.esc.JmlAssertionAdder.convert(JmlAssertionAdder.java:1414) 108 at com.sun.tools.javac.main.JmlCompiler.rac(JmlCompiler.java:610) 109 at com.sun.tools.javac.main.JmlCompiler.desugar(JmlCompiler.java:454) 110 at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:898) 111 at com.sun.tools.javac.main.JmlCompiler.compile2(JmlCompiler.java:712) 112 at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:867) 113 at com.sun.tools.javac.main.Main.compile(Main.java:553) 114 at com.sun.tools.javac.main.Main.compile(Main.java:410) 115 at org.jmlspecs.openjml.Main.compile(Main.java:581) 116 at com.sun.tools.javac.main.Main.compile(Main.java:399) 117 at com.sun.tools.javac.main.Main.compile(Main.java:390) 118 at org.jmlspecs.openjml.Main.execute(Main.java:417) 119 at org.jmlspecs.openjml.Main.execute(Main.java:375) 120 at org.jmlspecs.openjml.Main.execute(Main.java:362) 121 at org.jmlspecs.openjml.Main.main(Main.java:334) 122 $PATH\src\network\RealNetwork.java:193: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression 123 return groups.get(id).getRelationSum(); 124 ^ 125 $PATH\src\network\RealNetwork.java:248: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression 126 Graph<AbstractPerson> newGraph = new Graph<>(personSet); 127 ^ 128 $PATH\src\network\RealNetwork.java:249: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression 129 return newGraph.isReachable(oriPerson, dstPerson); 130 ^ 131 $PATH\src\com\oocourse\spec2\main\Group.java:33: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression 132 @ (\sum int j; 0 <= j && j < people.length && people[i].isLinked(people[j]); 1)); 133 ^ 134 $PATH\src\com\oocourse\spec2\main\Group.java:38: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression 135 @ (\sum int j; 0 <= j && j < people.length && 136 ^ 137 $PATH\src\com\oocourse\spec2\main\Group.java:45: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression 138 @ ensures (\exists BigInteger[] temp; 139 ^ 140 1 个错误