Note that the loop is not the outermost construct in your program; that is a sequential composition. In order to apply this rule, you first need to take care of the initial assignments. In this case that is straightforward: you get that the formula $x>0\wedge y>0\wedge z=0\wedge u=x$ holds after $z:=0; \ u:=x$.
For the loop rule, you need three formulas: a precondition $P$, a postcondition $Q$, and an invariant $R$, satisfying the premises of the rule. The precondition $P$ also needs to follow from the formula we obtained above. The postcondition $Q\equiv z=x*y$ is already given in your initial triple. What is left to do is therefore to find $P$ and $R$ such that
- $(x>0\wedge y>0\wedge z=0\wedge u=x)\to P$,
- $\{P\}\ z:=z+y;\ x:=x-1\ \{R\}$,
- $(R\wedge u\neq 0)\to P$,
- $(R\wedge u=0)\to z=x*y$.
A special case which may be worth trying here is to assume that the third condition holds with equality, i.e. $P\equiv (R\wedge u\neq 0)$. This reduces the problem to finding $R$ such that
- $(x>0\wedge y>0\wedge z=0\wedge u=x)\to (R\wedge u\neq 0)$,
- $\{R\wedge u\neq 0\}\ z:=z+y;\ x:=x-1\ \{R\}$,
- $(R\wedge u=0)\to z=x*y$,
which is essentially an application of the usual while rule. As for how to find $R$, that is in general a very tricky problem. You seem to be looking in the right direction, but you invariant still needs some work (checking which of the conditions it fails, and how, may help with that).
R
is the loop invariant. Finding it is a creative step. If you haveR
, pack intoP
all that you know prior to the loop, verify the three conditions of the rule (by recursively annotating the loop body, in particular) and you are done. (If it doesn't work, your loop invariant is wrong. Try again.) So, whatR
have you tried? What does the program do? $\endgroup$P
is the pre condition. Part of it is given as precondition of the whole program; you want to add the results of the first line. $\endgroup$