「BUAA OO Unit 3」 JML笔记

Part 0 前言

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言，对规格化设计有重要作用。这里记录Unit3中学习JML的相关笔记

Part 1 注释

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

按照javadoc习惯，JML注释一般放在被注释成分的近邻上部。

行注释

表示方式

1	//@ public model non_null int [] elements

块注释

表示方式

/*@ contents
  @
  @
  @
  @
  @
  @
  @*/

Part 2 JML表达式

`pure`

方法的执行不会有任何副作用

`model`

规格

`non_null`

数组引用对象不能为null

原子表达式

`\result`

表示一个非void类型的方法执行所获得的结果，即，方法执行后的返回值。事实上，该表达式的类型就是方法声明定义的返回值类型。

`\old(expr)`

表示一个表达式expr在相应方法执行前的取值。其遵循Java引用规则，即，针对一个对象引用，只判断引用本身是否变化，不判断引用指向的对象实体的内容是否发生变化。因此，只有当引用本身的值发生变化（即其指向了另一个对象）时，才会变化。我们应当把\old()关心的表达式取值整体括起来。

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

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

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

与\not_assigned()类似，限制括号中的变量在方法执行期间的取值不发生变化。

`\nonnullelements(container)`

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

1 2	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)`

返回expr对应的准确类型，如\typeof(false)为Boolean.TYPE。

量化表达式

`\forall`

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

举例而言，对于(\forall int i,j; 0 <= i && i <= j&& j < 10;a[i] < a[j])的意思为，对于任意0<=i<j<=10，a[i]<a[j]。这个表达式如果为真，表明数组a事实上是升序排列。

`\exists`

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

举例而言，对于(\exists int i; 0 <= i && i < 10;a[i] < 0)的意思为，对于0 <= i < 10，存在一个a[i] < 0。

`\sum`

求和表达式，返回给定范围内的表达式的和。

(\sum int i; 0<= i && i < 5;i)，意为计算 $ [0, 5) $ 范围内的整数i的和，即， $ 0 + 1 + 2 + 3 + 4 = 10 $。值得注意的是，0 <= i && i < 5是对i的范围的限制，而求和表达式是最后的那个i。

进一步说，如果表达式为(\sum int i; 0 <= i && i < 5 ; i * i)，则等价于表达式：

$\sum_{i = 0} ^ {4} {i \times i}$

`\product`

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

(\product int i;0 < i && i < 5; i)等价于：

$\prod_{i = 1}^{4}i$

`\max`

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

(\max int i; 0 <= i && i < 5;i)，这个表达式返回 $ [0, 5) $中最大的整数，即 $ 4 $ 。

`\min`

返回给定范围内的表达式的最小值，用法类似\max

`\num_of()`

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

(\num_of int x; 0 < x && x <= 20;x % 2 == 0)，这个表达式给出 $ (0,20] $中可以被 $ 2 $ 整除的整数的个数，即 $ 10 $ 。

一般而言，对于(\num_of T x; R(x); P(x)，T为变量 x的类型，R(x)为x的取值范围，P(x)定义x需要满足的约束条件。从逻辑等价角度看，事实上相当于(\num_of T x; R(x) && P(x);1)

集合表达式

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

new JMLObjectSet {Integer i | s.contains(i) && 0 < i.intValue()}表示构造一个JMLObjecti对象，包含的元素类型为Integer，集合中的所有元素都在容器集合s中出现（该容器集合指的是Java程序中构建的容器，比如ArrayList()），且整数值大于0。

集合构造表达式的一般形式为new ST{T x | R(x) && P(x)}，其中的R(x)对应集合中x的范围，通常是来自于某个既有集合中的元素，如s.has(x)，P(x)对应x取值的约束。

操作符

除了可以正常使用Java定义的操作符如算术操作符、逻辑运算操作符等，JML还定义了下面四类操作符

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

E1<:E2，如果E1是类型E2的子类型(sub type)或E1和E2是相同的类型，那么表达式的结果为真，否则为假。

举例而言，Integer.TYPE <: Integer.TYPE为真；Integer.TYPE <: ArrayList.TYPE为假。

值得注意的是，对于任何类X，都满足X.TYPE <: Object.TYPE，因为任何类都是Object的子类。

等价关系操作符`<==>`与`<=!=>`

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==false或者b_expr1==true且b_expr2==true时，整个表达式的值为true。

变量引用操作符

\nothing指示一个空集
\everything指示一个全集，即，包括当前作用域下能够访问的所有变量

变量引用操作符经常在assignable句子中使用，如assignable \nothing表示当前作用域下的每个变量都不可以在方法执行过程中被赋值。

Part 3 方法规格

方法规格的核心内容包括三方面：前置条件、后置条件和副作用约定。

前置条件：对方法输入参数的限制，如果不满足前置条件，那么方法执行结果不可预测，即，不保证方法执行结果的正确性
后置条件：对方法执行结果的限制，如果方法执行后的结果满足后置条件吉安，表明方法执行正确，否则错误
副作用：指方法在执行过程中对输入对象或this对象进行了修改（对成员变量赋值，或调用其修改方法）

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

全部过程：对应前置条件恒为真，即，可以适应任何调用场景
局部过程：提供非恒真的前置条件，要求调用者必须确保调用时满足相应的前置条件

从设计角度看，我们的软件应当能够处理用户得到所有可能输入，因此，需要对不符合前置条件的输入进行处理，这一般意味着异常处理。

从规格角度，JML区分两种场景，对应正常行为规格（normal_behavior）和异常行为规格（exceptional_behavior）

前置条件（pre-condition）

前置条件通过requires子句表示：requires P;。其中，requires是JML关键词，表达的意思是”要求调用者确保P为真“。值得注意的是，方法规格中可以有多个requires子句，为并列关系，即，调用者必须同时满足所有的并列子句要求。

如果设计者想表达或的逻辑，则应当使用一个requires子句，在其中的谓词P中使用逻辑或操作符表达相应的约束，如requires P1 || P2;。

后置条件（post-condition）

后置条件通过ensures子句表示：ensures Q;。其中，ensures是JML关键词，表达的意思是”方法实现者确保方法执行返回的结果一定满足谓词Q的要求，即，确保Q为真“。类似地，多个ensures子句是被允许的且为并列关系即须同时满足。类似地，或的表达应当在一个ensures子句中用逻辑或约束。

副作用范围限定（side-effects）

副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行造成影响。

从方法规格的角度看，必须要给出明确的副作用范围。JML提供了副作用范围子句，使用关键词assignable或者modifiable。

从语法上看，副作用约束子句有两种形态，一种不指明具体的变量，而是用JML关键词来概括；另一种指明具体的变量列表。

:chestnut::

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;
	  @*/
}

assignable表示可赋值，modifiable表示可修改。二者有一定差异，但是在大部分情况可以交换使用。

\nothing和\everything是两个关键词，前者表示当前作用域内所有可见类成员变量和方法输入对象都不可以赋值或者修改；后者表示当前作用域内可见的所有类成员变量和方法输入对象都可以赋值或者修改。也可以指明具体的可以修改的变量列表，为一个或多个变量，多个的时候需要用逗号分隔，如@assignable elements, max, min。

设计中会出现某些纯粹访问性的方法，不会对对象的状态进行任何改变，也不需要提供输入参数，这样的方法无需描述前置条件，也没有任何副作用，执行也一定会正常结束。对于这样的方法，可以使用简单的（轻量级）方式描述其规格，即，使用pure关键词。

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

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

//@ ensures \result >= 0;
public /*

在上面几个例子中，getName没有做任何限定，是一个极简的场景；getStatus()限定了返回值\result只能为bachelor和master中的一个；getCredits()的例子休闲南定了返回值必须大于等于0：\result >= 0。

在方法规格中，有些前置条件也可以引用pure方法返回的结果。

如前所述，为了有效区分方法的正常功能行为和异常行为，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 <= 99 $ 和 $ z < 0 $ 有交集），也因此对于这个例子的规格而言，任何实现都不能满足该规格，这是严重的设计错误，应当避免。作为重要的设计原则，同一个方法的正常功能前置条件和异常功能前置条件一定不能有重叠。

在上面的例子中，我们还可以看出，不管是正常功能规格还是异常功能规格，都包括了前置条件、后置条件和副作用声明。但不同的是，异常功能规格中，后置条件常表示为抛出异常，使用signals子句表示。

`signals`子句

signals子句结构为signals (***Exception e)b_expr，意思是当b_expr为true时，方法会抛出括号中给出的相应异常e。对于上面的例子而言，当z < 0时，就会抛出异常IllegalArgumentException

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

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

还有一个简化的signals子句，即signals_obly子句，其后跟着一个异常类型。signals子句强调在对象状态满足某个条件的时候抛出符合相应类型的异常。

有时，为了更明显地区分异常，会针对输入参数的取值范围抛出不同的异常，从而提醒调用者进行不同的处理。这时可以使用多个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;
}

上面的例子针对Student类的recordCredit(int z)方法，从规格角度定义了一个规格数据int[] credits，并提供了三个功能规格，使用了两个also分隔。

三个功能的requires子句合在一起覆盖了方法输入参数的所有取值范围，并且没有交叉，这是功能规格设计的基本要求。

其中，两个异常功能规格使用signals_only子句分别抛出相应的异常。

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

Part 4 类型规格

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

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

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

不变式invariant

不变式（invariant）是要求再所有可见状态（visible state）下都必须满足的特性，语法上定义为invariant P，其中invariant是关键词，P是谓词。对于类型规格而言，可见状态是一个重要概念，一般指特定时刻下对一个对象状态的观察。以下描述几种时刻下对象o的状态都是可见状态：

对象的有状态构造方法（用来初始化对象成员变量初值）的执行结束时刻
在调用一个对象回收方法（finilize方法）来释放相关资源开始的时刻
在调用对象o非静态、有状态方法（non-helper）的开始和结束时刻
在调用对象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;
	  @*/
}

上面的例子中，Path类的不变式定义了seq_nodes不能为null，且任何一个Path对象至少包含两个节点，一个起始节点（start_node）和一个终止节点（end_node）。

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

如果一个对象的可见状态不满足不变式，那么称该对象的状态有错。

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

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

状态变化约束constraint

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

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

类ServiceCounter拥有一个成员变量counter，包含一个不变式和一个状态约束变化。不变式指出counter >= 0，而constraint不同，约束每一次修改counter只能加1。虽然这个约束可以在对counter进行修改的方法中通过后置条件来表示，但是每个可能修改counter的方法都需要加上这样的后置条件，远不如constraint这样的表示来得方便。不仅如此，invariant和constraint可以直接被子类继承获得。

和不变式一样，JML也根据类的静态成员变量区分了两类约束：static constraint和instance constraint。其中static constraint指涉及类的静态成员变量，而instance constraint则可以涉及类的静态成员变量和非静态成员变量。同样，也可以在规格中通过关键词来明确区分：static constraint P和instance constraint P。

方法与类型规格的关系

如果一个类是不可变类，就没必要定义其不变式，只需要在构造方法中明确其初始状态应该满足的后置条件即可。当然，也可以反过来，定义不变式，而不定义构造方法的后置条件。

事实上，在大部分情况下，一个类有几种不同类别的方法：静态初始化（不是方法，但也是一种行为）、有状态静态方法、有状态构造方法、有状态非静态方法。以下展示两类不变式和方法的关系：

	静态成员初始化	有状态静态方法	有状态构造方法	有状态非静态方法
static invarient	建立	保持	保持	保持
instance invarient	（无关）	（无关）	建立	保持，除非是finalizer方法

注：“建立”的含义是静态成员建立了满足相应不变式的类或对象状态。“保持”的含义是如果方法执行前不变式满足，执行后还应该满足相应的不变式。

同理，JML也对constraint与方法之间的关系进行了约定：

	静态成员初始化	有状态静态方法	有状态构造方法	有状态非静态方法
static constraint	（无关）

「BUAA OO Unit 3」 JML笔记

Part 0 前言

Part 1 注释

行注释

块注释

Part 2 JML表达式

pure

model

non_null

原子表达式

\result

\old(expr)

\not_assigned(x,y,...)

\not_modified(x,y,...)

\nonnullelements(container)

\type(type)

\typeof(expr)