一、梳理JML语言的理论基础、应用工具链情况
JML的语言基础主要包括JML表达式、方法规格以及类规格
1、JML表达式
(1)原子表达式
\result
\old()
\not_assigned()
\not_modified()
\nonnullelements()
\type()
\typeof()
(2)量化表达式
\forall
\exists
\sum
\product
\max
\min
\num_of
(3)操作符
子类型关系操作符 <:
等价关系操作符 <==>
推理操作符 ==>
变量应用 \nothing \everything
2、方法规格
(1)前置条件 reqquires
(2)后置条件 ensures
(3)副作用范围限定 assignable modifiable
(4)signals子句
3、类规格
(1)状态变化约束 constraint
(2)不变式 invariant