JML是用于对Java程序进行规格化设计的一种表示语言。通过JML及其支持工具，不仅可以基于规格自动测试用例，还整合了SMT Solver等工具以静态方式来检查代码实现对规格的满足情况。
| 表达式 | 含义 |
| \result | 非void型方法执行结果 |
| \old(expr) | 表示表达式expr在相应方法执行前的取值 |
| \not_assigned(x,y,…) | 用来表示括号中的变量是否在方法执行过程中被赋值 |
| \not_modifed(x,y,…) | 表达式限制括号中的变量在方法执行期间的取值未发生变化 |
| \nonnullelements(container) | 表示 container 对象中存储的对象不会有 null |
| \type(type) | 返回类型type对应的类型(Class) |
| \typeof(expr) | 该表达式返回expr对应的准确类型 |
| 表达式 | 含义 | 举例 |
| \forall |
全称量词修饰的表达式，表示对于给定范围内的元素， 每个元素都满足相应的约束。 |
(\forall inti,j; 0 <= i && i < j && j < 10; a[i] < a[j]) |
| \exists | 存在量词修饰的表达式 | (\existsint i; 0 <= i && i < 10; a[i] < 0) |
| \sum | 返回给定范围内的表达式的和 | (\sum int i; 0 <= i && i < 5; i) |
| \product | 返回给定范围内的表达式的连乘结果 | (\product int i; 0 < i && i < 5; i) |
| \max | 返回给定范围内的表达式的最大值 | (\max int i; 0 <= i && i < 5; i) |
| \min | 返回给定范围内的表达式的最小值 | (\min int i; 0 <= i && i < 5; i) |
| \num_of | 返回指定变量中满足相应条件的取值个数 | (\num_of int x; 0<x && x<=20;x%2==0) |
| 符号 | 含义 | 举例 |
| <: | 子类型关系操作符 |
E1<:E2 // 如果 E1是 E2的子类型或者与 E2类型相同，则返回真 |
| <==>和<=!=> | 等价关系操作符 | b_expr1<==>b_expr2 |
| ==>和<== | 推力操作符 | b_expr1==>b_expr2 |
| \nothing和\everything | 变量引用操作符 |
assignable \nothing // 当前作用域下每个变量都不可以在方法执行过程中被赋值 |
前置条件 : 对方法输入参数的限制，不满足则不能保证正确性。
后置条件 : 对方法执行结果的限制，执行后如果满足则执行正确。
副作用约定 : 指方法在执行过程中对输入对象或 this 对象进行了修改。
不变式限制：不变式是要求在所有可见状态下都必须满足的特性。
状态变化约束：对前序可见状态和当前可见状态的关系进行约束。
类图：
第一次作业功能较简单卡的也不严，我大部分功能是完全按照jml的描述写的，没有什么优化。其中isCircle方法，怕使用dfs会报栈，所以我使用的bfs。
类图：
第二次作业加入了Group接口，而且数据量非常大，许多功能如果单纯按照jml写，会产生许多o(n^2),o(n^3)的时间复杂度。这次需要好好优化了。
首先MyPerson类中，使用HashMap替换掉原来的ArrayList来存储认识的人。
MyGroup类中，有两个属性sum和xor，分别代表年龄之和、性格的异或，每次组里添加一个人，就更新这两个属性，这样在getAgeMean和getConflictSum两个方法中就可以直接返回结果，不需要进行循环了。
MyGroup类的getValueSum和getRelationSum两个方法，不可避免地要用双循环，可以优化的就是，因为这里的关系是对称的，同一个关系只算一次然后数值上乘2，相当于砍掉原来循环次数的一半。
在MyNetwork类中，也是用HashMap替换掉了原来的ArrayList来存储Person对象，提高查找效率。
类图：
第三次作业加入了一些新的方法，其中queryMinPath,queryBlockSum和queryStrongLinked较为复杂。
queryBlockSum使用并查集来进行查询，并在每次添加Person的时候更新并查集。同时之前的isCircle方法也可以使用同一个并查集，而不用再bfs了。
queryMinPath求最短路径，我使用了堆优化的dijkistra算法，并且自己写了一个MyHeap类来实现堆。
queryStrongLinked本质是判断两个点是否为点双连通。好多同学用的Tarjan算法，我Tarjan算法没看懂，最后是根据https://oi-wiki.org/graph/bcc/里面描述的判断点双连通的方法来做的，使用了一个dfs和一个并查集，倒是也通过了测试。后来研讨课上听同学讲Tarjan算法，总算听懂了，实在太巧妙了~
第一次作业没有测出bug。
第二次作业在getValueSum出现了超时的问题，原因是我用的双循环来计算，而且没有记忆功能。
修复bug时，我加了一个变量用来标记组内是否有新关系的加入，如果没有新关系的加入，getValueSum就直接返回上一次计算的值，有新关系加入才重新计算。
第三次作业新添加了delPerson方法，但我没有在方法里更新上面说的那个标记，导致一个bug。以及在queryMinPath中，dijkistra算法在松弛时，遍历了全部节点，导致超时。
因为这次输入量很少，所以解决第一个bug的办法就是去掉了getValueSum的记忆的功能。第二个bug，改为遍历与这一轮最小堆弹出的节点相连的节点。其中涉及到直接修改最小堆里节点的值的操作，会破坏最小堆的性质。由于我是手写的最小堆，所以每修改一个节点的值之后，进行上移或者下移来保持最小堆性质。
通过阅读别人的博客学习了如何配置和使用JMLUnitNG，其中需要改一些原本的JML，不然会报错。
我的工作目录：
针对MyGroup类进行测试。cd到工作目录下，依次输入以下四条指令(以及根据途中的报错修改JML)：
java -jar jmlunitng.jar test/MyGroup.java
javac -cp jmlunitng.jar test/*.java
java -jar openjml.jar -rac test/MyPerson.java test/MyGroup.java
java -cp jmlunitng.jar test.MyGroup_JML_Test
最终运行结果：
可以发现JMLUnitNG会使用一些极端数据来测试我们的程序，但是没有构造更普通和更完整的数据。其更高级的功能有待我们挖掘。
按照jml写代码，感觉效率能得到很大提升。写一个方法的时候，只需要考虑这个方法自己，以及和它关联的数据结构，而不需要同时考虑其他方法甚至整个类。只需要专心满足jml要求的内容。而且用jml来描述规格，非常严谨，不会像自然语言那样模糊，不会有二义性，干净利落脆，感觉很舒服。之后我写其他代码也打算先自己写JML，然后再具体实现代码部分。
我们现在写的代码都比较简单，如果在一个特别复杂的工程里，一串JML超级长，想要读懂它估计会有难度吧，所以我感觉要是在JML或其他形式化规格的基础上能再配合上自然语言的“注释”来方便理解，应该会更好。
原文：https://www.cnblogs.com/wangyiou/p/12943302.html