已知循环不变式时，如何推导最弱前置条件？

背景 #

我已掌握简单if语句的最弱前置条件计算方法，示例如下：

if x > 0:
    x = x - 1
else:
    x = x + 1
# 后置条件: { x >= 0 }

为保证执行后满足后置条件，计算出的最弱前置条件为：

(x>0 ∧ x>=1) ∨ (x<=0 ∧ x+1>=0)

简化后得到：

(x>=1) ∨ (-1<=x<=0)

但我不清楚如何在存在循环且给定循环不变式的场景下，反向推导最弱前置条件。

问题 #

考虑以下循环代码（假设x为整数）：

i = 0
x = user_input
while i < 10:
    if x > 0:
        x = x - 1
    else:
        x = x + 1
# 后置条件: { x >= 0 }

已知循环不变式为 ( { x \geq 0 } )，请通过后置条件和该不变式，形式化推导整个程序的最弱前置条件。

推导过程 #

1. 核心规则回顾 #

结合循环不变式推导最弱前置条件（WP）需遵循三个核心约束：

• 不变式初始化：循环开始前的状态必须满足不变式；
• 不变式保持：若循环迭代前状态满足「不变式 ∧ 循环条件」，执行循环体后仍满足不变式；
• 退出有效性：循环退出时（循环条件不成立），「不变式 ∧ 循环条件取反」需蕴含后置条件。

2. 验证给定不变式的合法性 #

首先验证给定的不变式 ( I: { x \geq 0 } ) 是否符合约束：

• 退出有效性：循环退出条件为 ( i \geq 10 )，此时 ( I \land (i \geq 10) ) 即 ( x \geq 0 \land i \geq 10 )，显然蕴含后置条件 ( { x \geq 0 } )，约束成立；
• 不变式保持：当迭代前满足 ( I \land (i < 10) )（即 ( x \geq 0 ) 且 ( i < 10 )，x为整数）：
  • 若 ( x > 0 )（即x≥1），执行x=x-1后x≥0；
  • 若 ( x = 0 )，执行x=x+1后x=1≥0；
    执行循环体后始终满足I，约束成立；

3. 反向推导整个程序的最弱前置条件 #

程序执行流程为：i=0 → x=user_input → 循环。从后往前反向推导：

1. 循环的前置条件：根据不变式初始化约束，循环开始前需满足 ( I: { x \geq 0 } )；
2. x=user_input的前置条件：执行该赋值后要满足 ( x \geq 0 )，等价于输入值本身满足 ( user_input \geq 0 )；
3. i=0的前置条件：该赋值对x的值无影响，因此前置条件与x=user_input的前置条件一致。

最终，整个程序的最弱前置条件为：

user_input ≥ 0

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