不展开循环：将while循环转化为SMT-LIB公式以验证正确性

要完整验证这个while循环的正确性，需要分别证明部分正确性（循环终止时断言成立）和终止性（循环必然会结束），以下是具体的SMT-LIB转化方案：

一、验证部分正确性（循环终止则断言成立） #

部分正确性的核心是定义循环不变式——一个在循环全程始终成立的谓词，需满足三个条件：初始状态成立、循环体执行后保持成立、循环终止时可推导出目标断言。

选择合适的循环不变式 #

针对该循环，选取不变式 I(x) = 0 ≤ x ≤ 10：

• 初始状态x=0显然满足0 ≤ 0 ≤10；
• 若当前x满足I(x)且循环条件x≥0 ∧ x<10成立，执行x=x+1后，x的范围变为1 ≤ x ≤10，仍满足I(x)；
• 循环终止时，循环条件x≥0 ∧ x<10不成立，结合I(x)的x≥0可推出x≥10，再结合I(x)的x≤10，必然得到x=10，符合断言要求。

对应的SMT-LIB公式 #

我们通过断言“部分正确性的否定不可满足”来证明其永真性，代码如下：

; 声明整数变量
(declare-fun x () Int)

; 断言部分正确性的否定，若check-sat返回unsat，则部分正确性成立
(assert (not (and
  ; 1. 初始状态满足不变式
  (implies (= x 0) (and (>= x 0) (<= x 10)))
  ; 2. 循环体执行后不变式保持
  (forall ((x Int))
    (implies (and (and (>= x 0) (<= x 10)) (and (>= x 0) (< x 10)))
             (and (>= (+ x 1) 0) (<= (+ x 1) 10))))
  ; 3. 循环终止时不变式推导出断言
  (forall ((x Int))
    (implies (and (and (>= x 0) (<= x 10)) (not (and (>= x 0) (< x 10))))
             (= x 10))))))

; 检查可满足性
(check-sat)
; 返回unsat则说明部分正确性成立

二、验证终止性（循环必然会结束） #

终止性的核心是找到度量函数（映射到良序集，比如自然数），需满足：循环条件成立时函数值为正，每次执行循环体后函数值严格递减。

选择合适的度量函数 #

针对该循环，选取度量函数 f(x) = 10 - x：

• 当循环条件x≥0 ∧ x<10成立时，10-x的取值范围是1~10，均为正自然数；
• 执行循环体x=x+1后，f(x') = 10 - (x+1) = 9 -x，显然f(x') < f(x)，严格递减。

由于自然数集是良序集，严格递减的正自然数序列必然会终止，因此循环一定能结束。

对应的SMT-LIB公式 #

通过断言“终止性条件的否定不可满足”来证明，代码如下：

; 声明整数变量
(declare-fun x () Int)

; 断言终止性条件的否定，若check-sat返回unsat，则终止性成立
(assert (not (forall ((x Int))
  (implies (and (>= x 0) (< x 10))
           (and (>= (- 10 x) 1) ; 循环条件成立时度量函数为正
                (< (- 10 (+ x 1)) (- 10 x))))))) ; 执行循环体后度量函数严格递减

; 检查可满足性
(check-sat)
; 返回unsat则说明终止性成立

三、综合结论 #

当上述两个SMT查询均返回unsat时，即可证明：该循环必然终止，且终止后断言x==10成立。

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