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

冯维直 等: 带递归定义的 SMT 公式求解技术综述 509

随着计算机科学技术的发展, 计算机程序逐渐开始在社会各领域获得广泛应用. 对于安全攸关领域的程序, 代
码中任何一点错误都可能造成极大的风险和经济损失. 程序形式化验证方法被提出用于提升程序可信度, 减少代
码错误风险. 对程序进行形式化验证, 是使用数学方法将程序代码和程序需要满足的性质进行建模和表示, 然后从
理论上证明程序代码满足或者违反性质. 程序形式化验证主要基于定理证明、模型检测、自动推理和约束求解等
技术. 一般先在前端的程序代码层次进行分析, 基于程序语义将程序和待验证的性质编码为数学模型, 如迁移系统、
自动机或霍尔三元组等, 然后生成使用一阶逻辑公式表示的验证条件 (verification condition), 最终调用后端的求解
工具进行求解, 证明程序满足待验证性质或得到违反性质的反例.
对带有递归定义 (本文涉及的“递归定义”主要分为两类: 一类为递归数据结构, 另一类为递归函数) 的程序进
行形式化验证, 是程序验证领域, 尤其是函数式程序验证, 广受关注且具有挑战性的重要问题之一. 该领域早期通
常是在程序代码层次进行处理: 包括研究递归数据结构理论的判定算法、对递归函数进行展开、添加递归函数的
前置-后置条件、基于定理证明工具手动进行归纳证明等. 最终生成尽量简单的逻辑公式作为验证条件, 再交由后
端求解器完成求解. 随着后端求解技术的发展, 研究者逐渐开始直接在一阶逻辑公式层次对递归函数进行表示, 并
研究在原一阶逻辑求解框架中加入处理递归数据结构和递归函数的技术. 相比在代码层次处理, 在逻辑公式层次
的好处在于: 一阶逻辑公式的 SMTLIB 标准格式被形式化验证社区广泛认可和应用, 适合研究者在统一的样例上
进行算法研究和实验对比; 后端求解器可以被应用于许多不同的编程语言形式化验证框架中, 具有更大的影响力
和适用性; 另外在逻辑公式层次处理递归定义的特定技术可以更好地与原逻辑公式求解框架相结合. 本文将对这
些在逻辑公式层次求解递归数据结构和递归函数的技术和主流工具进行介绍.
带背景理论的一阶逻辑公式可满足性问题: 命题逻辑是最基础的逻辑形式, 命题逻辑可满足性 (satisfiability,
SAT) 问题是最早被证明的非确定性多项式完全 (non-deterministic polynomial-time complete, NPC) 问题. 但命题逻
辑的表达能力有限, 在实际的程序验证问题中, 往往需要对特定背景理论下的计算进行描述和求解. 于是研究者
将 SAT 问题扩展为可满足性模理论 (satisfiability modulo theories, SMT) 问题, 面向包含多种数据类型的一阶逻辑
背景理论. 其背景理论涉及多种数学和计算机领域内的常用理论, 如布尔理论、线性整数/实数算术、位向量、未
解释函数和数组理论等. 约束霍恩子句 (constrained Horn clause, CHC) 是另一种一阶逻辑公式表示形式, CHC 可
满足性可以被视作 SMT 问题的特殊情况. 相比一般通用的 SMT 问题, CHC 的公式结构更适合表示带有循环结构
的程序, CHC 公式的求解算法一般可以通过计算循环不变式来完成求解 [1] .
递归定义在程序代码和一阶逻辑公式层次的表示: 程序和一阶逻辑公式的递归定义主要分为如下两类.
1) 一类是递归数据结构, 递归数据结构由构造子 (constructor) 定义, 通常包含一个或多个基础情况 (base
case) 和一个或多个递归情形 (recursive case), 通过引用自身的方式构造出复杂的数据对象. 通常包括树状结构
(一般由表示空树的基础构造子和表示非空树, 即根节点与左右子树的递归构造子定义)、列表结构 (一般由空列
表的基础构造子和由头部元素与尾部列表组成的递归构造子定义) 以及基于 Peano 算术定义的自然数 (由表示零
的基础构造子和表示后继函数的递归构造子定义) 等. 对带有递归数据结构的程序进行验证, 通常将递归数据结构
转换为一阶逻辑公式中的代数数据类型 (algebraic data type, ADT), 通过求解 ADT 理论下的 SMT 问题进行验证
(详见第 1.3 节).
2) 另一类是递归函数, 递归函数是定义函数体中会调用自身的函数, 其函数结构通常包含一个用于终止计算
的基础条件和一系列将复杂问题分解为更小同类问题的递归等式. 递归函数通常用来表示程序中一些需要通过循
环或者递归计算的性质, 例如计算列表的长度等. 在一阶逻辑中通常将递归函数的定义分别转化为表示递归基础
情形 (base case) 和递归情形 (recursive case) 的多条包含全称量词的逻辑公理, 该公理描述函数在所有可能输入上
的行为. 递归函数 f 在逻辑上表示为如下的公理:

∀x. (φ(x) → f(x) = base(x) ∧ ¬φ(x) → f(x) = rec(x, f(g(x)))),
其中, φ(x) 表示终止条件, base(x) 表示基础情形; ¬φ(x) 表示未达到终止条件, rec(x, f(g(x))) 定义递归情形下的公
式, 表示递归情形中通过函数 g 构造规模更小的参数并递归调用 f 自身. 递归函数整体转换到在逻辑公式层次进