Compute the weakest precondition for the following sequence of assignment statements, for the postcondition given.

a) a := 2 * b + 1;

b := a 3

{b < 0}

b) a := 2*(b 1) 1 given the postcondition {a > 0)

c) if(a==b)

b=2*a+1

else

b=2*a

{b>1}

d)

if(x>y)

y=2*x+1

else

y=3*x-1

{y>3}