JML语言的理论基础、应用工具链
前言
JML是用于对java程序进行规格化设计的一种表示语言。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，而且能够以静态方式来检查代码实现对规格的满足情况。
理论基础
注释结构、
通过使用javadoc注释的形式表示规格，每行以@起头，包括行注释和块注释两种表示方式。
JML表达式
JML表达式是对java表达式的扩展，新增了一些操作符和原子表达式，但同样有优先级顺序的规定。
原子表达式
\result表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
\old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。
\not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。
\not_modi?ed(x,y,...)表达式：与上面的\not_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取值未发生变化。
\nonnullelements( container )表达式：表示 container 对象中存储的对象不会有 null 。
\type(type)表达式：返回类型type对应的类型(Class)，如type( boolean )为Boolean.TYPE。
\typeof(expr)表达式：该表达式返回expr对应的准确类型。
量化表达式
\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
\sum表达式：返回给定范围内的表达式的和。
\product表达式：返回给定范围内的表达式的连乘结果。
\max表达式：返回给定范围内的表达式的最大值。
\min表达式：返回给定范围内的表达式的最小值。
\num_of表达式：返回指定变量中满足相应条件的取值个数。
操作符
子类型关系操作符： E1<:E2 ，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。如 果E1和E2是相同的类型，该表达式的结果也为真，如 Integer.TYPE<:Integer.TYPE 为真；但 Integer.TYPE<:ArrayList.TYPE 为假。需要指出的是，任意一个类X，都必然满足 X.TYPE<:Object.TYPE 。
等价关系操作符： b_expr1<==>b_expr2 或者 b_expr1<=!=>b_expr2 ，其中b_expr1和b_expr2都是布尔表达 式，这两个表达式的意思是 b_expr1==b_expr2 或者 b_expr1!=b_expr2 。可以看出，这两个操作符和Java中的 == 和 != 具有相同的效果，按照JML语言定义， <==> 比 == 的优先级要低，同样 <=!=> 比 != 的优先级低。
推理操作符： b_expr1==>b_expr2 或者 b_expr2<==b_expr1 。对于表达式 b_expr1==>b_expr2 而言，当 b_expr1==false ，或者 b_expr1==true 且 b_expr2==true 时，整个表达式的值为 true 。
变量引用操作符：除了可以直接引用Java代码或者JML规格中定义的变量外，JML还提供了几个概括性的关键词来 引用相关的变量。\nothing指示一个空集；\everything指示一个全集，即包括当前作用域下能够访问到的所有变 量。变量引用操作符经常在assignable句子中使用，如 assignable \nothing 表示当前作用域下每个变量都不可以 在方法执行过程中被赋值。
方法规格
前置条件
前置条件通过requires语句表示，要求调用者确保被调用条件为真。
后置条件
后置条件通过ensures语句表示，要求方法实现者确保返回结果满足所定义条件的要求。
副作用范围限定
通过使用assignable或者modifiable关键词定义副作用约束语句，限定次方法执行对后续方法执行产生的影响范围。
类型规格
类型规格指针对Java程序中定义的数据类型所设计的限制规则，一般而言，就是指针对类或接口所设计的约束规则。 从面向对象角度来看，类或接口包含数据成员和方法成员的声明及或实现。
原文：https://www.cnblogs.com/DoubleRider/p/10906817.html