如何利用循环不变式与SMT工具定位程序Bug及推导前置条件？

我正在学习最弱前置条件（weakest preconditions）、循环不变式（loop invariants）以及基于SMT求解器的程序正确性验证。了解到循环不变式可用于证明或证伪程序是否满足后置条件。

我写了一段带Bug的测试程序：遍历整数数轴10次迭代，预期确保x始终不小于0，因此将x ≥ 0设为循环不变式及后置条件，但故意引入了错误：

i = 0
x = user_input  # 假设初始要求x >= 0
while i < 10:
    if x >= 0:
        # Bug：本该保护x不小于0，这里却减1，会让x变负
        x = x - 1  
    else:
        # 正常逻辑：x为负时加1，回到非负范围
        x = x + 1
    i += 1
    # 预期的循环不变式：{ x >= 0 }
# 后置条件：x >= 0

当x初始值为0时，x ≥ 0成立，但执行x = x - 1后x变为负数，明显违反了预期的循环不变式。

我的问题：

1. 在形式验证或基于SMT的方法中，如何通过循环不变式x ≥ 0识别这个Bug？我知道不变式需要在每次迭代的开始和结束时成立，但不清楚如何转化为证明/验证条件来标记代码错误。
2. 我知道可以通过反向推理推导前置条件来确保循环不变式初始成立，但不清楚如何结合循环不变式与后置条件正式推导初始前置条件（比如x ≥ 0），这应该是解决主问题的必要步骤。

希望得到指导，说明如何通过循环不变式（结合最弱前置条件推理及SMT工具）证明该程序不正确，尤其是x初始为0时违反不变式的情况。

问题1：用循环不变式结合SMT识别Bug #

要验证循环不变式I: x ≥ 0是否成立，需要检查三个核心验证条件，只要其中一个不成立，就能证明程序存在Bug：

• 不变式初始化条件：程序进入循环前，不变式必须成立。对应逻辑是「初始状态（i=0，x=user_input）满足I」，也就是x₀ ≥ 0（x₀为初始输入值）。这个条件在你设定的初始要求下是成立的，但后续的保持条件会暴露问题。

• 不变式保持条件：假设迭代开始时不变式I和循环条件B: i < 10同时成立，执行一次循环体后，不变式仍需成立。这是暴露Bug的关键：

  1. 将这个逻辑转化为SMT可检查的公式：(x ≥ 0 ∧ i < 10) → 执行循环体后x ≥ 0
  2. 拆分循环体的两个分支分析：
     • 当x ≥ 0时，执行x = x-1，此时需要x-1 ≥ 0；但结合前提x ≥ 0，存在x=0的情况，此时0-1 = -1 < 0，直接违反不变式。
     • 当x < 0时，执行x = x+1，此时需要x+1 ≥ 0；但迭代开始时I成立（x ≥0），这个分支实际不会触发。
  3. 将上述逻辑编码后交给SMT求解器，它会直接返回反例x=0——这个值满足循环开始时的不变式和循环条件，但执行循环体后违反了不变式，证明程序存在Bug。

• 不变式蕴含后置条件：循环结束后，不变式I要能推导出后置条件P: x ≥ 0。这里I和P是同一条件，所以该条件成立，但前面的保持条件已证明程序不正确。

问题2：结合循环不变式与后置条件推导初始前置条件 #

推导初始前置条件需要结合*最弱前置条件（WP）*和循环不变式的规则，核心是找到能让三个验证条件（初始化、保持、蕴含后置条件）同时成立的最宽松初始状态：

1. 循环的WP规则基础：对于循环while B do S od，若不变式I满足：

   • WP(S, I) ∧ B → I（保持条件：执行一次循环体后不变式仍成立）
   • I ∧ ¬B → P（循环结束后，不变式能推导出后置条件）
     那么程序的初始前置条件就是能推导出I的状态。

2. 针对你的程序的推导步骤：

   • 首先验证I ∧ ¬B → P：循环结束时¬B: i ≥10，结合I: x≥0，显然能推导出后置条件x≥0，该条件成立。
   • 接下来推导WP(循环体, I)（执行循环体后满足I的前置条件）：
     • 分支1（x≥0）：执行x=x-1后要满足x≥0，对应的WP是x-1 ≥0即x≥1。
     • 分支2（x<0）：执行x=x+1后要满足x≥0，对应的WP是x+1 ≥0即x≥-1。
     • 循环体的WP合并后为：(x≥0 → x≥1) ∧ (x<0 → x≥-1)，化简后是x≥1 或 -1≤x<0。
   • 保持条件要求(I ∧ B) → WP(循环体, I)，也就是(x≥0 ∧ i<10) → (x≥1 或 -1≤x<0)。这个公式显然不成立——当x=0时前件成立，后件不成立。
   • 这说明即使初始x≥0，也无法满足不变式的保持条件，因此程序不存在能保证正确性的初始前置条件（除非修改Bug，比如把分支1的x=x-1改成x=x+1，此时保持条件成立，初始前置条件就是x≥0）。

简单来说，推导初始前置条件的本质是反向寻找能支撑「不变式全程成立→满足后置条件」的初始状态，如果找不到这样的状态，就说明程序存在正确性问题。

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