基于SMT的循环不变量验证是否需要枚举变量取值？

先看你给出的示例循环代码：

i = 0
while i < 10:
    i += 1

当你错误选择{i ≠ 7}作为循环不变量时，SMT求解器完全不需要枚举i的具体取值，而是通过符号化逻辑推理直接检测出这个不变量不合法，核心过程如下：

循环不变量的验证要求 #

合法的循环不变量必须满足三个核心条件，这里问题出在保持性（即每次执行循环体后，不变量仍成立）：

• 初始化成立：循环开始前（i=0），不变量i≠7成立；
• 保持性：若进入循环时，不变量i≠7和循环条件i<10同时成立，执行循环体i +=1后，不变量仍需成立；
• 终止后有用：循环终止时（i≥10），不变量能辅助证明目标性质（这里暂不涉及）。

SMT求解器的符号化验证过程 #

对于保持性条件，求解器会将其转化为逻辑蕴含式，用符号变量代表循环执行前的状态（记为i_old），执行后的状态为i_new = i_old + 1，保持性的逻辑公式为：

(i_old ≠ 7 ∧ i_old < 10) → (i_old + 1 ≠ 7)

SMT求解器的任务是判断这个蕴含式是否永真（即对所有整数i_old都成立）。判断永真的等价方式是检查其否定式是否可满足：

i_old ≠ 7 ∧ i_old < 10 ∧ (i_old + 1 = 7)

求解器会基于整数理论的推理规则，化简这个公式：

• 由i_old +1 =7可直接推导出i_old=6；
• 代入前两个条件：6≠7且6<10，均成立。

这说明该否定式是可满足的，存在i_old=6这个反例：当循环前i=6时，满足不变量和循环条件，但执行循环体后i=7，违反了不变量。因此求解器可以直接返回这个反例，证明{i≠7}不是合法的循环不变量。

关键结论 #

SMT求解器全程采用符号化推理：它不枚举具体数值，而是通过逻辑公式的可满足性检查，直接推导是否存在破坏不变量的状态。只要能找到让保持性条件不成立的符号化反例，就能判定不变量不合法。

内容的提问来源于stack exchange，提问作者desert_ranger