Compute the weakest precondition for each of the following a

Compute the weakest precondition for each of the following assignment statements and post conditions: a = 2 * (b - 1) - 1 {a > 0} b = (c + 10)/3 {b > 6} a = a + 2 * b - 1 {a > 1} x = 2 * y + x - 1 {x > 11}

Solution

(a) a = 2 * (b – 1) – 1 {a > 0}
2 * (b – 1) – 1 > 0 (substitute a value>0)
2 * b – 2 – 1 > 0
2 * b > 3
b > 3 / 2
(b) b = (c + 10) / 3 {b > 6}
(c + 10) / 3 > 6
c + 10 > 6*3
c > 18-10
           c>8
(c) a = a + 2 * b – 1 {a > 1}
a + 2 * b – 1 > 1
2 * b > 2 – a
b > 1 – a / 2
(d) x = 2 * y + x – 1 {x > 11}
2 * y + x – 1 > 11
2 * y + x > 12