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.

Answer 2

The loop invariant can be derived from the post condition, a little intuition and some algebra-like reasoning.

You know one part of the post condition: x == Y!, where Y is the initial value given as an argument. y is a variable who's value changes. And that's the rest of the post condition, BTW: y == 1.

What's true on each pass? Reason backwards.

On the last pass x == Y*Y-1*...*2 and y == 2.

Before that? x == Y*Y-1*...*3 and y == 3.

Before that?

What is true initially, when y == Y?

Finally. Given the post-condition and the invariant, what precondition is the weakest set of statements required to set things in motion? The code suggests, x=1 and y=Y.

You know that each time through the loop, something must change and the program must provably advance the state toward the post-condition. Is that true? Is there a natural-valued function of the loop state which provable decreases toward zero? (This seems like a trick question because the y variable seems to do that trivially. It's not obvious in many real-world loops, so you have to ask the question of your loop design.)