CODEWITHSUNDEEP
algorithminvariantshoare-logic
JRR
JRR

Reputation: 6152

is this loop invariant and post condition correct?

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:

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

Upvotes: 0

Views: 290

Answers (2)

Henry
Henry

Reputation: 43738

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.

Upvotes: 3

Joop Eggen
Joop Eggen

Reputation: 109557

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

Upvotes: 1

Related Questions