is this loop invariant and post condition correct?

Question

I was trying to write a loop invariant and post condition for this code:

sum = 0;
for (i = 0; i < 10; ++i)
  ++sum;

sum = 10 is the obvious post condition here. But a friend told me that i = sum is also a loop invariant and sum = 12 is also a post condition. I checked the following:

• loop invariant is initially true: that's true for i = sum since both are 0 initially
• loop invariant is preserved: assume i < 10 and i = sum then after one iteration it's still true that ++i = ++sum
• loop invariant implies post condition: assume i >= 10 and i = sum then sum = 12 is also true

But obviously sum doesn't equal to 12 here. So what's wrong with my reasoning here?

Answer 1

Take a slightly different invariant i == sum && i <= 10. Together with i >= 10 you get then i = sum = 10.

Btw. in your original reasoning you cannot conclude that sum = 12 is true but only that sum >= 10. The latter is correct, just not strong enough to prove the desired result.

Answer 2

// Loop invariant SUM_IS_INDEX: sum == i
// Loop variant: i is increased in every step, and initial value 0 before 10.

sum = 0;
for (i = 0;
        // SUM_IS_INDEX      before the actual loop
        i < 10;
        // next loop step, after first step:
        // sum == index + 1
        ++i
        // next index = index + 1
        // sum == index
        // SUM_IS_INDEX      after a loop step, continuing
        ) {
    // SUM_IS_INDEX
    ++sum;
    // sum == index + 1
}
// Post: i >= 10 (negation of the for condition), SUM_IS_INDEX

The comment about 12 relates more to i. To have i == 10 one would need to add a predicate on increments of just 1.

Best practise is to rewrite the for in control flow order:

sum = 0;
i = 0;
while (i < 10)
    ++sum;
    ++i:
}

This prevents silly mistakes.