如何推导赋值语句a = a + 2*b -1 {a>1}的最弱前置条件？

首先得明确赋值语句的最弱前置条件（WP）核心规则：对于赋值操作 x := E，如果后置条件是 Q，那么它的最弱前置条件就是把 Q 中所有出现 x 的位置，全部替换成赋值右边的表达式 E。这是推导这类问题的关键，咱们一步步来拆解你的问题：

步骤1：写出WP的表达式 #

你的问题是推导 a = a + 2*b - 1 {a > 1} 的最弱前置条件，用WP符号表示就是：

WP(a := a + 2*b - 1, a > 1)

步骤2：应用替换规则 #

根据赋值语句的WP规则，我们需要把后置条件 a > 1 里的所有 a，替换成赋值右边的表达式 a + 2*b - 1，得到：

a + 2*b - 1 > 1

步骤3：整理不等式 #

接下来只需要解这个不等式就行：

• 先把常数项移到右边：a + 2*b > 1 + 1 → a + 2*b > 2
• 再把含 a 的项移到右边：2*b > 2 - a
• 两边除以2（注意2是正数，不等号方向不变）：b > (2 - a)/2 → 化简后就是 b > 1 - a/2

为什么你的思路不对？ #

你之前尝试直接让 a = a + 2*b -1 成立，推导出 2b-1=0，这是混淆了两个完全不同的逻辑：

• 最弱前置条件要求的是执行赋值操作之后，后置条件a>1成立，也就是执行后的a（即原来的a+2b-1）满足大于1，而不是让赋值的等式本身成立（这个等式本身除非2b-1=0否则不可能成立，但这和后置条件无关）。

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