写在前面：

本文章是根据法国国立高等电力技术、电子学、计算机、水力学与电信学校 (E.N.S.E.E.I.H.T.) 第九学期课程 “Formal development of complex system” 及以下参考资料总结而来的课程笔记。碍于本人学识有限，部分叙述难免存在纰漏，请读者注意甄别。

参考资料：

《Formal development of complex systems》Yamine AIT-AMEUR, Neeraj Kumar SINGH
《形式化方法：基于 B 方法的严格软件开发》裘宗燕，北京大学数学学院信息科学系
- 第一章：B 方法概述
- 第三章：集合论与逻辑
Oneree的博客：集合论与关系

零、前言

在软件工程的生命周期中，有一部分非常重要的工作，那就是进行需求分析和写出需求文档。

需求分析阶段需要清晰地说明什么是这个系统的功能和约束条件，
需求文档多半是使用自然语言写出的（大多数情况中，需求文档根本没有，或者写得很差）。需求文档如果不规范，会给后续阶段带来许多困难。特别是，由于需求文档的脆弱性，在设计阶段中就会出现不可避免的规范修改，并因此带来综合性的影响。如果需求文档写得好，这种困难可能就消失了。

形式化语言常用于软件工程生命周期的需求分析阶段，可以帮助工程师理解需求文档，完成建模（需求到形式化模型的转换），甚至进一步完善需求文档（挖掘隐藏的需求，以及改进需求中矛盾的部分）。

因此，我们在正式介绍 Event-B 这种形式化方法之前，需要先了解一些关于集合论的概念，以及其他的相关知识。

一、谓词逻辑与集合论

1 谓词逻辑

为了描述软件系统中的事实，就需要写各种各样的谓词（Predicate），也就是对事实的表述的断言。

我们不但需要描述一些简单的事实，还可能需要描述非常复杂的事实。为此就需要谓词逻辑表示为描述软件的性质。下面给出几个基础的谓词逻辑的表达形式：

数学表示	说明
$\top$	`TRUE`，永真（Constant True）
$\bot$	`FALSE`，永假（Constant False）
$\neg A$	否定（Negation）
$A \land B$	和取（Conjunction）
$A \lor B$	析取（Disjunction）
$A \Rightarrow B$	蕴含（Implication）
$A \Leftrightarrow B$	等价（Equivalence）

在谓词逻辑（和命题逻辑）里可以证明大量的等价公式，我们可以用这些公式做谓词的等价变换，这种操作称为谓词演算。例如（而是为了方便说逻辑公式之间的关系引进 “=” 来表示等价）

谓词演算	说明
$P \Rightarrow Q \quad = \quad \neg P \lor Q$
$P \Leftrightarrow Q \quad = \quad (P \Rightarrow Q) \land (Q \Rightarrow P)$
$P \land P \quad = \quad P$	$\land$ 幂等率（Idempotent）
$P \lor P \quad = \quad P$	$\lor$ 幂等率（Idempotent）
$P \land \neg P \quad = \quad \bot(\text{FALSE})$	矛盾律
$P \lor \neg P \quad = \quad \top(\text{TRUE})$	排中律
$P \land \top \quad = \quad P$
$P \land \bot \quad = \quad \bot$
$P \lor \top \quad = \quad \top$
$P \lor \bot \quad = \quad P$
$P \land Q \quad = \quad Q \land P$	$\land$ 交换律
$P \lor Q \quad = \quad Q \lor P$	$\lor$ 交换律
$(P \land Q) \land R \quad = \quad Q \land (P \land R)$	$\land$ 结合律
$(P \lor Q) \lor R \quad = \quad Q \lor (P \lor R)$	$\lor$ 结合律
$P \land (Q \lor R) \quad = \quad (P \land Q) \lor (P \land R)$	分配律
$P \lor (Q \land R) \quad = \quad (P \lor Q) \land (P \lor R)$	分配律
$\neg (P \land Q) \quad = \quad \neg P \lor \neg Q$	分配律
$\neg (P \lor Q) \quad = \quad \neg P \land \neg Q$	分配律

