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: Claude.Marche at (Claude Marché)
  • Date: Fri, 23 Jan 2009 11:01:05 +0100
  • In-reply-to: <1B357A360A3B42CDB13228DF5371E21B@AHARDPLACE>
  • References: <CCFF6F0509A5405C8124C03AA51AF1B1@AHARDPLACE> <> <1B357A360A3B42CDB13228DF5371E21B@AHARDPLACE>

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:
> 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) {
    if (c) break;

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

When the sequence
    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 }
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      |
F-91893 ORSAY Cedex                    |