Compute the weakest precondition for each of the following assignment statements and postconditions: 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}

a) b > 3/2

b) c > 8

c) b > 1 - a/2

d) y > 6 - x/2

Explanation:

a)

a = 2 × (b - 1) - 1   {a > 0}

2 × (b - 1) - 1 > 0

2b - 2 - 1 > 0

2b - 3 > 0

2b > 3

b > 3/2

b)

b = (c + 10) / 3 {b > 6}

(c + 10) / 3 > 6

multiply both side by 3

((c + 10) / 3) × 3 > 6 × 3

c + 10 > 18

c > 18 - 10

c > 8

c)

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

a + 2 × b - 1 > 1

a + 2b - 1 > 1

a + 2b > 1 + 1

2b > 2 - a

divide both sides by 2

2b/2 > 2/2 - a/2

b > 1 - a/2

d)

x = 2 × y + x - 1 {x > 11}

2 × y + x - 1 > 11

2y + x - 1 > 11

2y + x > 11 + 1

2y + x > 12

2y > 12 - x

divide both sides by 2

2y/2 > 12/2 - x/2

y > 6 - x/2