谓词逻辑和 Event-B 里还可以写全称量词和存在量词，形式是：

$\begin{aligned} & \text{全称量词: Universal Quantification} \quad \forall x.P \\ & \text{存在量词: Existential Quantification} \quad \exist x.P \\ \end{aligned}$

其中， $P$ 指代谓词（Predicate），其可以是（我们后面将介绍的）二元关系或函数。

写软件规范时，实际写出的全称和存在量化公式都是下面形式:

$\begin{aligned} & \forall x.(x \in P \Rightarrow Q) \\ & \exist x.(x \in P \land Q) \end{aligned}$

这两个公式说的是：对于属于类型 $P$ 的每个 $x$ 都有 $Q$ 或者存在属于类型 $P$ 的某个 $x$ 有 $Q$ 。

2 集合

一个集合 $S$ 是某种事物的一些实例的一个汇集。例如：自然数的集合、1 到 100 之间的自然数集合等。

对于一个集合 $S$ ，最经常要考虑的一个问题就是某事物是否在某集合里：

$e \in S$ ，表示 $e$ 是 $S$ 的元素；
$e \notin S$ ，表示 $S$ 中不存在 $e$ ；

对于元素个数很少的集合，可以用枚举元素的方式说明。例如 $\text{SQUARES} = \{1,4,9,16,25\}$ 。

集合的元素个数称为其序数，表示为 $card(S)$ 。例如 $card(\{2,4,6\}) = 3$ 。

空集（Empty Set）是没有元素的集合，用 $\varnothing$ 表示。

如果要描述有很多元素的集合，可以采用集合的内涵（comprehension）表示方式，用一个谓词 $P$ 描述集合元素满足的条件。一般表现形式为

$\begin{Bmatrix} e \mid e \in S \land P \end{Bmatrix}$

例如， $\text{SQUARES} = \{e \mid n\in \text{NAT}_1 \land n \le 5 \land e=n \times n\}$ 。

下面我们给出一些基本集合：

数学表示	正文表示	说明
$\mathbb{Z}$	`INREGER`	整数集合，看作抽象集合
$\mathbb{N}$	`NATURAL`	自然数集合
$\mathbf{INT}$	`INT`	系统可实现的整数集合
$\mathbf{NAT}$	`NAT`	系统可实现的自然数集合
$\mathbf{NAT}_1$	`NAT1`	$\mathbf{NAT}$ 的正子集
$\mathbf{BOOL}$	`BOOL`	布尔类型，只包括 `TRUE` 和 `FALSE`

其中，实际的整数只能是 $\mathbf{INT}$ 的元素,有两个预定义整数 $\mathbf{MININT}$ 和 $\mathbf{MAXINT}$ ，是 $\mathbf{INT}$ 集合里的最小和最大整数。而整数的区间是一类特殊集合，有专门表示形式：

$m..n \triangleq \{i | i\in \mathbb{Z} \land m \le i \le n\}$

例如， $\mathbf{INT} = \mathbf{MININT} .. \mathbf{MAXINT}$ 、 $\mathbf{NAT} = 0..\mathbf{MAXINT}$ 等。

基本集合运算

基本的集合运算是：

并集（Union）：$S \cup T $
交集（Intersection）： $S \cap T$
差集（Different）： $S - T$

对于集合的集合可以做广义并集（Generalised Union）和广义交集（Generalised Intersection）：

广义并集： $\bigcup SS \triangleq \{e \mid \text{ for all } s \in SS · e \in s\}$ ，写作 union SS
广义交集： $\bigcap SS \triangleq \{e \mid \text{ for some } s\in SS · e \in s\}$ ，写作 inter SS

一个集合的幂集（PowerSet）是它的所有子集的集合：

幂集，所有子集的集合： $\mathbb{P}S \triangleq \{ T \mid T \subseteq S\}$ ，写作 POW S

