面向对象-Unit3-JML

JML荣耀！

JML基本语法

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言，是一种行为接口规格
语言，提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。

一般而言，JML有三种主要的用法：

1. 开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
2. 针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
3. 基于规格和源代码实现，设计覆盖性更好的自动化测试，能够自动对测试执行结果进行判断，形成测试预言(test oracle)。

注释结构

JML使用javadoc风格的注释来表达规格，这些注释通常以’@'符号开始。有两种注释方式，行注释和块注释。其中行注释的表示方式为//@annotation，块注释的方式为/* @ annotation @*/ 。

//@ public model non_null int [] elements

/*@ contents
  @
  @*/

关键词

1. pure：方法的执行不会有任何副作用
2. model：规格
3. non_null：数组引用对象不能为null

JML表达式

原子表达式

原子表达式是指不能再分解为更小的表达式的基本表达式。它们通常用于描述程序的状态或行为。JML中的原子表达式包括：

1. \result：非void类型的方法执行所获得的结果，即方法执行后的返回值。

2. \old(expr)：表示一个表达式expr在相应方法执行前的取值。其遵循Java引用规则。

   针对一个对象引用，只判断引用本身是否变化（是否指向了另一个对象），不判断引用指向的对象实体的内容是否发生变化。

3. \not_assigned(x,y,...)：表示括号中的变量在方法执行过程中是否被赋值。

   如果没有被赋值，返回true，否则返回false。

   一般该表达式被用于后置条件的约束表示上，用来限制一个方法的实现不能对列表中的变量赋值。

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

5. \nonnullelements(container)：表示container对象中存储的对象不会有null，等价于如下断言：

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

6. \type(type)：返回类型type对应的类型。

7. \typeof(expr)：返回对象expr对应的准确类型。

量化表达式

量化表达式是JML中的一种表达式，用于描述某个条件对于一组对象是否成立。JML中的量化表达式包括：

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

   \forall的语法为量词对象-对象的限制-值为布尔类型的式子，最后返回一个布尔值。\forall语法可以进行嵌套。

   举例而言，对于(\forall int i,j; 0 <= i && i <= j&& j < 10;a[i] < a[j])的意思为，对于任意0<=i<j<=10，a[i]<a[j]。

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

3. \sum：求和表达式，返回给定范围内的表达式的和。

   (\sum int i; 0<= i && i < 5;i)。值得注意的是，0 <= i && i < 5是对i的范围的限制，而求和表达式是最后的那个i。

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

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

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

7. \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表示当前作用域下的每个变量都不可以在方法执行过程中被赋值。

方法规格

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

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

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

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

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

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

前置条件：requires

前置条件通过requires子句表示：requires P;。表达的意思是”要求调用者确保P为真“。

方法规格中可以有多个requires子句，为并列关系，调用者必须同时满足所有的并列子句要求。

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

后置条件：ensures

后置条件通过ensures子句表示：ensures Q;。表达的意思是”方法实现者确保方法执行返回的结果一定满足谓词Q的要求，即，确保Q为真“。

类似地，多个ensures子句是被允许的且为并列关系即须同时满足。类似地，或的表达应当在一个ensures子句中用逻辑或约束。

副作用范围限定：assignable/modifiable

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

从方法规格的角度看，必须要给出明确的副作用范围。JML提供了副作用范围子句，使用关键词assignable或者modifiable。assignable表示可赋值，modifiable表示可修改。二者有一定差异，但是在大部分情况可以交换使用。

从语法上看，副作用约束子句有两种形态：

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

例子为：

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关键词。

但可以对其后置条件进行约束。有些前置条件也可以引用pure方法返回的结果。

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

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

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

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

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

区分机制

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

• 正常功能，一般指输入或方法关联this对象的状态在正常范围内时所指向的功能
• 异常功能，即如下public exceptional_behavior所定义的规格。
• public指相应的规格在所在包范围内的所有其他规格处都可见。
• 如果一个方法没有异常处理行为，那么无需区分正常功能规格和异常功能规格。

