用B机检查JML规范

### 用 B 机检查 JML 规范 #### 1. 类和对象表示 在将 Java 类转换为 B 机表示时，我们把 Java 类视为一个整体集合。首先，收集指定规范中引用的所有 JML 类。由于某些原因，需要将所有类表达在单个 B 机中，该 B 机包含全局机。 为避免标识符名称冲突，从类中提取的标识符会加上 `b_ClassName_` 前缀，变量会加上 `b_ClassName` 前缀，其中 `ClassName` 是类名。对于每个类，用一个集合变量 `b_ClassNameInstances` 表示已创建的对象，它是抽象地址集的子集。 为表达 JML 历史约束，需表示当前状态之前的系统状态，因此复制表示实例的变量。由于不考虑回收未使用地址的垃圾回收器，前一状态的实例集是当前实例集的子集。此外，还声明常量来表示 JML 规范中可能抛出的每个异常。 以下是一个示例，展示了 `Purse` 和 `LimitedPurse` 类在 B 机中的表示： ```plaintext MACHINE system INCLUDES global CONSTANTS exc NoCreditException PROPERTIES exc NoCreditException ∈EXCEPTIONS ∧exc NoCreditException ̸= no exception VARIABLES b PurseInstances, b Purse oldInstances b LimitedPurseInstances, b LimitedPurse oldInstances INVARIANT b PurseInstances ⊆Instances ∧b Purse oldInstances ⊆b PurseInstances ∧ b LimitedPurseInstances ⊆Instances ∧ b LimitedPurse oldInstances ⊆b LimitedPurseInstances ∧... INITIALISATION b PurseInstances,b LimitedPurseInstances := ∅,∅∥ b Purse oldInstances,b LimitedPurse oldInstances := ∅,∅∥... ``` #### 2. 类型转换和属性表示 大部分 Java 类型仅用整数就能表达，如 `byte`、`short`、`int` 和 `long` 等整数类型。通过在机器不变式中指定其值的范围来区分这些类型。对于 `long` 类型，由于其值范围可能超出验证工具的最大和最小整数值，会有一些限制。字符用其无符号短整数值表示，而浮点类型（`float` 和 `double`）因无法用 B 符号表示而被禁止。 对象引用被类型化为地址，是相应类/机器已创建对象集的元素，该集合是公共 `INSTANCES` 集的子集，且对象引用可以为 `null`，以此模拟别名原则。数组被视为从自然数到相应类型值的部分函数。 以下是支持类型的值范围表： | 类型 | 值范围 | | ---- | ---- | | `byte` | -128..127 | | `short` | -32768..32767 | | `int` | -2147483648..2147483647 | | `char` | 0..65535 | | 类 C 的对象 | `b_CInstances ∪{null}` | | `Type[ ]...[ ]` | `NAT →(... (NAT →Range(Type))...)` | 类属性用机器变量表示，在相应的 B 机子句中声明、类型化和初始化。属性根据其 `static` 修饰符有两种情况： - 非静态属性：变量被类型化为将已创建实例映射到其对应值的全函数。 - 静态属性：对所有类实例具有相同值，其值不依赖于任何实例，可直接类型化。 为表达历史约束，复制每个属性以保留前一状态的值，通过在变量名前加 `old_` 来区分前值。 以下是一个示例，展示了 `Purse` 类的非静态属性 `balance` 和 `LimitedPurse` 类的静态属性 `max_amount` 在 B 机中的表示： ```plaintext VARIABLES ... b Purse balance, b Purse old balance, b LimitedPurse max amount, b LimitedPurse old max amount, ... INVARIANT ... b Purse balance ∈b PurseInstances →-32768..32767 ∧ b Purse old balance ∈b Purse oldInstances →-32768..32767 ∧ b LimitedPurse max amount ∈-32768..32767 ∧ b LimitedPurse old max amount ∈-32768..32767 ∧... INITIALISATION ... b LimitedPurse max amount, b LimitedPurse old max amount := 10000, 10000 ... END ``` #### 3. 实例创建 在 Java 语义中，类属性的初始值可以通过两种方式表达：在属性声明中指定值，或由构造函数赋值，构造函数赋值会覆盖声明中给定的值。若属性声明中未定义值且构造函数未赋值，则使用默认值，数值类型为 0，对象类型为 `null`。 在 JML 规范中，可通过查看 `assignable` 子句知道方法执行会影响哪些属性，从而推断哪些字段被赋予声明时给定的初始值。构造函数的表达基于方法规范表达式。 以下是 `Purse` 类构造函数 `Purse(short)` 在 B 机中的表示： ```plaintext b Purse constructorPurse short(this, b amount) ˆ= PRE this ∈INSTANCES - instances ∧this ̸= null ∧b amount ∈-32768..32767 ∧ exception = no exception ∧diverges = FALSE ∧b amount ≥0 THEN ANY assigned balance WHERE assigned balance ∈-32768..32767 ∧assigned balance = b amount THEN new({this}) ∥b PurseInstances := b PurseInstances ∪{this} ∥ b Purse balance := b Purse balance ∪{this  →assigned balance} END ∥b Purse oldInstances := b PurseInstances ∥b Purse old balance := b Purse balance END ``` 这个操作调用了全局机的 `new` 操作来注册新创建的实例。 #### 4. 在 B 机中表达 JML 规范 ##### 4.1 不变式和历史约束的表达 为检查不变式和历史约束，将它们都表达在机器的 `INVARIANT` 子句中。这些属性依赖于实例，因此其表达需在考虑类的已创建实例上进行全称量化