形式化建模与基于SMT的参数化验证

### 形式化建模与基于SMT的参数化验证 #### 1. 语言的作用与限制 有一种语言可以被视为从快照中检索数据的查询语言，也可以作为一种约束可注入流程的数据对象组合的机制。例如，`guard input(y:string, z:string) →y ̸= z` 会返回所有彼此不同的字符串对。从这个（无限的）字符串对集合中选择一个答案，可以看作是对 `y` 和 `z` 的（受约束的）用户输入。不过，如果超出这种防护查询语言的范围（例如引入全称量化），会影响基于SMT对所得DAB进行验证的可靠性和完整性。 #### 2. 任务、事件及对数据的影响 ##### 2.1 更新逻辑 给定数据模式 `D`，更新规范 `α` 是一个对 `<G, E>`，其中： - `G = α.pre` 是一个对 `D` 的防护，形式为 `q(⃗x) ←Q`，称为前置条件。 - `E = α.eff` 是一个改变 `D` 快照的效果规则，有以下几种形式： - **插入并设置（Insert&Set）**：`INSERT ⃗u INTO R AND SET x1 = v1, ..., xn = vn`，其中 `⃗u, ⃗v` 是 `⃗x` 中的变量或 `D` 中的常量对象，`⃗x` 是不同的案例变量，`R` 是 `D.repo` 中的关系模式，其元数（和类型）与 `⃗u` 匹配。`INSERT` 或 `SET` 部分可以省略，得到纯插入规则或设置规则。 - **删除并设置（Delete&Set）**：`DEL ⃗u FROM R AND SET x1 = v1, ..., xn = vn`，条件与插入并设置规则类似。`AND SET` 部分可省略，得到纯（存储库）删除规则。 - **条件更新（Conditional update）**：`UPDATE R(⃗v) IF ψ(⃗u, ⃗v) THEN η1 ELSE η2`，其中 `⃗u` 是包含 `⃗x` 中变量或 `D` 中常量对象的元组，`ψ` 是无存储库的防护（称为过滤器），`R` 是存储库关系模式，`⃗v` 是新变量的元组，`ηi` 要么是 `R(⃗u′)` 形式的原子公式，要么是嵌套的 `IF ... THEN ... ELSE`。 更新规范 `α` 在给定数据快照中可执行的条件是，该快照中至少有一个对 `α.pre` 的答案。如果有，流程执行器会非确定性地选择一个答案，将 `α.pre` 的答案变量绑定到 `D` 中的相应数据对象。一旦为答案变量选择了绑定，效果规则 `α.eff` 就会用该绑定实例化并执行。 不同效果规则对当前数据快照的影响如下： - **插入并设置规则**：绑定用于同时在某个存储库关系中插入一个元组，并更新一些案例变量。由于存储库关系没有显式主键，插入元组时会生成一个新的主键。有两种插入语义：多集插入语义下，更新总是能成功插入元组；集合插入语义下，只有当满足键约束时更新才会提交。 - **删除并设置规则**：更新的可执行性取决于绑定选择的要从 `R` 中删除的元组 `⃗u` 是否实际存在于 `R` 的当前实例中。如果存在，绑定用于同时从 `R` 中删除 `⃗u` 并更新一些案例变量。 - **条件更新规则**：对 `R` 中的每个元组进行批量操作。如果元组通过规则关联的过滤器，则根据 `THEN` 部分更新；否则根据 `ELSE` 部分更新。 以下是一些示例： - **插入并设置规则示例**： - 在工作招聘示例中，创建新案例时，`InsJobCat` 规范选择一个工作类别并将其分配给案例变量 `jcid`。 ```plaintext InsJobCat.pre ≜getJobType(c) ←JobCategory(c) InsJobCat.eff≜SET jcid = c ``` - 案例收到申请时，`InsUser` 规范从 `User` 中选择用户ID并分配给 `uid`。 ```plaintext InsUser.pre ≜getUser(u) ←User(u, n, a) InsUser.eff≜SET uid = u ``` - `CheckQual` 规范用于快速评估候选人是否有资格直接获得录用通知。 ```plaintext CheckQual.pre ≜isQualified(q : Bool) ←true CheckQual.eff≜SET qualif = q ``` - `EvalApp` 规范用于对未直接被判定为合格的候选人进行更细粒度的评估，并将分数记录到存储库中。 ```plaintext EvalApp.pre ≜getScore(s : NumScore) ←1 ≤s ∧s ≤100 EvalApp.eff≜INSERT ⟨jcid, uid, s, undef⟩INTO Applicatio ```