Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] bug with loop invariant, wrong loop invariant gets proven
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Fri, 23 Jan 2009 11:19:24 +0100
  • In-reply-to: <49799561.8070004@inria.fr>
  • References: <CCFF6F0509A5405C8124C03AA51AF1B1@AHARDPLACE> <4979803D.2090000@inria.fr><1B357A360A3B42CDB13228DF5371E21B@AHARDPLACE> <49799561.8070004@inria.fr>
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