计算最弱的前提条件

Question

计算以下每个赋值语句和后置条件的最弱前置条件：

a = a + 2 * b - 1 {a > 1}

尝试：

两边都有a

0 = 2b -1

1/2 = b 是最弱的precon

回答： b > 1 - a/2

你是怎么得到这个答案的？

Answer 1

这里是答案：

a = a + 2 * b - 1 {a > 1}

我们将a in {a > 1} 替换为a + 2 * b - 1

a + 2 * b - 1 > 1
a + 2 * b > 2
2 * b > 2 - a
b > 1 - a / 2`

我想你已经找到了答案，但对于那些可能会来这里寻找这个答案的人。