--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on January 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] bug with loop invariant, wrong loop invariant gets proven




Christoph Weber wrote:
> Hello and thank you very much for your quick answer.
> 
> I reviewed the ACSL section on loop invariants as well as the wikipedia 
> entry on loop invariants:
> 
> http://en.wikipedia.org/wiki/Loop_invariant
> 
> My Interpretation is, that a loop invariant must hold right after 
> termination of a loop.

But the semantics of loop invariant in ACSL does not imply that. 
Generally speaking, in

//@ invariant I;
while (true) {
    s1;
    if (c) break;
    s2;
}

I is asked to be true when entering the loop, and being preserved by the 
sequence
    s1;
    if (c) break;
    s2;

When the sequence
    s1;
    if (c) break;

exits the loop, I may be made wrong if there are side-effects in s1 (or 
in c!)

In other words: loop invariant hold right after termination of a loop 
only if there are no side-effects between the loop start and the exit. 
But otherwise not necessarily... This is why in textbooks you usually 
prefer to assume side-effect free loop conditions...


> I also ran the a function in  a debug mode. Which showed me, that "i" 
> will reach length in each loop.
> 
> On my opinion, the index should also be printed right after termination.
> 
> Therefore, I added a printf() after each loop. Doing this, "i" will 
> reach 10.

Sure, but the program points where I put my printf are exactly where the 
invariant should hold. It is not the case for your additional printf, as 
said above.

> 
> 
>> second loop: although 0 <= i <= length is true, it is not an *inductive*
>> invariant: imagine i=length before an iteration, then ++i != will be
>> true and i will get value length+1. So no bug here.
> 
> I do not understand, I required "i" to be less then "length"

The VC for preservation of an inductive invariant is like this:

{ 0<=i<=length }
i++;
if (i == length) break;
{ 0<=i<=length }

which is not true when i==length at the beginning!

Hence: the right invariant is 0 <= i < length !


-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |