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 10:28:09 +0100
  • In-reply-to: <4979803D.2090000@inria.fr>
  • References: <CCFF6F0509A5405C8124C03AA51AF1B1@AHARDPLACE> <4979803D.2090000@inria.fr>
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.

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.



> 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"

Please tell me if I havn't understood  "loop invariants" because I am a 
little confused.


Cheers
Christoph 
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: bug.c
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090123/f02af8b3/attachment.txt