/*@ public normal_behavior
  @ requires z >= 0;
  @ 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)方法的正常功能给出规格。

上述代码有一个关键词also，意为除了正常功能规格外还有一个异常功能规格。

在JML中，有两种使用also的场景：

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

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

signals子句

signals子句结构为signals (Exception e) b_expr，意思是当b_expr为true时，方法会抛出括号中给出的相应异常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;
}

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

三个功能的requires子句合在一起覆盖了方法输入参数的所有取值范围，并且没有交叉，这是功能规格设计的基本要求。其中，两个异常功能规格使用signals_only子句分别抛出相应的异常。

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

类型规格

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

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

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

不变式invariant

不变式（invariant）是要求在所有可见状态下都必须满足的特性，语法上定义为invariant P，其中invariant是关键词，P是谓词。一个不严谨的表述是：一个写方法的执行前后，必须满足条件P。

对于类型规格，可见状态是一个重要概念，一般指特定时刻下对一个对象状态的观察。这里的可见不是一般意义上的是否可以见到，而是带有完整可见的含义。在会修改状态的方法的执行期间，对象状态不稳定，对视可能会被修改，因此在这样的方法执行期间，对象和的不变式有可能不满足。

以下是几种常见的可见状态：

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

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

类型规格强调在任意可见状态下（状态稳定的修改完成阶段）都要满足不变式。

一个类可以包括多个不变式，相互独立。如果一个对象的可见状态不满足不变式，那么称该对象的状态有错。不变式中可以直接引用pure状态方法。

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。

对应类成员变量有静态和非静态之分，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	（无关）	遵从	遵从	遵从
instance constraint	（无关）	（无关）	（无关）	遵从

• “建立”的含义是静态成员建立了满足相应不变式的类或对象状态。
• “保持”的含义是如果方法执行前不变式满足，执行后还应该满足相应的不变式。
• “遵从”的含义是成员变量的当前取值和上一个取值之间的关系满足constraint的规定，即“遵从规定”。

Java异常处理

异常处理是一种重要的编程概念，用于处理程序执行过程中可能出现的错误或异常情况。

基本概念

Thorwable类（表示可抛出）是所有异常和错误的超类，两个直接子类为Error和Exception，分别表示错误和异常。

其中异常类Exception又分为运行时异常（RuntimeException）和非运行时异常， 这两种异常有很大的区别。Error类及其子类也是非检查异常。

• 检查异常/编译时异常：编译器在编译期间检查的那些异常。除了RuntimeException之外，所有直接继承 Exception 的异常都是检查异常。
• 非检查异常/运行时异常：编译器不会检查运行时异常，在抛出运行时异常时编译器不会报错，当运行程序的时候才可能抛出该异常。Error及其子类和RuntimeException 及其子类都是非检查异常。

下面的列表是 Throwable 类的主要方法:

1. public String getMessage()：返回关于发生的异常的详细信息。这个消息在Throwable 类的构造函数中初始化了。
2. public Throwable getCause()：返回一个 Throwable 对象代表异常原因
3. public String toString()：返回此 Throwable 的简短描述
4. public void printStackTrace()：将此 Throwable 及其回溯打印到标准错误流
5. public StackTraceElement [] getStackTrace()：返回一个包含堆栈层次的数组。下标为0的元素代表栈顶，最后一个元素代表方法调用堆栈的栈底
6. public Throwable fillInStackTrace()：用当前的调用栈层次填充Throwable 对象栈层次，添加到栈层次任何先前信息中

捕获异常

使用try/catch关键字可以捕获异常。try/catch代码块放在异常可能发生的地方。try/catch代码块中的代码称为保护代码。

catch语句包含要捕获异常类型的声明。当保护代码块中发生一个异常时，try后面的catch块就会被检查。如果发生的异常包含在catch块中，异常会被传递到该catch块，这和传递一个参数的方法是一样。

无论是否发生异常，finally代码块中的代码总会被执行。在finally代码块中，可以运行清理类型等收尾善后性质的语句。

try {
   // 程序代码
} catch(异常类型1 异常的变量名1) {
  // 程序代码
} catch(异常类型2 异常的变量名2) {
  // 程序代码
} catch(异常类型3 异常的变量名3) {
  // 程序代码
} finally {
    
}

抛出异常

throw用于在程序运行过程中抛出异常，以供其他类进行捕获，进行异常处理。

throws关键字用于在方法声明中指定该方法可能抛出的异常。当方法内部抛出指定类型的异常时，该异常会被传递给调用该方法的代码，并在该代码中处理异常。

例如，下面的代码中，当readFile方法内部发生IOException异常时，会将该异常传递给调用该方法的代码。在调用该方法的代码中，必须捕获或声明处理IOException异常。

public void readFile(String filePath) throws IOException {
  // 异常是由new BufferedReader()抛出的，代码别的地方不会抛出
  BufferedReader reader = new BufferedReader(new FileReader(filePath));
  String line = reader.readLine();
  while (line != null) {
    System.out.println(line);
    line = reader.readLine();
  }
  reader.close();
}

一个方法可以声明抛出多个异常，多个异常之间用逗号隔开。

public void withdraw(double amount) throws RemoteException, InsufficientFundsException{}

自定义异常类

一般地，用户自定义异常类都是RuntimeException的子类。

• 自定义异常类通常需要编写几个重载的构造器。
• 自定义异常需要提供全局常量：serialVersionUID
• 自定义的异常通过throw抛出。
• 自定义异常最重要的是异常类的名字，当异常出现时，可以根据名字判断异常类型。

用户自定义异常类MyException，用于描述数据取值范围错误信息。用户自己的异常类必须继承现有的异常类。

不同处理方法

反射：处理了一种意外情况，根据软件需求，这种情况也需要报告给上层

• 方法m被方法p调用
• 方法m在运行过程中抛出异常e1
• 方法p捕捉到e1
• 经过处理后抛出另一个异常e2给其调用者

屏蔽：处理了一种意外情况，根据软件需求，没必要让上层知道是否发生了这种意外

• 方法m被方法p调用
• 方法m在运行过程中抛出异常e1
• 方法p捕捉到e1
• 经过处理后不再抛出异常给其调用者

如果期望不去“干扰”调用者的处理逻辑，即不必捕捉相应的异常，则应使用不可控异常（隐式处理）

• 优点：不可控异常默认逐层“上报”，可以在合适位置集中捕捉和处理
• 缺点：如果每一层都忘记捕捉处理，一旦抛出异常会导致程序崩溃

如果要求调用者必须进行处理，应该使用可控异常（显式处理）

• 优点：通过编译确保异常一定会得到处理
• 缺点：分散的异常捕捉和处理，容易出现不一致

规格模式

规格模式（Specification Pattern）可以认为是组合模式的一种扩展。

很多时候程序中的某些条件决定了业务逻辑，这些条件就可以抽离出来以某种关系（与、或、非）进行组合，从而灵活地对业务逻辑进行定制。

另外，在查询、过滤等应用场合中，通过预定义多个条件，然后使用这些条件的组合来处理查询或过滤，而不是使用逻辑判断语句来处理，可以简化整个实现逻辑。

这里的每个条件都是一个规格，多个规格（条件）通过串联的方式以某种逻辑关系形成一个组合式的规格。规格模式属于结构型设计模式。

规格模式主要适用于以下应用场景：

1. 验证对象，检验对象本身是否满足某些业务要求或者是否已经为实现某个业务目标做好了准备
2. 从集合中选择符合特定业务规则的对象或对象子集
3. 指定在创建新对象的时候必须要满足某种业务要求。

规格模式

规格模式主要包含6个角色：

1. 抽象规格书（Specification）：对规格书的抽象定义
2. 组合规格书（CompositeSpecification）：一般设计为抽象类，对规格书进行与或非操作，实现and()、or()、not()方法，在方法中关联子类，因为子类为固定类，所以父类可以进行关联
3. 与规格书（AndSpecification）：对规格书进行与操作，实现isSatisfiedBy()方法
4. 或规格书（OrSpecification）：对规格书进行或操作，实现isSatisfiedBy()方法
5. 非规格书（NotSpecification）：对规格书进行非操作，实现isSatisfiedBy()方法
6. 业务规格书（BizSpecification）：实现isSatisfiedBy()方法，对业务进行判断，一个类为一种判断方式，可进行扩展。