对于任何集合都有：
- $\varnothing \in \mathbb{P}S$
- $S \in \mathbb{P}S$
所有非空子集的集合： $\mathbb{P}_1S \triangleq \{ T \mid T \subseteq S \land T \ne \varnothing \}$ ，写作 POW1 S

两个集合 $S$ 和 $T$ 笛卡尔积（Cartesian Product）是二元有序对 $(s,t)$ 的集合，写作 S*T

$S \times T \triangleq \{ (s,t) | s \in S \land t \in T\}$

集合之间的关系有：

数学表示	说明	注释
$S = T$	$S$ 等于 $T$	$S = T\quad \triangleq \quad S \subseteq T \land T \subseteq S$
$S \ne T$	$S$ 不等于 T$
$S \subseteq T$	$S$ 是 $T$ 的子集	$S \subseteq T\quad \triangleq \quad S \in \mathbb{P}(T)$
$S \subset T$	$S$ 是 $T$ 的真子集
$S \nsubseteq T$	$S$ 不是 $T$ 的子集
$S \not\subset T$	$S$ 不是 $T$ 的真子集

显然，对于任何 $S$ ，都有：

$S \subseteq S \\ \varnothing \subseteq S$

二元关系

相关阅读：

Oneree的博客：集合论与关系-有序对

我们集合的笛卡尔积部分介绍过，两个集合 $S$ 和 $T$ 笛卡尔积 $S \times T$ 是二元有序对 $(s,t)$ 的集合，其中 $s \in S$ ，$ t \in T$。有时也将二元有序对写作 $s \mapsto t$

二元关系 $S \leftrightarrow T$ 就是所有二元有序对组成集合的子集。下面列出了一些重要的二元关系操作：

数学形式	解释	等价推理
$S \leftrightarrow T$	二元关系	$r \in S \leftrightarrow T \quad \triangleq \quad r \subseteq S \times T$
$\text{dom}(r)$	关系 $r$ 的定义域	$E \in \text{dom}(r) \quad \triangleq \quad \exist y.(E \mapsto y \in r)$
$\text{ran}(r)$	关系 $r$ 的值域	$E \in \text{ran}(r) \quad \triangleq \quad \exist x.(x \mapsto E \in r)$
$r^{-1}$	关系 $r$ 的逆关系	$E \mapsto F \in r ^{-1} \quad \triangleq \quad F \mapsto E \in r ^{1}$
	部分满射（Partial Surjective）二元关系	$\text{if } r \in S$ `<->>` $T$ $\text{ then ran}(r)=T$
	完全二元关系	$\text{if } r \in S$ `<<->` $T$ $\text{ then dom}(r)=S$
	全满射（Total Surjective）二元关系	$\text{if } r \in S$ `<<->>` $T$ $\text{ then dom}(r)=S \land \text{ran}(r)=T$
$S \triangleleft r$	限制关系 $r$ 的定义域为集合 $S$	$S \triangleleft r$ $\triangleq \quad \{x \mapsto y \mid x \mapsto y \in r \land x \in S\}$
$r \triangleright T$	限制关系 $r$ 的值域为集合 $T$	$r \triangleleft T$ $\triangleq \quad \{x \mapsto y \mid x \mapsto y \in r \land y \in T\}$
	限制关系 $r$ 的定义域排除集合 $S$	$\triangleq \quad \{x \mapsto y \mid x \mapsto y \in r \land x \notin S\}$ $\triangleq \quad (\text{dom}(r) - S) \triangleleft r$
	限制关系 $r$ 的值域排除集合 $T$	$\triangleq \quad \{x \mapsto y \mid x \mapsto y \in r \land y \notin T\}$ $\triangleq \quad r \triangleright (\text{ran}(r) - T)$
$r[S]$	$r[S]$ 称为集合 $S$ 在关系 $r$ 下的像（Image）	$\triangleq \quad \{y \mid \exist .x \in S \land x \mapsto y \in r\}$ $\triangleq \quad \text{ran}(S \triangleleft r)$
$p;q$	关系 $p$ 和关系 $q$ 复合而成的关系	$\forall p,q.\quad p \in S \leftrightarrow T,q \in T \leftrightarrow U$ $\triangleq \quad \{x\mapsto y \mid (\exist z. \; x \mapsto z \in p \land z \mapsto y \in q)\}$
	关系 $p$ 对关系 $q$ 覆盖而成的关系
