Hoare Logic for Factorial
What the Hoare invariant state is the following:


  If you run the code with $X$ equal to some value $x &gt; 0$, then at the end, $F$ will have the value $x!$ ($x$ factorial).


You can check that this is indeed the case.