OO第三单元博客作业

系统管理员 2021-12-17 00:21 293阅读 0赞

## 一、JML语言及工具 ##

JML是java modeling language的缩写，用于对Java程序进行规格化设计的一种表示语言，可以用来描述一段代码的具体行为，比如前置条件、副作用、后置条件等。通过JML的相关支持工具，可以检查规格是否合乎规范、可以基于规格自动构造测试用例，同时可使用SMT Solver等工具以静态方式来检查代码实现对规格的满足情况。

### （1）JML表达式 ###

#### （一）原子表达式 ####

1.  `\result`：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
2.  `\old(expr)`：表示一个表达式`expr`在相应方法执行前的取值，该表达式涉及到评估`expr`中的对象是否发生变化。  
    *如果是引用（如hashmap)，对象没改变，但进行了插入或删除操作。v和odd(v)也有相同的取值。*
3.  `\not_assigned(x,y,...)`：用来表示括号中的变量是否在方法执行过程中被赋值。如果没有被赋值，返回为true ，否则返回 false 。用于后置条件的约束，限制一个方法的实现不能对列表中的变量进行赋值。
4.  `\not_modified(x,y,...)`：该表达式限制括号中的变量在方法执行期间的取值未发生变化。
5.  `\nonnullelements(container)`：表示container对象中存储的对象不会有null。
6.  `\type(type)`：返回类型type对应的类型(Class)，如type(boolean)为Boolean.TYPE。TYPE是JML采用的缩略表示，等同于Java中的 java.lang.Class。
7.  `\typeof(expr)`：该表达式返回expr对应的准确类型。如`\typeof(false)`为Boolean.TYPE。

#### （二）量化表达式 ####

1.  `\forall`：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。

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

1.  `\sum`：返回给定范围内的表达式的和。

1.  `\product`：返回给定范围内的表达式的连乘结果。

1.  `\max`：返回给定范围内的表达式的最大值。

1.  `\min`：返回给定范围内的表达式的最小值。

1.  `\num_of`：返回指定变量中满足相应条件的取值个数。可以写成`(\num_of T x; R(x);P(x))`，其中T为变量x的类型，R(x)为x的取值范围；P(x)定义了x需要满足的约束条件。从逻辑上来看，该表达式也等价于`(\sum T x;R(x)&&P(x);1)`。

#### （三）集合表达式 ####

可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素。集合构造表达式的一般形式为：`new ST {T x|R(x)&&P(x)}`，其中的R(x)对应集合  
中x的范围，通常是来自于某个既有集合中的元素，如s.has(x)，P(x)对应x取值的约束。

表示构造一个JMLObjectSet对象，其中包含的元素类型为Integer，该集合中的所有元素都在容器集合s中出现（注：该容器集合指Java程序中构建的容器，比如ArrayList），且整数值大于0。

#### （四）操作符 ####

JML可以正常使用java所定义的操作符，此外，还专门定义了以下四类。

1.  `E1<:E2`子类型操作符：如果类型E1是类型E2的子类型(sub type)或相同类型，则该表达式的结果为真，否则为假。任意一个类X，都必然满足`X.TYPE<:Object.TYPE`。

1.  `b_expr1<==>b_expr2`或`b_expr1<=!=>b_expr2`等价关系操作符：其中b\_expr1和b\_expr2都是布尔表达式。
2.  `b_expr1==>b_expr2`或`b_expr1<==b_expr2`推理操作符：相当于离散的->，只有（1，0）是false。
3.  `\nothing`或`\everthing`变量引用操作符：表示当前作用域访问的所有变量。前者空集，后者全集。变量引用操作符经常在`assignable`句子中使用，如 `assignable \nothing`表示当前作用域下每个变量都不可以在方法执行过程中被赋值。

### 方法规格 ###

定义前置条件和满足后置条件的东西。

#### （一 )前置条件 ####

对方法输入参数的限制，如果不满足前置条件，方法执行结果不可预测，或者说不保证方法执行结果的正确性。  
`requires P;`其中`requires`是JML关键词，表达的意思是“要求调用者确保P为真”。多个分开的requires是并列关系都要满足，或关系用`requires P1||P2`;

#### （二）后置条件 ####

对方法执行结果的限制，如果执行结果满足后置条件，则表示方法执行正确，否则执行错误。其中`ensures`是JML关键词，表达的意思是“方法实现者确保方法执行返回结果一定满足谓词P的要求，即确保P为真”。并列关系和或关系与前置相同。  
`ensures P;`

#### （三）副作用 ####

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

*  从方法规格的角度，必须要明确给出副作用范围。
 *  JML提供了副作用约束子句，使用关键词`assignable`（表示可赋值）或者`modifiable`（可修改）。虽然二者有细微的差异，在大部分情况下，二者可交换使用。
 *  副作用约束子句共有两种形态，  
    1. 用JML关键词来概括，不指明具体的变量；  
    2. 指明具体的变量列表。

### 其他 ###

1.  `(/*@ pure @ */)`  
    指不会对对象的状态进行任何改变，也不需要提供输入参数，这样的方法无需描述前置条件，也不会有任何副作用，且执行一定会正常结束。有些前置条件可以引用`pure`方法的返回结果。
2.  `forall`和`exists`  
    前置条件或后置条件需要对不止一个变量进行约束，往往是需要对一个容器中的所有元素进行约束。
3.  `public normal_behavior`和`public exception_behavior`  
    为了有效地区分方法的正常功能行为和异常行为。如果一个方法没有异常处理行为，不必使用这两个关键词。  
    `public`，指相应的规格在所在包范围内的所有其他规格处都可见。  
    `also` ，这里指除了正常功能规格外，还有一个异常功能规格。
4.  `signals (***Exception e) b_expr`  
    强调满足某个条件抛出相应异常。  
    是当 b\_expr 为 true 时，方法会抛出括号中给出的相应异常e。注意一定要在方法声明中明确指出（使用Java的 throws 表达式），且必须确保signals子句中给出的异常类型一定等同于方法声明中给出的异常类型，或者是后者的子类型。  
    `signals_only (***Exception e)`  
    强调满足前置条件抛出相应异常。

### 类型规格 ###

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

*  `invariant P`  
    不变式（invariant）是要求在所有可见状态下都必须满足的特性，其中`invariant`为关键词， `P`为谓词。对于类型规格而言，可见状态(visible state)是一个特别重要的概念。

凡是会修改成员变量（包括静态成员变量和非静态成员变量）的方法执行期间，对象的状态都不是可见状态。这里的可见不是一般意义上的能否见到，而是带有完整可见的意思。在会修改状态的方法执行期间，对象状态不稳定，随时可能会被修改。换句话说，在方法执行期间，对象的不变式有可能不满足。因此，类型规格强调在任意可见状态下都要满足不变式。

### （2）依赖工具 ###

openJML可以编译有JML的代码，常用选项有如下几个。

\-check 可以检查.java文件中JML是否有语法错误

\-esc可以对代码静态检查

\-rac可以动态编译检查

## 二、**部署JMLUnitNG/JMLUnit** ##

这里使用的是openjml工具。

编译过程

java -jar jmlunitng.jar -cp demo/Demo.java

javac -cp jmlunitng.jar demo/\*\*/\*.java demo/\*.java

输入以下运行代码

java -cp jmlunitng.jar demo.Demo\_JML\_Test