# 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 > 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!\}$$

• I don't see any sum at the end. Apr 5, 2020 at 16:06

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.