JML-level0

注释结构

JML以javadoc注释的方式来表示规格，每行以@起头，有行注释和块注释两种方式。

1	//@ public model non_nul int [] elements

1
2
3

/*@ public model non_nul int [] elements
  @ ...
  @*/

JML表达式

原子表达式

`\result`

表示一个非void类型的方法执行所获得的结果，即方法执行后的返回值，类型为方法声明中定义的返回值类型。

`\old(expr)`

用来表示一个表达式expr在方法执行前的取值，对于一个对象引用而言只能判断引用本身是否发生变化，而不判断指向的对象实体是否发生变化，即引用是否改变所指的对象。(这的引用更像C++的指针)

例如对于HashMap类型的v而言，\old(v).size()和\old(v.size())含义不同，前者是取了v在方法执行前的对象再使用方法，如果v没有改变所指的对象的话，即使有插入删除操作，\old(v).size()和v.size()也一样，而后者是取的执行方法前的值。

因而，任何情况下都应该使用\old将关心的表达式整体括起来。

`\not_assigned(x,y,...)`

表示括号中的变量是否在方法执行过程中被赋值，没有则返回true，否则为false。一般用于后置条件的约束表示上，限制方法的实现不能对列表中的变量赋值。

`\not_modified(x,y,...)`

与上面类似，限制列表中的变量在方法执行过程中取值不变。

`\nonnullelements(container)`

表示container对象中储存的对象不会有null，等价于下面的断言

1	container != null && (\forall int i; 0 <= i && i < container.length; container[i] != null)

`\type(type)`

返回类型type对应的类型(Class)，如\type(boolean)为Boolean.TYPE，TYPE是JML采用的缩略表示，等同于Java中的java.lang.Class。

`\typeof(expr)`

返回表达式对应的准确类型，如\typeof(true)为Boolean.TYPE。

量化表达式

`\forall`

全称量词修饰的表达式，表示对给定范围内的元素，每个元素都满足相应的约束，例如

1	(\forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j])

为真(ture)则表示a数组升序排列(在[0,10))

`\exists`

存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足满足相应的约束。

`\sum`

返回给定范围内表达式的和，例如

1	(\sum int i; 0 <= i && i < 5; i * i)

返回结果为30 (0+1+4+9+16)

`\product`

返回给定范围内表达式的连乘结果。

`\max`

返回给定范围内表达式的最大值。

`\min`

返回给定范围内表达式的最小值。

`\num_of`

返回指定变量中满足相应条件的取值个数。

1 2	(\num_of T x; R(x); P(x)) (\sum T x; R(x) && P(x); 1)

R(x)为变量范围，P(x)为约束条件。

集合表达式

可以在JML中构造一个局部的集合(容器)，明确集合中可以包含的元素。

1	new JMLObjectSet {Integer i \| s.contains(i) && 0 < i.intValue()}

表示构造一个JMLObjectSet对象其中包含元素类型为Integer，该集合元素均在容器集合s中出现且为正数。(容器集合值Java中构建的容器，如ArrayList)

一般形式

1	new ST {T x \| R(x) && P(x)}

R(x)表示x的范围通常来自某个既有集合，P(x)为约束条件。

操作符

JML表达式可以正常使用Java所定义的操作符，包括运算操作符、逻辑操作符等。此外，JML定义了以下四类操作符。

子类型关系操作符 `E1<:E2`

如果类型E1是类型E2的子类型，表达式为真，否则为假。(类型相同也为真)

显然任意类X满足X.TYPE<:Object.TYPE。

等价关系操作符 `b_expr1<==>b_expr2`或者`b_expr1<=!=>b_expr2`

其中b_expr1和b_expr2都是布尔表达式，这两种运算符和Java的==、!=具有相同的效果，但等价关系操作符的优先级更低。

推理操作符 `b_expr1==>b_expr2`或者`b_expr2<==b_expr1`

相当于蕴含式，当且仅当b_expr1为真且b_expr2为假时表达式为假。

变量引用操作符

除了可以直接引用Java代码或者JML规格中定义的变量外，JML还提供了几个概括性的关键词来引用相关的变量。

\nothing表示一个空集。

\everything表示一个全集，即当前作用域下能访问到的所有变量。

变量引用操作符常在\assignable句子中使用。

方法规格

方法规格的核心分为三个方面——前置条件、后置条件和副作用。

前置条件：对方法输入参数的限制，如果不满足前置条件则方法的执行结果不可预测，或者是不保证结果的正确性。

后置条件：对方法执行结果的限制，执行结果满足后置条件则方法执行正确，否则错误。

副作用：方法在执行过程中对输入对象或者this对象进行了修改。

两类方法——全部过程和局部过程。

全部过程：前置条件恒为真，可以适应于任意调用场景。

