Consider the following program, where :$=$ denotes variable assignment. Assume only integer variables.

$y$:$=w+1$;

$z$:$=y*w$;

$x$:$=\frac{1}{z}$

We don't want the last instruction to divide by zero. In order to avoid this contingency, what needs to be True in the initial

state?

Hint: insert the assertion$/$comment $\{z0\}$ before the line that assigns to $x.$ Then use the "magic" technique

described in Appendix D$.2$ of the IFM book to determine what must be True before each of the preceding

assignments.

a$.)0$

b$.w>0$

c$.w0$

d$.)-1$

e$.z0$