Problem $3$: Program Verification I

Consider the following program fragment:

$x$:$=x+2$

$y$:$=y**x$

$z$:$=z-y$

Hoare Triple Construction: Define a Hoare triple $\{P\}S\{Q\},$ where $S$ is the program above. Let $Q$ be $z>0.$ Construct a suitable precondition $P$ such that the triple is valid.

Compute the weakest precondition $($WP$)$ for the program such that $Q$ holds after execution. Show the step$-$by$-$step derivation.

Program Reasoning:

$($a$)$ Does the computed weakest precondition place any restrictions on the initial values of $x,y,z?$ If so$,$ explain these restrictions in detail.

$($b$)$ How would the precondition change if $Q$ were $z0$ instead of $z>0?$