Hoare Logic for Factorial I came across this hoare logic for factorials but I don't quite understand it. We multiply F and X but we're not adding up all values of F so how do we get the sum/factorial at the end?

Precondition: $\{ X &gt; 0 \land X = x \}$


$F := 1$
while $X &gt; 0$ do
$\quad F := F \cdot X$
$\quad X := X - 1$
od


Postcondition: $\{F = x!\}$
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.