如何计算if-else分支程序的最弱前置条件（weakest condition）

数据老陈

2026-10-1

最弱前置条件正确推导过程

if(x < y) 
    x = x + 1;
else
    x = 3 * x;
// 后置条件：{x < 0}

霍尔逻辑中，if分支语句的最弱前置条件计算公式为：

WP(if B then S1 else S2, Q) = (B → WP(S1, Q)) ∧ (¬B → WP(S2, Q))
其中B是分支判定条件，S1是if分支语句，S2是else分支语句，Q是后置条件，A→B表示逻辑蕴含（等价于¬A ∨ B）。

分别计算两个分支赋值语句的最弱前置
- if分支语句x = x + 1的后置是x < 0，代入赋值规则（将后置条件中的x替换为赋值语句右侧的表达式），得到WP(S1, Q) = x + 1 < 0，即x < -1
- else分支语句x = 3 * x的后置是x < 0，代入赋值规则得到WP(S2, Q) = 3 * x < 0，即x < 0
代入if分支规则展开
整个语句的最弱前置为两个蕴含式的合取：
```
(x < y → x < -1) ∧ (x ≥ y → x < 0)
```
逻辑化简
将蕴含式转换为析取形式后可得：
```
(x ≥ y ∨ x < -1) ∧ (x < y ∨ x < 0)
```
进一步化简可得到三种场景的结果：
- 允许前置条件包含y：完整最弱前置为x < -1 ∨ (x ≥ y ∧ x < 0)，即只要x小于-1，或者x在[-1, 0)区间且x大于等于y，都可以满足后置条件
- 要求前置条件仅包含x（对任意y都生效）：只有当x < -1时，不管y取何值，两个分支执行后都能满足x < 0，也就是你最初算出的结果
- 若题目隐含else分支必然执行（即x ≥ y恒成立）的前提，此时最弱前置简化为x < 0，也就是你看到的标准答案。