$id(S)$	集合 $S$ 上的恒等关系	$\triangleq \quad \{x \mapsto y \mid x \mapsto y \in (S \times S) \land x=y\}$
$p \otimes q$	关系 $p$ 和关系 $q$ 的直积	$\triangleq \quad \{x \mapsto (y \mapsto z) \mid x \mapsto y \in p \land y \mapsto z \in q\}$
$p \parallel q$	关系 $p$ 和关系 $q$ 的平行积	$\{(x \mapsto y) \mapsto (m \mapsto n) \mid x,y,m,n. \; x \mapsto m \in p \land y \mapsto n \in q\}$
$\text{prj}_1(r)$	投影关系	$\triangleq \quad \{x \mid x \mapsto y \in r\}$
$\text{prj}_2(r)$	投影关系	$\triangleq \quad \{y \mid x \mapsto y \in r\}$

【示例】

$\begin{aligned} p \; & = \; \{ 1 \mapsto 5, 3 \mapsto 9, 6 \mapsto 3, 9 \mapsto 2\} \\ q \; & = \; \{ 2 \mapsto 7, 3 \mapsto 4, 5 \mapsto 1, 9 \mapsto 5\} \\ S \; & = \; \{1,2,3\} \\ p[S] & = \; \{5,9\} \quad \text{关系p中以集合S为定义域的值的集合（像）} \\ p;q & = \; \{1 \mapsto 1, 3 \mapsto 5, 6 \mapsto 4, 9 \mapsto 7\} \end{aligned}$

3 函数

函数是关系的特殊情况。对于关系，其定义域中的任意一个值都有若干个值与之对应。而对于函数，其定义域中的任何一个点，值域里最多只有一个对应的值。

例如我们有一个函数关系 $f$ ：

$f = \{ 2 \mapsto 5, 3 \mapsto 9, 6 \mapsto 3, 9 \mapsto 2 \}$

该函数在定义域为 $S=\{2,6,9\}$ 的值（像）为：

$f[S] = f[\{2,6,9\}] = \{5,3,2\}$

对于任意一个函数 $f$ ，其中 $a \mapsto b \in f$ 。有

$f(a)=b \text{，即 } f[\{a\}] = \{b\}$

【部分函数（Partial Function）】：

对于关系 $r \in S ⇸ T$ ，考虑任意 $a \in T$ ，由于 $(r^{-1};r) \in id(T)$ ，对于任意 $b \in r^{-1} [\{a\}]$ ，像集 $r[\{b\}]$ 只能是单点集合 $\{a\}$ ，但是***并不是所有定义域中的点都能映射到值域的点***，所以关系 $r$ 是部分函数。

$f \in S ⇸ T \quad \triangleq \quad f \in S \leftrightarrow T \land f^{-1};f \subseteq id(\text{ran}(f))$

【全函数（Total Function）】：

全函数是指，在部分函数的基础上使得关系 $r$ 的定义域 $\text{dom}(r) = S$ 。即

$f \in S \to T \quad \triangleq \quad f \in S ⇸ T \land S = \text{dom}(f)$

数学形式	解释	等价推理
$S ⇸ T$	部分函数（Partial Function）	$\triangleq \quad f \cdot f \in S \leftrightarrow T \land f^{-1};f \subseteq id(\text{ran}(f))$
$S \leftrightarrow T$	全函数（Total Function）	$\triangleq \quad f \cdot f \in S ⇸ T \land S = \text{dom}(f)$
	部分单射（Partial Injection）
	全单射（Total Injection）
	部分满射（Partial Surjection）
	全满射（Total Surjection）
	全双射（Bijection）

单射、满射与双射- WiKiPedia

