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

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

手工构造的 102 个样例分为两类.
1) 第 1 类样例的背景来源于我们 2024 年基于 Scala 验证方法对 Chisel 硬件电路设计进行参数化验证的工
作 [73] . 这个工作中为了能表示任意位长的位向量类型, 使用整数来模拟位向量的运算. 使用整数模拟位向量运算时
涉及大量以 2 为底的幂函数和对数函数计算. 例如取位向量 R 的低 m 位得到位向量 , 需要用取模计算来表示位
S
m
向量对应数值的关系: S.v = R.v mod 2 , 其中 S.v 和 R.v 表示位向量对应的数值. 该工作将电路中信号需要满足的
性质表示为数学公式, 在程序中用程序规约 (specification) 进行表示, 然后从程序规约中生成验证条件 (verification
condition), 基于 SMT 求解器进行求解. 验证条件往往包含大量幂函数、对数函数相关计算 (且包括取模、除法等
非线性计算) 的求解, 为了使求解器能处理这些问题, 在文献 [73] 中我们使用 Stainless 工具提供的接口, 在程序层
次手工书写归纳推理证明过程和进行验证条件公式化简.
我们从上述问题背景下提取 SMT 公式, 注意到这些 SMT 公式所包含的重点函数定义, 如幂函数、对数函数
等均为递归函数. 在本文中我们考察在不经过程序层次用户手工书写归纳推理证明对公式进行化简的情况下, 直
接使用现有求解工具对这些包含递归函数和复杂计算的 SMT 公式进行自动求解的能力.
第 1 类样例我们选取两个关键整数递归函数 pow2(x) 和 bitLen(x). 从它们对应的数学性质直接生成 SMT 公
式. 然后直接使用现有求解工具进行实验. 这里两个函数的参数和返回值均为自然数. pow2 函数用于计算 2 的自
然数次幂, 表 3 中 ∀x,y ∈ N. 2 x+y = 2 ·2 是它相关的一个待验证数学性质举例. bitLen 函数表示数值 x 的二进制位
x
y
向量形式需要的位长. 它实际上可以用于计算参数为正整数、返回值取整的 2 为底的对数函数, 但 bitLen 具有更
0 x > 0 时,
直观的硬件类型背景, 因此本文选择它作为样例. 令 x = 0 时返回 ; x = 1 时, 对应二进制 x = 1 (2) , 需要 1
位表示; x = 2 时, 对应二进制 x = 10 (2) , 需要 2 位表示; 以此类推有递推关系 bitLen(x) = bitLen(⌊x/2⌋)+1, 对 x 为正
整数成立. 注意这里 bitLen 函数的递推关系中出现了取整除法运算, 而现有的整数递归函数样例中一般只考虑线
x 的递
性加法, 例如最简单的 f(x) = a f(x−1)+b 形式, 递推关系是从 x−1 到 x, 对应弱数学归纳法, 而从 ⌊x/2⌋ 到
推关系一般需要强数学归纳法来进行求解. 因此这里选取 bitLen 函数可以提升样例中递归函数递推关系类别的多
样性.
2) 第 2 类样例来源于被广泛使用的离散数学教材 [74] 中递推函数相关的例题和课后习题. 其中主要包括斐波
拉契数列和其他类似的递推数列函数, 待求解性质为递推数列需要满足的数学性质. 选取这部分样例的原因和
,
bitLen 函数类似, 由于斐波拉契数列相关性质涉及从 x−1 x−2 到 x 的递推关系归纳证明, 一般需要强数学归纳来
求解, 用于丰富样例涉及的求解技术类别. 另外这部分例子来源于实际的数学问题, 更具有应用意义.
● ADT 和整数混合理论样例
这一部分样例中包含了 251 个例子, 最早由 Reynolds 等人在文献 [31] 中提供, 在后续 ADT 和递归函数求解
相关文献 [13,15,47] 中也被部分沿用. 这部分样例由代数数据类型和整数类型混合组成, 涉及的逻辑主要是 SMTLIB
标准格式中的 UFDTLIA 理论, 即未解释函数 (UF)、代数数据类型 (DT) 和线性整数 (LIA) 混合理论. 这些例子从
带有 list、tree、queue 和 heap 等递归数据结构的程序验证问题中产生.
以 list 为例, 样例中的 list 表示每个元素为整数的列表 (类型写作 Int, 为 SMTLIB 标准中的整数类型, 表示数
学意义上的整数, 注意它与 C++等程序语言中的整型有区别). 样例中对不同的 ADT 结构定义用于表示其计算或
者操作的递归函数, 这里我们以在 list 上定义 len 和 append 函数为例. 它们分别表示 list 长度的计算和在 list 尾端
添加一个 list 的操作. 待求解性质为定义的递归函数线性计算, 表示性质分别为: 对任意 list x 和 y, x 尾端添加 y 后
得到的新列表长度等于 y 尾端添加 x 的新列表长度; 对任意 list x 和 y, x 尾端添加 y 后得到的新列表长度等于 x 的
长度加上 y 的长度.
251 个例子中包括 168 个待证明的问题和 83 个性质不成立的问题. 待证明问题需要证明性质成立, 性质将在
SMT 文件中被取反, 当 SMT 求解器返回 UNSAT 时表示反例不存在, 证明性质成立. 性质不成立的问题一般是将
原问题中递归函数定义或待证明性质进行简单改动所得到, 目标是让求解器求解出性质不成立的反例, 当 SMT 求
解器返回 SAT 时表示找到一个不满足性质的反例. 以表 4 中待求解性质为例: 对于 ∀x : list,y : list. len((append(x,y))) =
len(x)+len(y), 在 SMTLIB 中取反, 表示为如下断言.