Hoare Logic for Factorial

Question

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 > 0 \land X = x \}$

1. $F := 1$
2. while $X > 0$ do
3. $\quad F := F \cdot X$
4. $\quad X := X - 1$
5. od

Postcondition: $\{F = x!\}$

Answer 1

What the Hoare invariant state is the following:

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

You can check that this is indeed the case.