在数学定义中，单射、满射和双射是指根据其定义域和陪域的关联方式所区分的三类映射。

单射：一个映射称为单射（一对一）如果每个可能的像最多只有一个变量映射其上。等价的有，一个映射是单射如果它把不同值映射到不同像。一个单射映射简称单射。下图中第二个映射不必是单射。

满射：一个映射称为满射（到上）如果每个可能的像至少有一个变量映射其上，或者说陪域任何元素都有至少有一个变量与之对应。下图中第一个映射不必为满射。

双射：既是单射又是满射的映射称为双射。映射为双射当且仅当每个可能的像有且仅有一个变量与之对应。下图中第一个映射不必为满射、第二个映射不必为单射。

二、`Event-B`

1 抽象机与上下文

Event-B 是一个基于事件（Event）的、状态迁移（State- transition）模型系统，通过细化（Refinement）将抽象系统完善为一个具体系统，通过证明（Proving）验证系统的正确性。

模型的定义是逐渐完善的：

首先设计一个初始的抽象自动机（Abstract Machine）；
然后通过一系列的细化（Refinement）来完善这个初始的抽象机

一个模型包含了一个离散迁移系统的完整数学开发，它由分属两个类别的一些组件构成，这两个类别分别称为自动机（ $Machine$ ）和上下文（ $Context$ ）。

自动机（ $Machine$ $M a c h i n e$ ）包含模型的动态部分，也就是状态变量、不变式、定理、变动式和事件；
- REFINES：定义该自动机是另一个抽象机的细化；
- SEES：用来引入一个上下文（ $Context$ ），表达了机器对常量和集合的使用，这些常量和集合是通过上下文的公理和实现定理定义的；
- VARIABLES：定义模型中的状态变量；
- INVARIANTS：定义了相应的变量 VARIABLES（状态）需要满足的状态（定义了相应 VARIABLES 的类型）；
- THEOREMS：定义了相应的变量 VARIABLES（状态）需要满足的状态，和 SEES 的上下文中推导出的“约束”，（定义了相应 VARIABLES 的行为）；
- VARIANT：相对于 VARIABLES 来说，是 EVENT 中临时变量，作用域比 VARIABLES 小；
- EVENT：EVENT 则定义了能使状态变量改变的事件，其中包括初始化。
上下文（ $Context$ $C o n t e x t$ ）包含模型的静态部分，对系统建模所需的领域概念的定义，包括载体集合、常量、公理和定理。
- EXTENDS：通过添加新的集合、常量、公理和定理来表达扩展（对另一个上下文的丰富）；
- SETS：声明一些集合；
- CONSTANTS：定义的一些常量；
- AXIOMS：公理，定义集合和常量的属性，描述了不能从其他公理派生出来的属性；
- THEOREMS：描述了可以由 AXIOMS 公理推导出的性质

【 $Context$ 示例】

CONTEXT
	ctx
EXTENDS
	actx        // 上下文ctx扩展了另一个上下文actx, 并添加了一些新的元素
SETS
	s           // 定义一个新集合s
CONSTANTS
	c           // 定义一个新常量c
AXIOMS
	A_c : ...   // 公理A_c定义了集合和常量的属性
THEOREMS
	T_c : ...   // 定义了从公理和定理推导出的一些定理
END

【 $Machine$ 示例】

MACHINE
	m           // 自动机m对应的系统模型
REFINES
	am          // 自动机m从抽象机am细化而来
SEES
	acts        // 将上下文acts导入抽象机m
VARIABLES
	x           // 自动机的变量(状态)
INVARIANTS
	inv(x)      // 关于变量x的不变量"约束"
THEOREMS
	t(x)        // 从上下文推导出的定义和不变量"约束"
VARIANT
	v           // 
EVENTS
	ev1: ...    // ev1, ... 描述状态变化的机器事件列表，至少有一个 INITIALISATION 事件
	...
END

在抽象机中，VARIABLES 的修改是由事件中的动作（Action）和替换（Substitution）导致的。其中，有几种不同种类的替换类型，它们以前后谓词（Before-After Predicates，BAP）为特征描述：

