문제

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

도움이 되었습니까?

해결책

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.

라이센스 : CC-BY-SA ~와 함께 속성
제휴하지 않습니다 cs.stackexchange
scroll top