一.JML基础
二.部署JMLUnitNG/JMLUnit并应用
三.梳理架构及Bug分析
四.心得体会
? JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言
? （1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
? （2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
? <1>注释结构。每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式为 //@annotation ，块注释的方式为 /* @ annotation @*/ .
? <2>JML表达式。
? a.原子表达式:
\result表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值
\old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值
? b.量化表达式
forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束
\sum表达式：返回给定范围内的表达式的和
? c.集合表达式
? 集合构造表达式：可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素
? d.操作符
(1) 子类型关系操作符： E1<:E2 ，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假
(2) 等价关系操作符： b_expr1<==>b_expr2 或者 b_expr1<=!=>b_expr2 ，其中b_expr1和b_expr2都是布尔表达式，这两个表达式的意思是 b_expr1==b_expr2 或者 b_expr1!=b_expr2
(3) 推理操作符： b_expr1==>b_expr2 或者 b_expr2<==b_expr1 。对于表达式 b_expr1==>b_expr2 而言，当b_expr1==false ，或者 b_expr1==true 且 b_expr2==true 时，整个表达式的值为 true 。
(4) 变量引用操作符：除了可以直接引用Java代码或者JML规格中定义的变量外，JML还提供了几个概括性的关键词来
引用相关的变量。\nothing指示一个空集；\everything指示一个全集，即包括当前作用域下能够访问到的所有变
量。
? d. 方法规格
(1)前置条件通过requires子句来表示： requires P; 。其中requires是JML关键词，表达的意思是“要求调用者确保P为真”。
(2)后置条件通过ensures子句来表示： ensures P; 。其中ensures是JML关键词，表达的意思是“方法实现者确保方法执行返回结果一定满足谓词P的要求，即确保P为真”
(3)副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。从方法
规格的角度，必须要明确给出副作用范围。JML提供了副作用约束子句，使用关键词 assignable 或者
modifiable
(4)signals子句的结构为 signals (Exception e) b_expr ，意思是当 b_expr 为 true 时，方法会抛出括号中给出的相应异常e。
? e.类型规格
(1)不变式（invariant）是要求在所有可见状态下都必须满足的特性，语法上定义 invariant P ，其中 invariant 为关键词， P 为谓词
(2对象的状态在变化时往往也许满足一些约束，这种约束本质上也是一种不变式。JML为了简化使用规则，规定
invariant只针对可见状态(即当下可见状态)的取值进行约束，而是用constraint来对前序可见状态和当前可见状态的
关系进行约束
1.OpenJML.可以编译含有jml注释的代码，在运行生成的类时，会自动检查是否符合jML规格的要求，不符合时会抛出断言进行提示
2.SMT Solver。能够对代码进行静态检查以判断是否符合jml规格的要求
3.JMLUnit。可根据JML规格自动生成测试用例
安装好JMLUnitNG后，在本地编写好测试函数：
测试结果：
第一次作业：
根据指导书所言，写了Main，myPath，MyPathContainer三个类，这一次作业相对简单，无论是类的复杂度还是方法的复杂度都偏低。主要的思路是在每add或者remove一条路径时，就计算出容器类有多少个不同的点这种以后需要查询的信息，将查询指令所花的时间分摊到数量较少的add及remove等指令中去。
这一次作业比较简单，没有Bug
第二次作业：
第二次作业内路径新增了查询两个点之间的连通性和两点间的最短路等查询指令，因此在上一次作业的基础上，每add或者remove一条路径时，用floyd算法遍历出任意两点间的最短路径长度，并记录在一个数组当中。当然需要对节点做一个映射，节点的编号在整数范围内，但节点个数却是保证在200多个以内，因此需再用一个hashmap加以映射。
第三次作业没能进强测，就不说了
经过这一单元的训练，我对jml已有了一定程度的了解，熟悉了jml的大部分语法，能够看懂已有jml规格和根据已有代码编写规格。个人感觉写jml偏麻烦，未来工作中倒不一定能够用上，但是在对精度要求极高的地方可能会用上，jml相较于用自然语言所写的注释不会产生歧义，而且通过jml规格可以采用相关的工具来自动生成测试用例也是极佳的。
原文：https://www.cnblogs.com/notorious/p/10905934.html