PDF《JML(Level 0)使用手册》

JML(Level 0)使用手册 JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言.

JML是一种行为接口规格语言 (Behavior Interface Speci?cation Language,BISL),基于Larch方法构建.BISL提供了对方法和类型的规格定义 手段.所谓接口即一个方法或类型外部可见的内容.JML主要由Leavens教授在Larch上的工作,并融入了Betrand Meyer, John Guttag等人关于Design by Contract的研究成果.近年来,JML持续受到关注,为严格的程序设计提供 了一套行之有效的方法.通过JML及其支持工具,不仅可以基于规格自动构造测试用例,并整合了SMT Solver等工具 以静态方式来检查代码实现对规格的满足情况. 一般而言,JML有两种主要的用法: (1)开展规格化设计.这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述,而是逻辑严格的规 格. (2)针对已有的代码实现,书写其对应的规格,从而提高代码的可维护性.这在遗留代码的维护方面具有特别重要 的意义. JML的设计考虑到了未来扩展需要,把语言分成了几个层次.其中level 0是最核心的语言特征,要求所有的JML工具 都要支持.从课程教学角度,我们仅针对level 0语言特征,选择其中最核心和最常用的一些要素进行介绍和训练.建 议同学们通过http://www.jmlspecs.org/来了解更多细节. 1. 注释结构 JML以javadoc注释的方式来表示规格,每行都以@起头.有两种注释方式,行注释和块注释.其中行注释的表示方式 为//@annotation ,块注释的方式为 /* @ annotation @*/ .按照Javadoc习惯,JML注释一般放在被注释成分的 近邻上部,如下面的例子所示.其中有效的Java代码为line1, line 3, line 15,line18和line19. package org.jmlspecs.samples.jmlrefman;

line

1 line

2 public abstract class IntHeap line

3 line

4 ? ?//@ public model non_null int [] elements;

line

5 line

6 ? ?/*@ public normal_behavior line

7 requires elements.length >= 1;

line

8 assignable \nothing;

line

9 ensures \result line

10 max int j;

line

11 0 =1 ,即IntHeap中管理着至少一个元 素;

(2)副作用范围限定,assignable列出这个方法能够修改的类成员属性,\nothing是个关键词,表示这个方法不对 任何成员属性进行修改,所以是一个pure方法. (3)ensures子句定义了后置条件,即largest方法的返回结果等于elements中存储的所有整数中的最大的那个 (\max也是一个关键词). 需要注意的是,规格中的每个子句都必须以分号结尾,否则会导致JML工具无法解析.相比较而言,largest方法的规 格复杂,而size 方法的规格则相对简略.在JML中对应着两类规格写法,前者适用于前置条件不是恒真的场景,后 者则适用于无需描述其前置条件的场景. 最后还要补充说明一下规格变量的声明.按照JML的语法,可以区分两类规格变量,静态或实例.如果是在Interface 中声明规格变量,则要求明确变量的类别.针对上面的例子,如果是静态规格变量,则声明为 //@public static model non_null int []elements ;

如果是实例规格变量,则可声明为 //@public instance model non_null int []elements . 2. JML表达式 JML的表达式是对Java表达式的扩展,新增了一些操作符和原子表达式.同样JML表达式中的操作符也有优先级的概 念.请参见JML语言手册12.3节(Expression)获得完整的优先级列表.需要提醒的是,JML相对于Java新增的表达式成 分仅用于JML中的断言(assertion)语句和其他相关的注释体.特别需要提醒,在JML断言中,不可以使用带有赋值语 义的操作符,如 等操作符,因为这样的操作符会对被限制的相关变量的状态进行修改,产生副作用. 2.1 原子表达式 \result表达式:表示一个非 void 类型的方法执行所获得的结果,即方法执行后的返回值.\result表达式的类型就是 方法声明中定义的返回值类型.如针对方法: public boolean equals (Object o) ,\result的类型是 boolean , 任意传递一个 Object 类型的对象来调用该方法,可以使用\result来表示 equals 的执行结果( true 表示 this 和o相等;