Page 49 - 《软件学报》2026年第2期

528 软件学报 2026 年第 37 卷第 2 期

变式. 在本文中, 我们考虑的主要问题是带有递归结构的 SMT 公式求解, 由于递归函数定义一般具有基础步骤和
递归步骤, 这一形式类似于迁移系统中的起始状态和状态迁移, 可以分别对应将递归函数编码为 CHC 形式. 于是
除了上述直接在 SMT 层面进行求解的技术外, 还可以将复杂的 SMT 问题编码为 CHC, 然后进行求解. 这一方法
往往可以利用 CHC 求解技术计算原问题中递归函数定义的归纳不变式的优势, 来求解原 SMT 方法无法求解的问
题, 作为对直接面向 SMT 求解方法的一种补充. 下面首先介绍求解 CHC 问题的主流方法框架, 然后介绍针对带有
递归结构 CHC 问题进行求解的技术.
4.1 约束霍恩子句

约束霍恩子句 (CHC) 是一阶逻辑的一部分, 通常用于程序验证和程序合成问题中. 一个 CHC 通常表示成如
下形式的公式:

∀V. (φ∧ p 1 (X 1 )∧...∧ p n (X n )) → h(X).
令 T 表示一阶逻辑的背景理论, 如线性实数算术理论、Bool 理论或理论的组合, φ 是在背景理论下的约束
(constraint), V 是变量, X i 是 V 上的项, p 1 ,..., p n ,h 是谓词, p i [X i ] 是谓词在一阶逻辑项上的应用. 通常将 p i (X i ) 形式
的公式称为一个原子公式 (atom), h(X) 被称为 CHC 公式的 head 部分, 它是一个原子公式或者 false. ∀V. (φ∧ p 1 (X 1 )
∧...∧ p n (X n )) 通常称为 CHC 公式的 body 部分. 如果 head 是一个形如 p(t 1 ,...,t n ) 的原子公式, 那么称谓词 p 是一
个 head predicate. 对于 head 是一个原子公式的子句, 称它为 definite 子句, head 是 false 的子句称为 goal 子句.
4.2 CHC 可满足性
对于一个 CHC 公式的集合 Π, 称它的 T-model 是它的模型 M 在背景理论 T 下的扩展, 该扩展带有对每个谓
词 p i 的一阶逻辑解释, 该解释使 M 中 Π 的所有子句为 true. 从谓词 p i 到背景理论 T 中公式的替换 σ, 当 Πσ 在 T
理论中有效 (valid), 即公式在变量的任意赋值均为真时, 称该替换为 Π 的 T-solution.
例 14: 我们用一个程序验证中的问题来解释上述可满足性相关定义, 如下.
1 assume (x <= 0)
2 while (x < 5) {
3 x = x + 1 ∀x. x ⩽ 0 → Inv(x)
4 } ∀x,y. Inv(x)∧ x < 5∧y = x+1 → Inv(y)
5 assert (x < 10) ∀x. Inv(x)∧¬(x < 5)∧¬(x < 10) → false
给定例 14 代码左边的程序, 它假设前置条件为 x <= 0, 经过一个循环, 要验证跳出循环后满足性质 x < 10. 将
程序编码为 CHC 问题, 用未解释谓词 Inv 表示程序中的循环不变式, 那么程序待验证断言的正确性可以通过
CHC 的可满足性得到. 求解右边的 CHC 公式, 本例的 T-model 可以视作对算术理论带有对谓词 Inv 的如下解释的
扩展:

M
Inv = {z | z ⩽ 5}.
且例 14 代码右边的 CHC 公式有一个 T-solution, 将 Inv 进行如下定义:

Inv = λz. z ⩽ 5,
将这一定义代回 CHC 公式, 可以轻易地验证原公式是 valid, 即它和我们的定义相符合.
CHC 的提出主要用于解决程序验证问题, 将程序编码为 CHC 公式后, CHC 公式和原程序验证问题有如下
的对应关系: 1) 一个程序满足待验证性质当且仅当其对应的 CHC 公式是可满足的. 2) CHC 公式的模型对应原
程序中的验证证明 (verification certificate), 如循环不变式. 3) CHC 公式不可满足对应一个原程序中违反性质的
反例. 在本文中我们主要将关注利用 CHC 来求解带有递归函数和归纳数据结构的问题, 为了和其他方法/工具
进行统一比较, 我们将对 SMT 公式进行编码和转换, 表示为 CHC 的形式然后求解, 下面介绍具体的求解和编
码技术.