--- layout: fc_discuss_archives title: Message 38 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



Thank you very much,

I think I understand.

I confused the requirements of annotation-writing with the execution.

That was a valuable information

Cheers

 Christoph


----- Original Message ----- 
From: "Claude March?" <Claude.Marche at inria.fr>
To: "Frama-C public discussion" <frama-c-discuss at lists.gforge.inria.fr>
Sent: Friday, January 23, 2009 11:01 AM
Subject: Re: [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                    |







_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss