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 inria.fr (Claude Marché)
  • Date: Fri, 23 Jan 2009 09:30:53 +0100
  • In-reply-to: <CCFF6F0509A5405C8124C03AA51AF1B1@AHARDPLACE>
  • References: <CCFF6F0509A5405C8124C03AA51AF1B1@AHARDPLACE>
Hi,

To illustrate my answer, I attach an instrumented version of your code. 
If you compile and run it you will get :

loop1:
0
1
2
3
4
5
6
7
8
9
loop2:
0
1
2
3
4
5
6
7
8
9
loop3:
1
2
3
4
5
6
7
8
9
10

first loop: invariant 0 <= i < length is indeed true: no bug here

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.

third loop: no problem. Beware that your "rewriting" of the loop has the 
effect that the invariant is now posed after incrementation of i. Which 
makes things different! No bug here.

The key point is to understand where the invariant is supposed to hold, 
which is quite tricky if there are side effects in the loop condition. 
Please reread the loop invariant section of ACSL manual...

By the way: if you think you find a bug, could you use the BTS instead? 
Today, it was fortunate that I was willing to answer quickly, but 
otherwise, a bug report only given in the mailing list might get lost...

Regards,

- Claude





Christoph Weber wrote:
> Hello,
> 
> I think I discovered a bug:
> Following function:
> 
> /*@
>  requires 0 < length;
> */
> int loopinvariant(int length)
> {
> // loop 1: proof of false specification 
>  int i = 0;
>  /*@
>      loop invariant 0 <= i < length;
>  */
>  while(++i != length)
>  {}
>  
> // loop 2: proof failed for intended specification 
>  i = 0;
>  /*@
>      loop invariant 0 <= i <= length;
>  */
>  while(++i != length)
>  {}
>  
> // loop 3: proof of rewritten loop 2
>  i = 0;
>  i++;
>  /*@
>      loop invariant 0 <= i <= length;
>  */
>  while(i != length)
>  {
>  i++;
>  }
>  return 0;
> }
> 
> As you can see from my comments, I expect loop 2 to be correct.
> 
> It is courious, that  a weaker loop invariant fails.
> 
> But loop 1 is falsly specifyed but proven never the less.
> 
> I think this is of interest and please tell me if I misinterpreted something
> 
> Cheers
> 
> Christoph
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> 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

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






-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: bug.c
Type: text/x-csrc
Taille: 656 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090123/b6edd1cd/attachment.c