Loop Invariant for function to compute factorials

Question

I'm having a hard time correctly identifying a loop invariant for the following function:

F(y)
    X <-- 1
    while (y > 1)
        do x <-- x * y
           y <-- y - 1
    return (x)

I've identified the loop invariant to be x = 1 OR x = y! as that statement holds true as a pre-condition and holds true as a post-condition.

It doesn't seem to hold true for every iteration, as for example if y = 3, then on the first iteration of the loop, x = 1 * 3 which equates to 3 and NOT 3! which equates to 6.

This is where my confusion really is I guess. Some books articles state that a loop invariant is a statement that must equate to true at the beginning or a loop (thus the precondition) and must also hold true at the end of the loop (thus post-condition) but does not necessarily need to hold true part-way through the loop.

What is the correct loop invariant for the function above?

Answer 1

A possible loop invariant would be x⋅y! = y₀! where y₀ is the initial value of y that is passed to the function. This statement is always true, no matter how many iterations of the loop have already been done.

A precondition has to hold before the loop starts, a postconditions has to hold after the loop finishes, and an invariant has to hold no matter how many iterations of the loop have been done (that's why it's called "invariant" -- it doesn't change that it is true).

Generally, there might be different possible invariants for the same loop. For example 1 = 1 will be a true as a invariant for any loop, but to show correctness of an algorithm you usually will have to find a stronger invariant.