局部过程：提供非恒真的前置条件，需要对不符合前置条件的输入情况进行处理，往往对应着异常处理。

JML区分这两种场景分别对应着正常行为规格(normal_behavior)和异常行为规格(exceptional_behavior)。

前置条件(pre-condition)

通过requires子句来表示:requires P;，表示要求调用者确保P为真。

可以有多个requires子句，是并列关系，即调用者必须满足所有子句要求。

想设计或逻辑则应使用一个requires子句，requires P1 || P2;。

后置条件(post-condition)

通过ensures子句来表示:ensures P;，表示方法实现者确保方法执行结果一定满足P的要求，即P为真。

ensures子句同样是并列关系，必须同时满足，或逻辑实现应使用一个ensures子句。

副作用范围限定(side-effects)

副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法执行带来影响，必须明确给出副作用的范围。

使用关键词assignable或者modifiable,前者表示可赋值，后者表示可修改，大部分情况下可交换使用。

约束子句有两种形态——使用JML关键词概括或者指明具体的变量列表。

public class IntegerSet{
	private /*@spec_public@*/ ArrayList<Integer> elements;
	private /*@spec_public@*/ Integer max;
	private /*@spec_public@*/ Integer min;
	/*@
	  @ assignable \nothing;
	  @ assignable \everything;
	  @ modifiable \nothing;
	  @ modifiable \everthing;
	  @ assignable elements;
	  @ modifiable elements;
	  @ assignable elements, max, min;
	  @ modifiable elements, max, min;
	  @*/
}

JML不允许在副作用约束子句中指定规格声明的变量数据，因为这样的声明只是为了描述规格，并不意味实现者一定要实现这样的数据。

默认情况下，方法的规格对调用者可见，但是方法所在类的成员变量一般都声明为private,对调用者不可见。有时方法规格不得不使用类的成员变量来限制方法的行为，比如上面例子中的副作用范围限定，这就和类对相应成员变量的私有化保护产生了冲突。为了解决这个问题，JML提供了/@spec_public@/来注释一个类的私有成员变量，表示在规格中可以直接使用，从而调用者可见。

对于某些纯粹访问性的方法，不会对对象状态进行修改也不需要输入参数，这样的方法无需描述前置条件也不会有副作用，且一定能正常结束，可以使用pure关键词描述其规格。

public /*@ pure @*/ String getName();

//@ ensures \result == bachelor || \result == master;
public /*@ pure @*/ int getStatus();

//@ ensures \result >= 0;
public /*@ pure @*/ int getCredits();

在方法规格中可以引用pure方法返回的结果。

/*@ requires c >= 0;
  @ ensures getCredits() == \old(getCredits()) + c;
  @*/
public void addCredits(int c);

为了有效的区分方法的正常功能行为和异常行为，JML提供了这两类行为的区分机制，可以明确按照这两类行为来分别描述方法的规格，如下所示：

/*@ public normal_behavior
  @ requires z <= 99;
  @ assignable \nothing;
  @ ensures \result > z;
  @ also
  @ public exceptional_behavior
  @ requires z < 0;
  @ assignable \nothing;
  @ signals (IllegalArgumentException e) true;
  @*/
public int cantBeSatisfied(int z) throws IllegalArgumentException；

其中public normal_behavior表示接下来的部分对cantBeSatisfied(int z)方法的正常功能给出规格。所谓正常功能，一般指输入或方法关联this对象的状态在正常范围内时所指向的功能。与正常功能相对应的是异常功能，即public exceptional_behavior下面所定义的规格。

其中的public指相应的规格在所在包范围内的所有其他规格处都可见。

需要说明的是，如果一个方法没有异常处理行为，则无需区分正常功能规格和异常功能规格，因而也就不必使用这两个关键词。

上面例子中出现了一个关键词also，它的意思是除了正常功能规格外，还有一个异常功能规格。需要说明的是，按照JML语言规范定义，有两种使用also的场景:

父类中对相应方法定义了规格，子类重写了该方法，需要补充规格，这时应该在补充的规格之前使用also。
一个方法规格中涉及多个功能规格描述，正常功能规格或者异常功能规格，需要使用also来分隔。

作为一种重要的设计原则，同一个方法的正常功能前置条件和异常功能前置条件一定不能有重叠。对于上面的例子而言，如果正常功能前置条件修改为 z>=0 就能满足这个要求。可以看出不论是正常功能规格，或者是异常功能规格，都包括前置条件、后置条件和副作用声明。不同的是，异常功能规格中，后置条件常常表示为抛出异常，使用signals子句来表示。

signals

signals子句的结构为signals (***Exception e) b_expr，意思是当b_expr为真时，方法抛出括号中给出的相应异常e。

抛出的异常既可以是Java预先定义的异常类型，也可以是用户自定义的异常类型。