Before-After Predicates（BAP）	解释
$Skip$	`NULL` / 为空的动作
$x := E$	为 $x$ 赋值为表达式 $E$
$x :\in S$	使 $x$ 赋值为集合 $S$ 中的一个元素
$x : \mid P$	使 $x$ 赋值为满足谓词 $P$ 的一个元素
$f(x):=E$

可以使用 $x : \mid P$ 来代替其他的替换类型，即 $P(x,x')$ ，其可以扩展到对多个变量修改：

$x_1,...,x_n : \mid P$

2 事件

【初始化】定义状态变量的初始化的值。

【状态变量的修改】Before-After Predicates，BAP(x,x')。例如 $x : \mid (x'=x+1) \text{ or } x := x+1$

【三种类型的事件】：

无卫（Non guarded）事件： $P(x,x')$ ，卫 $grd(E)$ ： $\text{TRUE}$
1
2
3
4
event_non_guarded =
BEGIN
x :| BAP(x, x')
END
有卫（Guarded）事件： $G(x) \land P(x,x')$ ，卫 $grd(E)$ ： $G(x)$
1
2
3
4
5
6
event_guarded =
WHEN
G(x)
BEGIN
x :| BAP(x, x')
END
有参（Parameterised）事件： $\exist I.(G(x, I) \land P(x,x',I))$ ，卫 $grd(E)$ ： $\exist I.G(x, I)$
1
2
3
4
5
6
7
8
event_guarded =
ANY
I
WHERE
G(x,I)
BEGIN
x :| BAP(x, x', I)
END

其关于细化的证明义务（PO）规则为：

（ $\Gamma(s,c)$ 表示在关于 $s,c$ 的环境下，一般与 $s,c$ 有关的部分都在 $Axiom$ 中，可以在本章最后的部分：义务证明中查看更详细的内容）

POs	数学表达
Invariant preservation at initialisation (INIT)	$\Gamma(s,c) \vdash Init(x)$ $\Rightarrow I(x)$
Invariant preservation by each event (INV)	$\Gamma(s,c) \vdash I(x) \land G(I,x) \land BAP(x,x',l)$ $\Rightarrow I(x')$
Deadlock freeness (DEAD)	$\Gamma(s,c) \vdash I(x)$ $(grd(e_1) \lor ... \lor grd(e_n))$
Theorems shall be prove (SAFE)	$\Gamma(s,c) \vdash I(x)$ $T_{heorem}(x)$
Events shall be feasible (FIS)	$\Gamma(s,c) \vdash I(x) \land G(I,x)$ $\Rightarrow \exist x'.BAP(x,x',l)$

3 细化

一个项目中可以存在多个 $Machine$ 和 $Context$ ，但它们不能是独立的，这也从侧面解释了“Event-b支持逐步精化地建立系统模型”。

抽象机和上下文之间存在多种关系：一个抽象机可以被另一个抽象机“细化”（refines），一个上下文可以被另一个上下文“扩展”（extends），一个抽象机可以“观看”一个或几个上下文，下图描绘了机器和上下文之间的关系：

"Machines and contexts have various relationships: a machine can be ”refined” by another one, and a context can be ”extended” by another one (no cycles are allowed in both these relationships).

Moreover, a machine can ”see” one or several contexts. An example of machine and context relationship is as follows:"

细化是增加系统的功能、增加细节、改变状态模型。细化一个自动机过程中，可能需要增加新的变量和新的事件。一般一个模型需要进行多次细化才能符合要求。即 Machine 在细化中越来越复杂，越来越细致。 $Context$ 也越来越庞大。 $Machine$ 和 $Context$ 之间的可见性遵循下面的规则：

一个 $Machine$ 可以显式地 SEES（导入）若干上下文（也可以不引入上下文）。
一个 $Context$ 可以显式地 EXTENDS（扩充）若干上下文（也可以不扩充任何上下文）。
上下文扩充的概念具有传递性：当上下文 $C_2$ 显式地扩充另一上下文 $C_1$ 时，它也隐式地扩充了那些被 $C_1$ 扩充的上下文。
当上下文 $C_2$ 扩充上下文 $C_1$ 时， $C_1$ 的集合和常量都能被 $C_2$ 使用。
把细化和扩充关系放一起，不允许出现任何循环。
一个 $Machine$ 最多只能细化另一个抽象机
一个 $Machine$ 显式或隐式 SEES（导入）的上下文必须不小于它所细化的那一个抽象机。

抽象（Abstract）模型使用变量 $x$ ，而具体（Concrete）模型使用变量 $y$ ，那么

对于抽象机：INVARIANTS 为 $I(x)$
对于细化的 $Machine$ ：INVARIANTS 为 $J(x,y)$

$Machine$ 必须保持不变式和联结不变式 $J(x,y)$ （Gluing Invariants，连接具有细化关系的两个 $Machine$ 的不变式）。一个 $Machine$ 最多只能细化一个抽象机，通过引入新的变量、新的不变式和新的事件细化抽象机中的状态或事件。

抽象机之间的细化关系是指对应事件之间具有细化关系，事件之间的细化关系是指对应事件的卫式条件满足卫式条件加强、动作满足模拟关系。

graph LR
MACHINE之间的细化 --"是指"--> EVENT之间的细化
EVENT之间的细化 --"是指"--> GUARD条件加强,动作满足模拟关系

事件的细化

对于事件：

一个新事件：通过 Skip 事件细化得来，即一个不执行任何动作（Action）的无卫无参数事件；
对于一个具体（Concrete）的事件：通过与其对应的抽象（Abstract）事件细化得来。

注意 ⚠️ ：新的事件可能造成系统的活性（Liveness）问题。

我们假设一个抽象事件中有变量（variable） $x$ ，其对应的具体时间中有变量 $y$ ：

抽象事件中的不定式（Invariant）为 $I(x)$ ，对应的，具体事件中的不定式（Gluing invariant）为 $J(x,y)$ 。说明具体事件需要同时满足抽象和其本身参数的不定式；
对于一个如下所示的新事件（即，细化自 Skip 事件的事件）：

其中，细化的具体事件的不定式义务证明（Invariant Preservation PO）为：

$\begin{aligned} & \text{(其他条件，如AXIOMS等)} \\ \land \quad & I(x) \land J(x,y) \land H(y) \\ \Rightarrow \quad & J(x,F(y)) \end{aligned}$
对于一个如下所示的有卫事件：

其中，细化的具体事件的不定式义务证明（Invariant Preservation PO）为：

$\begin{aligned} & \text{(其他条件，如AXIOMS等)} \\ \land \quad & I(x) \land J(x,y) \land H(y) \\ \Rightarrow \quad & G(x) \land J(E(x),F(y)) \end{aligned}$
对于一个如下所示的含参有卫事件：

其中，细化的具体事件的不定式义务证明（Invariant Preservation PO）为：

$\begin{aligned} & \text{(其他条件，如AXIOMS等)} \\ \land \quad & I(x) \land J(x,y) \land H(y,w) \\ \Rightarrow \quad & \exist v. (G(x,v) \land J(E(x,v),F(y,v))) \end{aligned}$

此时，我们考虑一个任意的抽象机及其对应的具体机：

其关于细化的义务推理（PO）规则为：

POs	数学表示
(6) Initialisation (INIT)	$A \land G^C(\alpha ^C) \land W(\alpha ^A, \alpha ^C, x^{A\prime}, x^{C\prime}) \land BAP^C(\alpha^C, x^{C\prime})$ $\Rightarrow J(x^{A\prime}, x^{C\prime})$
Invariant preservation (INV)	$A \land G^C(x^C, \alpha ^C) \land W(\alpha ^A, \alpha ^C, x^A, x^{A\prime}, x^C, x^{C\prime}) \land BAP^C(x^C, \alpha^C, x^{C\prime})$ $\land I^A(x^A) \land J(x^A, x^C)$ $\Rightarrow J(x^{A\prime}, x^{C\prime})$
Event Simulation (SIM)	$A \land G^C(x^C, \alpha ^C) \land W(\alpha ^A, \alpha ^C, x^A, x^{A\prime}, x^C, x^{C\prime}) \land BAP^C(x^C, \alpha^C, x^{C\prime})$ $\land I^A(x^A) \land J(x^A, x^C)$ $\Rightarrow BAP^A(x^A, \alpha ^A, x^{A\prime})$
Guard Strengthening (GS)	$A \land G^C(x^C, \alpha ^C) \land W(\alpha ^A, \alpha ^C, x^A, x^{A\prime}, x^C, x^{C\prime}) \land I^A(x^A) \land J(x^A, x^C)$ $\Rightarrow G^A(x^A, \alpha^A)$

4 证明义务

证明义务规则定义定义了“对一个 Event-B 模型必须证明些什么”。证明义务（proof obligation）并不是为了得到某些信息而进行的操作，它并不是必须的。它的作用只是确定建立的模型是否符合原始需求以及内部需求。

Rodin 平台中有一个称为证明义务生成器的工具，它对上下文和抽象机的正文做一些静态检查，自动确定要证明的东西。这些相继式被送给证明器，在那里完成自动的或者交互式的证明。证明义务规则包括：

INV

不变式保持证明义务规则（Invariant Preservation）：这一证明义务规则保证机器里的每一条不变式被每个事件保持

“Ensuring that each invariant is preserved by each event.”

FIS

可行性证明义务规则（Feasibility PO）：这一证明义务规则的用途是保证非确定性动作的可行性。

“Ensuring that each non-deterministic action is feasible.”

GRD

卫加强证明义务规则：这一证明义务规则的用途是保证一个具体事件的具体卫强于对应的抽象事件的抽象卫。这样就能保证，当具体事件被使能时，抽象事件也能被使能。

“Ensuring that each abstract guard is stronger than the concrete ones in the refining event. This ensures that when a concrete event is enabled then so is the corresponding abstract one.”

MRG

归并证明义务规则：这一证明义务保证，当一个具体事件归并了两个抽象事件时，它的卫应强于那两个抽象事件卫的析取。

SIM

模拟证明义务规则：这一证明义务规则的作用是保证在一个具体事件每一个抽象事件的每个动作，在相应的具体事件里都得到了正确的模拟。

“Ensuring that each action in a concrete event simulates the corresponding abstract action.”

NAT

数值变动式证明义务规则：这一证明义务规则保证，在每个收敛的或者预期事件的卫条件下，我们提出的变动式确实是有自然数值。

“Ensuring that under the guards of each convergent event a proposed numeric variant is indeed a natural number.”

FIN

有穷集变动式证明义务规则：这一证明义务规则保证，在每个收敛的或者预期事件的卫条件下，我们提出的集合变动式确实是一个有穷集。

“Ensuring that a proposed set variant is indeed a finite set.”

VAR

变动量证明义务规则：这一证明义务规则保证，每一个收敛事件都能使我们提出的数值变动式或者有穷集变动式减小。它也保证了每一个预期事件不会增大我们提出的数值变动式或有穷集变动式。

“Ensuring that each convergent event decreases the proposed numeric variant.”

WFIS

非确定性见证证明义务规则：这一证明义务规则保证，在一个具体事件的见证谓词中提出的每个见证都存在。

“Ensuring that each witness proposed in the witness predicate of a concrete event indeed exists.”

THM

定理证明义务规则：这一证明义务规则保证所提出的上下文或及其定理是可证的。定理的重要性在于有可能简化证明。

“Ensuring that a proposed context theorem is indeed provable.”

WD

良好证明义务规则：这一证明义务规则保证，每个有可能病态定义的公理、定理、不变式、卫、动作、变动式或者见证都确实是良好定义的。

“Ensuring that a potentially ill-defined axiom, theorem, invariant, guard, action, variant, or witness is indeed well-defined.”