Compute the weakest precondition for the following sequence of statements as used in axiomatic semantics. Show your work.

a.

a:= (c + 2) / 3 {a 1}

b.

{P1} x:= 2 * (y - 4) {Q1}

{P2} y:= 2 * x 1 {y < 7}

Pre-condition for y:= 2 * x 1 {P2} is ___________________

Post-condition for x:= 2 * (y - 4) {Q1} is ___________________

Pre-condition for x:= 2 * (y - 4) {P1} is ___________________ Hence, the weakest precondition is: