收缩与B工具包：理论与实践的探索

# 收缩与B工具包：理论与实践的探索 ## 1. 引言 在系统工程领域，基于模型的精化方法具有显著的理论深度和实用价值。B方法在这方面取得了巨大成功，其构建的系统在法国铁路等领域广泛应用。然而，精化方法存在一定的局限性，抽象和具体模型之间的关系必须恰到好处，才能完成精化证明义务（POs），这忽略了以人类为中心的需求工程，可能阻碍系统的透明构建过程。 为了改善这种情况，收缩（Retrenchment）的概念被引入。它允许在类似于精化的形式框架内描述“几乎但不完全是精化”的关系，从而能够描述和分析更广泛的系统演化场景。不过，这种灵活性是以牺牲精化提供的保证为代价的。 如果精化能够从机械化中获益，那么收缩也同样如此。本文旨在描述将收缩纳入B工具包的实验，B工具包是B方法的两种商业实现之一。 ## 2. 为收缩扩展B方法 ### 2.1 语法、证明义务和示例 在B方法中，精化将目标描述为源抽象的扩展。而收缩是两个抽象机器之间的关系，因此引入了新的`RETRENCHMENT`构造。该构造引用相关的机器，但不影响它们的语法和处理。表1展示了其语法： | 语法类别 | 定义 | | --- | --- | | RETRENCHMENT | 标识符 | | FROM | 标识符 | | TO | 标识符 | | RETRIEVES | 谓词 | | OPERATIONS | 分支 | | END | - | | 分支 | 分支 ; 分支声明 | | 分支声明 | RAMIFICATIONS 标识符<br>LVAR 标识符列表<br>WITHIN 谓词<br>CONCEDES 声明 谓词<br>OUTPUT 谓词<br>NEVERTHELESS 谓词<br>END | | 标识符列表 | 标识符列表 , 标识符 | | 标识符 | - | 对于给定的操作，`RAMIFICATIONS`子句包括`LVAR`子句（允许引入“逻辑变量”）、`WITHIN`子句（用于约束操作PO的前件）以及`CONCEDES`、`OUTPUT`和`NEVERTHELESS`子句（用于操作PO的后件）。操作PO如下： \[ICf ∧ ICt ∧ (Qf ∧ R ∧ W) ⇒ Qt ∧ [St]¬[Sf]¬(((R ∧ O) ∨ D) ∧ E)\] 其中，$ICf$、$ICt$是源/目标静态上下文，$Qf$、$Qt$是源/目标前置条件，$Sf$、$St$是源/目标谓词变换器，$R$、$W$、$O$、$D$、$E$分别是检索、范围内、输出、让步和尽管如此关系。 初始化PO为： \[ICf ∧ ICt ⇒ [It]¬[If]¬(R)\] 以下是一个收缩的小示例： ```plaintext MACHINE abc MACHINE def VARIABLES aa, bb, cc SEES Bool TYPE INVARIANT aa ∈ N ∧ CONSTANTS MaxNum bb ∈ N ∧ PROPERTIES MaxNum ∈ N cc ∈ N VARIABLES dd INITIALISATION aa := 0 ∥ INVARIANT dd ∈ N bb := 1 ∥ INITIALISATION dd := 0 cc := 2 OPERATIONS OPERATIONS my plus ≜ aa := bb + cc resp ←− my plus(ee, ff) ≜ PRE ee ∈ N ∧ ff ∈ N ∧ ee ≤ MaxNum ∧ ff ≤ MaxNum THEN IF ee + ff ≤ MaxNum THEN dd := ee + ff ∥ resp := TRUE ELSE dd := 0 ∥ resp := FALSE END END END END RETRENCHMENT abc to def FROM abc TO def OPERATIONS RAMIFICATIONS my plus WITHIN bb = ee ∧ cc = ff CONCEDES (resp = TRUE ∧ dd = aa) ∨ (resp = FALSE ∧ dd = 0) END END ``` ### 2.2 类型检查 B方法要求在证明涉及集合论变量的谓词之前，必须进行类型检查。通过扩展“check”谓词，可以对收缩构造进行类型检查。假设源机器$Mf$和目标机器$Mt$之间存在收缩关系，操作分别为$opf$和$opt$。 表4展示了收缩构造的类型检查规则： | 前件 | 后件 | | --- | --- | | Mf,Mt,N,vf,vt,rmDup(cf, ct),<br>rmDup(Sf, St),rmDup(Tf, Tt),rmDup(af, at),<br>rmDup(bf, bt),Xf,Xt,xf,xt 都不同<br>操作 of 的名称与操作 o 的名称相同，并且都包含在操作 ot 的名称中<br>给定(Xf), 给定(Xt),<br>给定(Sf), 给定(St),<br>给定(Tf), 给