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?

Loop invariant is NOT the post-condition. Anything you read which stated that is flat-out wrong. If you found something that implied the invariant was also the post condition, please include a link or reference. It's incomplete or misleading. The invariant AND NOT the while condition IS the post-condition. — S.Lott, Dec 05 '11 at 23:14
I guess I definitely missread the autor's statements. I was reading 'Discrete Mathematics with Applications" by Susanna Epp and I assumed that a loop invariant is a combination of the pre/post conditions when it seems that the author meant that the loop invariante simply also ensures the truth of the pre/post conditions. — Brownbay, Dec 05 '11 at 23:26
"author meant that the loop invariante simply also ensures the truth of the pre/post conditions". Given that revised understanding, please **update** your question to ask for the help you really need. — S.Lott, Dec 06 '11 at 00:25

score 6 · Accepted Answer · answered Dec 05 '11 at 23:39

6

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.

answered Dec 05 '11 at 23:39

sth

222,467
53
283
367

Your loop invariant definitely makes sense and holds true for the few examples I've tried... But for the sake of argument, what would be wrong with an alternative loop invariant -- for example: `x <= y!` Is it simply that it's too vague? – Brownbay Dec 05 '11 at 23:45
@Brownbay: The problems usually start when you try to use the loop invariant to show that the program does the correct thing. With a strong loop invariant you can prove that the function will actually return the correct result. Your loop invariant is also completely valid, but it's probably too vague to prove the correctness of the function. My guess would be that with the `x <= y_0!` invariant you can only prove that the algorithm produces something that is smaller or equal to the factorial. – sth Dec 05 '11 at 23:55

score 1 · Answer 2 · answered Dec 06 '11 at 01:00

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.)

Loop Invariant for function to compute factorials

2 Answers2