如果一个方法在运行时会抛出异常，一定要在方法声明中明确指出(使用Java的throws表达式)，且必须确保signals子句中给出的异常类型一定等同于方法声明中给出的异常类型，或者是后者的子类型。

还有一个简化的signals子句，即signals_only子句，后面跟着一个异常类型。signals子句强调在对象状态满足某个条件时会抛出符合相应类型的异常；而signals_only则不强调对象状态条件，强调满足前置条件时抛出相应的异常。

有时，为了更明显地区分异常，会针对输入参数的取值范围抛出不同的异常，从而提醒调用者进行不同的处理。这时可以使用多个exceptional_behavior：

public class Student {
	//@ public model non_null int[] credits;
	/*@ normal_behavior
	  @ requires z >=0 && z <= 100;
	  @ assignable \nothing;
	  @ ensures \result == credits.length;
	  @ also
	  @ exceptional_behavior
	  @ requires z < 0;
	  @ assignable \nothing;
	  @ signals_only IllegalArgumentException;
	  @ also
	  @ exceptional_behavior
	  @ requires z > 100;
	  @ assignable \nothing;
	  @ signals_only OverFlowException;
	  @*/
public int recordCredit(int z) throws IllegalArgumentException,
OverFlowException;
}

需要指出的是，在异常功能规格中，除了抛出异常，也一样可以正常使用ensures子句来描述方法执行产生的其他结果。

类型规格

类型规格是针对Java程序中定义的数据类型所设计的限制规则。一般而言，就是针对类或接口所设计的约束规则。

从面向对象角度来看，类或接口包含数据成员和方法成员的声明及（或）实现。不失一般性，一个类型的成员要么是静态成员(static member)，要么是实例成员(instance member)。一个类的静态方法不可以访问这个类的非静态成员变量(即实例变量)。静态成员可以直接通过类型引用，而实例成员只能通过实例化对象来引用。因此，在设计和表示类型规格时需要加以区分。

JML针对类型规格定义了多种限制规则，本课程主要涉及两类——不变式限制(invariant)和约束限制(constraint)。无论哪种，类型规格都是针对类型中定义的数据成员的限制规则，一旦违反就称相应的状态有错。

不变式

要求在所有**可见状态(visible state)**下都必须满足的特性，语法上定义为invariant P，P为谓词。

可见状态一般指在特定时刻下对一个对象状态的观察，下述对象o的状态都是可见状态:

对象的有状态构造方法（用来初始化对象成员变量初值）的执行结束时刻
在调用一个对象回收方法（finilize方法）来释放相关资源开始的时刻
在调用对象o非静态、有状态方法（non-helper）的开始和结束时刻
在调用对象o对应的类或父类的静态、有状态方法的开始和结束时刻
在未处于对象o的构造方法、回收方法、非静态方法被调用过程中的任意时刻
在未处于对象o对应类或者父类的静态方法被调用过程中的任意时刻

凡是会修改成员变量(包括静态和非静态)的方法执行期间，对象的状态都是不可见的(其本质原因是对象的状态修改未完成，此时观察到的状态可能不完整)。

类型规格强调在任意可见状态下都要满足不变式。

public class Path{
	private /*@spec_public@*/ ArrayList <Integer> seq_nodes;
	private /*@spec_public@*/ Integer start_node;
	private /*@spec_public@*/ Integer end_node;
	/*@ invariant seq_nodes != null &&
	  @ seq_nodes[0] == start_node &&
	  @ seq_nodes[seq_nodes.legnth-1] == end_node &&
	  @ seq_nodes.length >=2;
	  @*/
}

一个类可以包括多个不变式，相互独立。

不变式中可以直接引用pure状态方法。

对应类成员变量有静态和非静态之分，JML也区分两类不变式，静态不变式(static invariant)和实例不变式(instance invariant)。其中静态不变式只针对类中的静态成员变量取值进行约束，实例不变式则可以针对静态成员变量和非静态成员变量的取值进行约束。可以在不变式定义中明确使用instance invariant或者static invariant来表示不变式的类别。

状态变化约束

对象的状态在变化时往往也满足一些约束，这种约束本质上也是一种不变式。JML为了简化使用规则，规定invariant只针对可见状态（即当下可见状态）的取值进行约束，而使用constraint来对前序可见状态和当前可见状态的关系进行约束，如下例：

public class ServiceCounter{
	private /*@spec_public@*/ long counter;
	//@ invariant counter >= 0;
	//@ constraint counter == \old(counter)+1;
}

invariant和constraint可以直接被子类继承获得。

和不变式一样，JML也根据类的静态成员变量区分了两类约束：static constraint和instance constraint。

注释结构

JML表达式

原子表达式

\result

\old(expr)

\not_assigned(x,y,...)

\not_modified(x,y,...)

\nonnullelements(container)

\type(type)

\typeof(expr)