Finding a Hoare logic correctness proof for a Repeat-Until loop
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&gt;0\wedge y&gt;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&gt;0\wedge y&gt;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&gt;0\wedge y&gt;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).