Explaining a loop invariant

Question

This is a question from a past exam paper.

Why does the loop invariant say i<=n when the loop test says i<n.

Is an appropriate answer: It says i<=n as i will equal n on the failing condition of the while loop. Therefore the 6th iteration of i will equal the n value 6 on the failing condition. However, the while loop itself states i<n as i starts at 0 and will finish looping once i is equal to 5.

private int n =6;

public int fact(){
    int i = 0;
    int f = 1;

    /**loop invariant
     * 0<=i<=n
     * f=i!
     */
    while(i<n){//loop test
        i=i+1;
        f=f*i;
    }

    return f;
}

Oh, wait. It's because of the `i=i+1` in there. Didn't even look at that. Yeah, your answer is correct. And @Keppil almost, but the invariant has to be true at the beginning AND end of the loop. — Phillip Schmidt, Aug 29 '12 at 22:32
Please stop prepending all your questions with "java" - it's in your tags where it belongs. =) — J. Steen, Sep 19 '12 at 11:38

Code-Apprentice · Answer 1 · 2012-08-30T00:02:24.390

1

A loop invariant is a condition that must be true during every iteration of a loop. In this example, we are considering what are the possible values of the variable i. When the loop starts, the value of i is 0. On the last iteration of the loop, i is incremented to n at the beginning of the loop and then another calculation is done. Therefore, the value of i satisfies the condition 0<=i<=n during the execution of this loop.

edited Aug 30 '12 at 00:02

answered Aug 29 '12 at 22:25

Code-Apprentice

81,660
23
145
268

In other words, although the invariant at the start of the body of the loop is `0 – MRAB Aug 29 '12 at 22:29

Fabian Barney · Accepted Answer · 2012-08-30T09:00:11.430

Because Post-Condition is i==n when the loop is left. Pre-Condition when entering the loop is i==0. Inside the loop i is counting up towards n. So the invariant is 0 <= i <= n.

I omitted the invariant parts for f in my exlanation. This is not really sufficient since the invariant must capture the correctness and the meaning of the loop.

private int n = 6;

public int fact(){
    int i = 0;
    int f = 1;

    /* loop invariant: 0 <= i <= n && f == i! */
    /* PRE: i == 0 && f == i! */
    while (i < n) {
        i = i + 1;
        f = f * i;
    }
    /* POST: i == n && f == i! */

    return f;
}

Phillip Schmidt · Answer 3 · 2012-08-29T22:40:12.247

0

On the final iteration of the loop, i starts at five and then gets incremented to 6. i<n wouldn't hold upon completion of the final iteration. Remember, loop invariants musts hold at the beginning (the conditional) and the end (after the last statement) of each iteration.

Also note that it must be 0 <= i<=n rather than 0 < i<=n, since 0<i wouldn't hold at the end of the first iteration.

edited Aug 29 '12 at 22:40

answered Aug 29 '12 at 22:34

Phillip Schmidt

8,805
3
43
67

Explaining a loop invariant

3 Answers3